D:\User\...\Article_final.DVI


Mathematical Problems of Computer Science 49, 103{109, 2018.

On Dependence of I nter pr etation Algor ithms of T yped

Functional P r ogr ams on Canonical N otion of

±-Reduction

D a vit A . Gr ig o r ya n

Department of Informatics and Applied Mathematics, YSU

e-mail: david.grigoryan.a@gmail.com

Abstract

In this paper the interpretation algorithms of typed functional programs are consid-
ered. The interpretation algorithm is based on substitutions, ¯-reduction and canonical
±-reduction. The basic semantics of typed functional program is a function with inde-
terminate values of arguments, which is the main component of its least solution. If
the value of the basic semantics for some values of arguments is indeterminate, then
the interpretation algorithm either stops with the value ?, or works endlessly. It is
shown that seven known interpretation algorithms are ?-depend on canonical notion
of ±-reduction. Here are these algorithms: FS (of full substitution), PES (of paral-
lel external substitution), LES (of left external substitution), PIS (of parallel inner
substitution), LIS (of left inner substitution), ACT (active algorithm), PAS (passive
algorithm).

Keywords: Typed functional program, Canonical ±-reduction, Interpretation al-
gorithm, ?-dependency.

1 . Typ e d ¸-Te r m s , Ca n o n ic a l N o t io n o f ±-R e d u c t io n , Typ e d Fu n c t io n a l P r o -
g r a m s

Th e d e ¯ n it io n s o f t h is s e c t io n c a n b e fo u n d in [1 ; 2 ; 3 ]. L e t M b e a p a r t ia lly o r d e r e d s e t ,
wh ic h h a s a le a s t e le m e n t ?, wh ic h c o r r e s p o n d s t o t h e in d e t e r m in a t e va lu e . E a c h e le m e n t o f
M is c o m p a r a b le o n ly wit h it s e lf a n d wit h ?, wh ic h is t h e le a s t e le m e n t o f M. L e t u s d e ¯ n e
t h e s e t o f t yp e s ( d e n o t e d b y T ypes) .

1 . M 2 T ypes,
2 . If ¯,®1,...,®k 2 T ypes ( k > 0 ) , t h e n t h e s e t o f a ll m o n o t o n ic m a p p in g s fr o m ®1 £:::£®k

in t o ¯ ( d e n o t e d b y [®1 £ ::: £ ®k ! ¯]) b e lo n g s t o T ypes.
L e t ® 2 T ypes, t h e n t h e o r d e r o f t yp e ® ( d e n o t e d b y ord ( ®) ) will b e a n a t u r a l n u m b e r ,

wh ic h is d e ¯ n e d in t h e fo llo win g wa y: if ® = M t h e n ord ( ®) = 0 , if ® = [®1 £ ::: £ ®k ! ¯],
wh e r e ¯; ®1; :::; ®k 2 T ypes; k > 0 , t h e n ord( ®) = max ( ord ( ®1 ) ; :::; ord( ®k ) ; ord( ¯ ) ) + 1 . If x
is a va r ia b le o f t yp e ® a n d c o n s t a n t c 2 ®, t h e n ord( x ) = ord ( c) = ord( ® ) :

L e t ® 2 Typ e s a n d V® b e a c o u n t a b le s e t o f va r ia b le s o f t yp e ®, t h e n V =
S

®2T ypes
V® is

t h e s e t o f a ll va r ia b le s . Th e s e t o f a ll t e r m s , d e n o t e d b y ¤ =
S

®2T ypes
¤ ®, wh e r e ¤ ® is t h e s e t

o f t e r m s o f t yp e ®, is d e ¯ n e d in t h e fo llo win g wa y:

1 0 3



1 0 4 On Dependence of Interpretation Algorithms of Typed Functional Programs on Canonical Notion

1 . If c 2 ®; ® 2 Typ e s , t h e n c 2 ¤ ®,
2 . If x 2 V®, ® 2 Typ e s , t h e n x 2 ¤ ®,
3 . If ¿ 2 ¤ [®1£:::£®k!¯], ti 2 ¤ ®i , wh e r e ¯; ®i 2 T ypes; i = 1 ; :::; k; k ¸ 1 , t h e n ¿ ( t1; :::; tk ) 2

¤ ¯ ( t h e o p e r a t io n o f a p p lic a t io n , ( t1; :::; tk ) is t h e s c o p e o f t h e a p p lic a t o r ¿ ) ,

4 . If ¿ 2 ¤ ¯; xi 2 V®i wh e r e ¯; ®i 2 T ypes, i 6= j ) xi 6= xj; i; j = 1 ; :::; k; k ¸ 1
t h e n ¸x1:::xk[¿ ] 2 ¤ [®1£:::£®k!¯] ( t h e o p e r a t io n o f a b s t r a c t io n , ¿ is t h e s c o p e o f t h e
a b s t r a c t o r ¸x1:::xk ) .

Th e n o t io n o f fr e e a n d b o u n d o c c u r r e n c e s o f va r ia b le s a s we ll a s fr e e a n d b o u n d va r ia b le
a r e in t r o d u c e d in t h e c o n ve n t io n a l wa y. Th e s e t o f a ll fr e e va r ia b le s in t h e t e r m t is d e n o t e d
b y F V(t). Te r m s t1 a n d t2 a r e s a id t o b e c o n g r u e n t ( wh ic h is d e n o t e d b y t1 ´ t2 ) if o n e
t e r m c a n b e o b t a in e d fr o m t h e o t h e r b y r e n a m in g b o u n d va r ia b le s . Th e o c c u r r e n c e o f fr e e
va r ia b le in t h e t e r m is c a lle d in t e r n a l if it d o e s n o t e n t e r t h e a p p lic a t o r , t h e s c o p e o f wh ic h
c o n t a in s a fr e e o c c u r r e n c e o f s o m e va r ia b le . Th e o c c u r r e n c e o f fr e e va r ia b le in t h e t e r m is
c a lle d e xt e r n a l if it d o e s n o t e n t e r t h e s c o p e o f t h e a p p lic a t o r t h a t c o n t a in s a fr e e o c c u r r e n c e
o f s o m e va r ia b le .

L e t t 2 ¤ ®; ® 2 T ypes a n d F V ( t ) ½ fy1; :::; yng; y0 = ( y01 ; :::; y0n ) , wh e r e yi 2 V¯i ; y0i 2
¯i; ¯i 2 T ypes; i = 1 ; :::; n; n ¸ 0 : Th e va lu e o f t h e t e r m t fo r t h e va lu e s o f t h e va r ia b le s
y1; :::yn e qu a l t o y0 = ( y

0
1; :::; y

0
n ) , is d e n o t e d b y V aly0 ( t) a n d is d e ¯ n e d in t h e c o n ve n t io n a l

wa y.

L e t t e r m s t1; t2 2 ¤ ®; ® 2 T ypes, F V ( t1 ) [F V ( t2 ) = fy1; :::; yng; yi 2 V¯i ; ¯i 2 T ypes; i =
1 ; :::; n; n ¸ 0 , t h e n t e r m s t1 a n d t2 a r e c a lle d e qu iva le n t ( d e n o t e d b y t1 » t2 ) if fo r a n y
y0 = ( y

0
1; :::; y

0
n ) , wh e r e y

0
i 2 V¯i ; i = 1 ; :::; n we h a ve t h e fo llo win g : V aly0 ( t1 ) = V aly0 ( t2 ) . A

t e r m t 2 ¤ ®; ® 2 T ypes, is c a lle d a c o n s t a n t t e r m wit h va lu e a 2 ® if t » a.
Fu r t h e r , we a s s u m e t h a t M is a r e c u r s ive s e t a n d t h e c o n s id e r e d t e r m s u s e va r ia b le s o f

a n y o r d e r a n d c o n s t a n t s o f o r d e r · 1 , wh e r e c o n s t a n t s o f o r d e r 1 a r e s t r o n g c o m p u t a b le ,
m o n o t o n ic fu n c t io n s wit h in d e t e r m in a t e va lu e s o f a r g u m e n t s . A fu n c t io n f : M k ! M; k ¸
1 , wit h in d e t e r m in a t e va lu e s o f a r g u m e n t s , is s a id t o b e s t r o n g c o m p u t a b le if t h e r e e xis t s a n
a lg o r it h m , wh ic h s t o p s wit h t h e va lu e f ( m1; :::; mk ) 2 M fo r a ll m1; :::; mk 2 M, s e e [2 ].

A t e r m t 2 ¤ wit h a ¯ xe d o c c u r r e n c e o f a s u b t e r m ¿1 2 ¤ ®, wh e r e ® 2 T ypes, is d e n o t e d
b y t¿1 , a n d a t e r m wit h t h is o c c u r r e n c e o f ¿1 r e p la c e d b y ¿2, wh e r e ¿22 ¤ ®, is d e n o t e d b y t¿2.
To s h o w m u t u a lly d i®e r e n t va r ia b le s o f in t e r e s t x1; :::; xk; k ¸ 1 , o f a t e r m t, t h e n o t a t io n
t[x1; :::; xk] is u s e d . Th e n o t a t io n t[t1; :::; tk] d e n o t e s t h e t e r m o b t a in e d b y t h e s im u lt a n e o u s
s u b s t it u t io n o f t h e t e r m s t1; :::; tk fo r a ll fr e e o c c u r r e n c e s o f t h e va r ia b le s x1; :::; xk, r e s p e c -
t ive ly, wh e r e xi 2 V®i ; i 6= j ) xi 6´ xj, ti 2 ¤ ®i ; ®i 2 T ypes; i; j = 1 ; ::; k; k ¸ 1 .

A t e r m o f t h e fo r m ¸x1:::xk[¿ [x1; :::; xk]]( t1; :::; tk ) , wh e r e xi 2 V®; i 6= j ) xi 6´ xj ; ¿ 2
¤ ; ti 2 ¤ ®i ; ®i 2 T ypes; i; j = 1 ; :::; k; k ¸ 1 , is c a lle d a ¯-r e d e x, it s c o n vo lu t io n is t h e t e r m
¿ [t1; :::; tk]. Th e s e t o f a ll p a ir s ( ¿0; ¿1 ) , wh e r e ¿0 is a ¯-r e d e x a n d ¿1 is it s c o n vo lu t io n , is
c a lle d a n o t io n o f ¯-r e d u c t io n a n d is d e n o t e d b y ¯. A o n e -s t e p ¯-r e d u c t io n ( !¯ ) a n d ¯-
r e d u c t io n ( !!¯ ) a r e d e ¯ n e d in t h e c o n ve n t io n a l wa y. A t e r m c o n t a in in g n o ¯-r e d e xe s is
c a lle d a ¯-n o r m a l fo r m . Th e s e t o f a ll ¯-n o r m a l fo r m s is d e n o t e d b y ¯-N F .

±-r e d e x h a s a fo r m f ( t1; :::; tk ) , wh e r e f 2 [M k ! M ], ti 2 ¤ M ; i = 1 ; :::; k; k ¸ 1 , it s
c o n vo lu t io n is e it h e r m 2 M a n d in t h is c a s e f ( t1; :::; tk ) » m o r a s u b t e r m ti a n d in t h is
c a s e f ( t1; :::; tk ) » ti; i = 1 ; :::; k. A ¯ xe d s e t o f t e r m p a ir s ( ¿0; ¿1 ) , wh e r e ¿0 is a ±-r e d e x
a n d ¿1 is it s c o n vo lu t io n , is c a lle d a n o t io n o f ±-r e d u c t io n a n d is d e n o t e d b y ±. A o n e -s t e p
±-r e d u c t io n ( !± ) a n d ±-r e d u c t io n ( !!± ) a r e d e ¯ n e d in t h e c o n ve n t io n a l wa y.



D. Grigoryna 1 0 5

A o n e -s t e p ¯±-r e d u c t io n ( !¯± ) a n d ¯±-r e d u c t io n ( !!¯± ) a r e d e ¯ n e d in t h e c o n ve n t io n a l
wa y. A t e r m c o n t a in in g n o ¯±-r e d e xe s is c a lle d a n o r m a l fo r m . Th e s e t o f a ll n o r m a l fo r m s
is d e n o t e d b y NF .

A n o t io n o f ±-r e d u c t io n is c a lle d a s in g le -va lu e d n o t io n o f ±-r e d u c t io n , if ± is a s in g le -
va lu e d r e la t io n , i.e ., if ( ¿0; ¿1 ) 2 ± a n d ( ¿0; ¿2 ) 2 ±, t h e n ¿1 ´ ¿2, wh e r e ¿0; ¿1; ¿2 2 ¤ M . A
n o t io n o f ±-r e d u c t io n is c a lle d a n e ®e c t ive n o t io n o f ±-r e d u c t io n if t h e r e e xis t s a n a lg o r it h m ,
wh ic h fo r a n y t e r m f ( t1; :::; tk ) , wh e r e f 2 [M k ! M ], ti 2 ¤ M ; i = 1 ; :::; k; k ¸ 1 , g ive s it s
c o n vo lu t io n if f ( t1; :::; tk ) is a ±-r e d e x a n d s t o p s wit h a n e g a t ive a n s we r o t h e r wis e .

De¯nition 1. [3 ] An e®ective, single-valued notion of ±-reduction is called a canonical no-
tion of ±-reduction if:

1. t 2 ¯-NF ,t » m; m 2 M n f?g ) t !! ±m,

2. t 2 ¯-NF ; F V ( t ) = ;; t » ? ) t !!± ?.

T heor em 1. (on canonical notion of ±-reduction). F or every recursive set of strong com-
putable, monotonic functions with indeterminate values of arguments there exists a canonical
notion of ±-reduction.

P r o ve d in [3 ].

Typ e d fu n c t io n a l p r o g r a m P is t h e fo llo win g s ys t e m o f e qu a t io n s :

P

8
><
>:

F1 = t1[F1; :::; Fn]
:::

Fn = tn[F1; :::; Fn]
( 1 )

wh e r e Fi 2 V®i ; i 6= j ) Fi 6´ Fj; ti[F1; :::; Fn] 2 ¤ ®i , FV ( ti[F1; :::; Fn]) ½ fF1; :::; Fng,
®i 2 T ypes; i; j = 1 ; :::; n; n ¸ 1 ; ®1 = [M k ! M ]; k ¸ 1 .

E ve r y t yp e d fu n c t io n a l p r o g r a m P h a s t h e le a s t s o lu t io n ( s e e [1 ]) . L e t ( f1; :::; fn ) 2
®1 £ ::: £ ®n b e t h e le a s t s o lu t io n o f P , t h e n t h e ¯ r s t c o m p o n e n t f1 2 [M k ! M] o f t h e
le a s t s o lu t io n is s a id t o b e t h e b a s ic s e m a n t ic s o f t h e p r o g r a m P a n d is d e n o t e d b y fp.

F ix ( P ) = f ( m1; :::; mk; m ) j fp ( m1; :::; mk ) = m; wh e r e m; m1; :::; mk 2 M; k ¸ 1 g.

2 . In t e r p r e t a t io n A lg o r it h m s , ?-D e p e n d e n c e
Th e in p u t o f t h e in t e r p r e t a t io n a lg o r it h m A is a p r o g r a m P o f t h e fo r m ( 1 ) , a t e r m
F1 ( m1; :::; mk ) , wh e r e mi 2 M , i = 1 ; :::; k; k ¸ 1 a n d a c a n o n ic a l n o t io n o f ±-r e d u c t io n .
A lg o r it h m A s t o p s wit h t h e r e s u lt m 2 M o r wo r ks in ¯ n it e ly. A lg o r it h m A u s e s t h r e e kin d s
o f o p e r a t io n s : s u b s t it u t io n o f t h e t e r m s t1; :::; tn in s t e a d o f s o m e fr e e o c c u r r e n c e s o f va r ia b le s
F1; :::; Fn, o n e -s t e p ¯-r e d u c t io n a n d o n e -s t e p ±-r e d u c t io n .

P rocA ( P ) = f ( m1; :::; mk; m ) j a lg o r it h m A s t o p s fo r t h e p r o g r a m P a n d t h e t e r m
F1 ( m1; :::; mk ) wit h t h e r e s u lt m, wh e r e m; m1; :::; mk 2 M; k ¸ 1 g

In t e r p r e t a t io n a lg o r it h m A is c o n s is t e n t if fo r a n y p r o g r a m P a n d fo r a n y c a n o n ic a l n o t io n
o f ±-r e d u c t io n we h a ve : P rocA ( P ) ½ F ix ( P ) .
T heor em 2. E very interpretation algorithm A is consistent.



1 0 6 On Dependence of Interpretation Algorithms of Typed Functional Programs on Canonical Notion

P r oof. Fo llo ws fr o m t h e r e s u lt s o f [4 ].

De¯nition 2. An interpretation algorithm A ?-depends on canonical notion of ±-reduction
if there exist ±1 and ±2 canonical notions of ±-reduction, program P and m1; :::; mk 2 M; k ¸ 1
such that: ( m1; :::; mk; ? ) 2 P rocA ( P ) for ±1 and ( m1; :::; mk; ? ) 62 P rocA ( P ) for ±2.

To s h o w a s e qu e n c e Fi1 ; :::; Fis; s ¸ 1 o f s o m e fr e e o c c u r e n c e s o f va r ia b le s o f t h e s e t fF1; :::; Fng
in t h e t e r m t, t h e n o t io n t < Fi1; :::; Fis > is u s e d . Th e n o t io n t < ti1; :::; tis > d e n o t e s t h e
t e r m o b t a in e d b y t h e s im u lt a n e o u s s u b s t it u t io n o f t h e t e r m s ti1; :::; tis fo r fr e e o c c u r e n c e s
Fi1 ; :::; Fis, r e s p e c t ive ly.

De¯nition 3. (Interpretation algorithms) F S, P E S, L E S, P IS, L IS, P AS, ACT

S TE P 1 :
F S, P E S, L E S, P IS, L IS, P AS, ACT : If t 2 N F a n d F V ( t ) \ fF1; :::; Fng = ; t h e n t.

e ls e g o t o S t e p 2 .
S TE P 2 :
F S, P E S, L E S, P IS, L IS : If t ´ t¿ wh e r e ¿ is a le ft m o s t r e d e x ( ±-r e d e x o r ¯-r e d e x) , t h e n

A( P; t¿0 ) , wh e r e ¿
0 is t h e c o n vo lu t io n o f t h e ¿ , A 2 fF S; P ES; LES; P IS; LISg, e ls e g o t o

S t e p 3 .
ACT, P AS : If t ´ tFi ; ( 0 · i · n) , wh e r e tFi is t h e t e r m t wit h a ¯ xe d le ft m o s t fr e e

o c c u r r e n c e o f a va r ia b le o f t h e s e t fF1; :::; Fng, wh ic h is lo c a t e d t o t h e le ft o f t h e le ft m o s t
r e d e x, t h e n A ( P; tti ) , wh e r e A 2 fACT; P ASg, e ls e g o t o S t e p 3 .

S TE P 3 :
F S : If t ´ t[F1; :::; Fn], t h e n F S ( P; t[t1; :::; tn]) .
P E S : If t ´ t < Fi1 ; :::; Fik >, wh e r e Fi1 ; :::; Fik ; k > 0 is t h e s e qu e n c e o f a ll e xt e r n a l fr e e

o c c u r r e n c e s o f va r ia b le s o f t h e s e t fF1; :::; Fng, t h e n P ES ( P; t < ti1; :::; tik >) .
L E S : If t ´ tFi , wh e r e Fi is t h e le ft m o s t e xt e r n a l fr e e o c c u r r e n c e o f a va r ia b le o f t h e s e t

fF1; :::; Fng, t h e n LES ( P; tti ) .
P IS : If t ´ t < Fi1; :::; Fik >, wh e r e Fi1; :::; Fik ; k > 0 is t h e s e qu e n c e o f a ll in t e r n a l fr e e

o c c u r r e n c e s o f va r ia b le s o f t h e s e t fF1; :::; Fng, t h e n P IS ( P; t < ti1 ; :::; tik >) .
L IS : If t ´ tFi , wh e r e Fi is t h e le ft m o s t in t e r n a l fr e e o c c u r r e n c e o f a va r ia b le o f t h e s e t

fF1; :::; Fng, t h e n LIS ( P; tti ) .
ACT : If t ´ t¿ wh e r e ¿ ´ ¸x1:::xr[¿[x1; :::; xr]]( ¿1; :::; ¿r ) a n d ¿ is a le ft m o s t r e d e x, t h e n

ACT ( P; t¿ [ACT (P;¿1);:::;ACT (P;¿r)] ) , e ls e g o t o S t e p 4 .
P AS : If t ´ t¿ wh e r e ¿ ´ ¸x1:::xr[¿[x1; :::; xr]]( ¿1; :::; ¿r ) a n d ¿ is a le ft m o s t r e d e x, t h e n

P AS ( P; t¿ [¿1;:::;¿r] ) , e ls e g o t o S t e p 4 .
S TE P 4 :
ACT, P AS : If t ´ t¿ wh e r e ¿ is a le ft m o s t r e d e x, wh ic h is a ±-r e d e x, t h e n A ( P; t¿0 ) , wh e r e

¿ 0 is t h e c o n vo lu t io n o f t h e ¿, A 2 fACT; P ASg.

T heor em 3. Any interpretation algorithm F S, P E S, L E S, P IS, L IS, P AS, ACT ?-depends
on canonical notion of ±-reduction.

P r oof. L e t u s ¯ x M = N [ f?g, wh e r e N = f 0 ; 1 ; 2 ; :::g a n d C = fnot eqg wh e r e
not eq 2 [M 2 ! M] is a b u ilt -in fu n c t io n a n d fo r e ve r y m1; m2 2 M we h a ve :

not eq ( m1; m2 ) =

(
1 ; if m1; m2 2 N and m1 6= m2
?; otherwise



D. Grigoryna 1 0 7

It is e a s y t o s e e t h a t not eq is a s t r o n g c o m p u t a b le , n a t u r a lly e xt e n d e d fu n c t io n wit h
in d e t e r m in a t e va lu e s o f a r g u m e n t s ( a fu n c t io n is s a id t o b e n a t u r a lly e xt e n d e d , if it s va lu e
is ? wh e n e ve r t h e va lu e o f a t le a s t o n e o f t h e a r g u m e n t s is ? ) . Th e r e fo r e , fr o m Th e o r e m 1
it fo llo ws t h a t t h e r e e xis t s t h e fo llo win g c a n o n ic a l n o t io n o f ±-r e d u c t io n ± fo r t h e s e t C:

± is : ( not eq ( n1; n2 ) ; 1 ) 2 ±, wh e r e n1; n2 2 N a n d n1 6= n2
( not eq ( n; n) ; ?) 2 ±, wh e r e n 2 N
( not eq ( n; ?) ; ? ) 2 ±, wh e r e n 2 N
( not eq ( ?; n) ; ? ) 2 ±, wh e r e n 2 N
( not eq ( ?; ? ) ; ? ) 2 ±

L e t u s d e ¯ n e t wo c a n o n ic a l n o t io n s o f ±-r e d u c t io n ±1 a n d ±2.

±1 is : ( not eq ( n1; n2 ) ; 1 ) 2 ±1, wh e r e n1; n2 2 N a n d n1 6= n2
( not eq ( t; t ) ; ?) 2 ±1, wh e r e t 2 ¤ M
( not eq ( t; ? ) ; ?) 2 ±1, wh e r e t 2 ¤ M
( not eq ( ?; t ) ; ?) 2 ±1, wh e r e t 2 ¤ M

±2 is : ( not eq ( n1; n2 ) ; 1 ) 2 ±2, wh e r e n1; n2 2 N a n d n1 6= n2
( not eq ( m; m ) ; ?) 2 ±2, wh e r e m 2 M
( not eq ( t; ? ) ; ?) 2 ±2, wh e r e t 2 ¤ M
( not eq ( ?; t ) ; ?) 2 ±2, wh e r e t 2 ¤ M

It is e a s y t o s e e t h a t ±1 is a n e ®e c t ive , s in g le -va lu e d n o t io n o f ±-r e d u c t io n . Th e r e fo r e ,
t o s h o w t h a t ±1 is a c a n o n ic a l n o t io n o f ±-r e d u c t io n it s u ± c e s t o s h o w t h a t ± ½ ±1. L e t
( ¿1; ¿2 ) 2 ±, wh e r e ¿1; ¿2 2 M , t h e n t h e fo llo win g c a s e s a r e p o s s ib le :

¿1 ´ n1 a n d ¿2 ´ n2, wh e r e n1; n2 2 N a n d n1 6= n2, t h e n it is o b vio u s t h a t
( not eq ( n1; n2 ) ; 1 ) 2 ±1.
¿1 ´ ¿2 ´ n, wh e r e n 2 N , t h e n fr o m ( not eq ( t; t) ; ? ) 2 ±1, wh e r e t 2 ¤ M , fo llo ws t h a t
( not eq ( n; n) ; ?) 2 ±1.
¿1 ´ n a n d ¿2 ´ ?, wh e r e n 2 N , t h e n fr o m ( not eq ( t; ? ) ; ? ) 2 ±1, wh e r e t 2 ¤ M ,
fo llo ws t h a t ( not eq ( n; ? ) ; ? ) 2 ±1.
¿1 ´ ? a n d ¿2 ´ n, wh e r e n 2 N , t h e n fr o m ( not eq ( ?; t ) ; ? ) 2 ±1, wh e r e t 2 ¤ M ,
fo llo ws t h a t ( not eq ( ?; n) ; ? ) 2 ±1.
¿1 ´ ? a n d ¿2 ´ ?, t h e n fr o m ( not eq ( t; t) ; ? ) 2 ±1, wh e r e t 2 ¤ M , fo llo ws t h a t
( not eq ( ?; ? ) ; ? ) 2 ±1.

It is e a s y t o s e e t h a t ±2 is a n e ®e c t ive , s in g le -va lu e d n o t io n o f ±-r e d u c t io n . Th e r e fo r e ,
t o s h o w t h a t ±2 is a c a n o n ic a l n o t io n o f ±-r e d u c t io n it s u ± c e s t o s h o w t h a t ± ½ ±2. L e t
( ¿1; ¿2 ) 2 ±, wh e r e ¿1; ¿2 2 M , t h e n t h e fo llo win g c a s e s a r e p o s s ib le :

¿1 ´ n1 a n d ¿2 ´ n2, wh e r e n1; n2 2 N a n d n1 6= n2, t h e n it is o b vio u s t h a t
( not eq ( n1; n2 ) ; 1 ) 2 ±2.
¿1 ´ ¿2 ´ n, wh e r e n 2 N, t h e n fr o m ( not eq ( m; m ) ; ? ) 2 ±2, wh e r e m 2 M, fo llo ws
t h a t ( not eq ( n; n) ; ? ) 2 ±2.
¿1 ´ n a n d ¿2 ´ ?, wh e r e n 2 N , t h e n fr o m ( not eq ( t; ? ) ; ? ) 2 ±2, wh e r e t 2 ¤ M ,
fo llo ws t h a t ( not eq ( n; ? ) ; ? ) 2 ±2.



1 0 8 On Dependence of Interpretation Algorithms of Typed Functional Programs on Canonical Notion

¿1 ´ ? a n d ¿2 ´ n, wh e r e n 2 N , t h e n fr o m ( not eq ( ?; t ) ; ?) 2 ±2, wh e r e t 2 ¤ M ,
fo llo ws t h a t ( not eq ( ?; n) ; ? ) 2 ±2.
¿1 ´ ? a n d ¿2 ´ ?, t h e n fr o m ( not eq ( m; m) ; ? ) 2 ±2, wh e r e m 2 M, fo llo ws t h a t
( not eq ( ?; ? ) ; ?) 2 ±2.

L e t P b e t h e fo llo win g p r o g r a m , wh e r e F1; F2 2 V[M !M]; x 2 VM

P

(
F1 = ¸x[not eq ( F2 ( x) ; F2 ( x ) ) ]
F2 = ¸x[F2 ( x ) ]

Fo r ±1, p r o g r a m P a n d F S; P ES; LES; P IS; LIS; P AS; ACT we h a ve :
F1 ( 0 ) ;
¸x[not eq ( F2 ( x) ; F2 ( x) ) ]( 0 ) !¯ not eq ( F2 ( 0 ) ; F2 ( 0 ) ) !±1?;
Th e r e fo r e ( 0 ; ? ) 2 P rocF S ( P ) , ( 0 ; ? ) 2 P rocP ES ( P ) , ( 0 ; ?) 2 P rocLES ( P ) ,
( 0 ; ? ) 2 P rocP IS ( P ) , ( 0 ; ?) 2 P rocLIS ( P ) , ( 0 ; ?) 2 P rocP AS ( P ) , ( 0 ; ? ) 2 P rocACT ( P ) .

Fo r ±2, p r o g r a m P a n d ACT , LIS, P AS, LES we h a ve :
F1 ( 0 ) ;
¸x[not eq ( F2 ( x) ; F2 ( x) ) ]( 0 ) !¯ not eq ( F2 ( 0 ) ; F2 ( 0 ) ) ;
not eq ( ¸x[F2 ( x) ]( 0 ) ; F2 ( 0 ) ) !¯ not eq ( F2 ( 0 ) ; F2 ( 0 ) ) ;
... a n d s o o n .
Th e r e fo r e ( 0 ; ?) 62 P rocLES ( P ) , ( 0 ; ? ) 62 P rocLIS ( P ) , ( 0 ; ? ) 62 P rocP AS ( P ) , ( 0 ; ? ) 62

P rocACT ( P ) .

Fo r ±2, p r o g r a m P a n d F S, P ES, P IS we h a ve :
F1 ( 0 ) ;
¸x[not eq ( F2 ( x) ; F2 ( x) ) ]( 0 ) !¯ not eq ( F2 ( 0 ) ; F2 ( 0 ) ) ;
not eq ( ¸x[F2 ( x) ]( 0 ) ; ¸x[F2 ( x ) ]( 0 ) ) !¯ not eq ( F2 ( 0 ) ; F2 ( 0 ) ) ) ;
... a n d s o o n .
Th e r e fo r e ( 0 ; ? ) 62 P rocF S ( P ) , ( 0 ; ? ) 62 P rocP ES ( P ) , ( 0 ; ?) 62 P rocP IS ( P ) .
In c o n c lu s io n , fo r e a c h in t e r p r e t a t io n a lg o r it h m A 2 fF S; P ES; LES; P IS; LIS; P AS; ACT g

t h e r e e xis t ±1 a n d ±2 c a n o n c ia l n o t io n s o f ±-r e d u c t io n a n d p r o g r a m P s u c h t h a t ( 0 ; ? ) 2
P rocA ( P ) fo r ±1 a n d ( 0 ; ? ) 62 P rocA ( P ) fo r ±2, t h e r e fo r e A ?-d e p e n d s o n c a n o n ic a l n o t io n
o f ±-r e d u c t io n .

Refer ences

[1 ] S . A . N ig iya n \ Fu n c t io n a l L a n g u a g e s " , P rogramming and Computer Software, vo l. 1 7 ,
n o . 5 , p p . 2 9 0 -2 9 7 , 1 9 9 2 .

[2 ] S . A . N ig iya n , \ On n o n -c la s s ic a l t h e o r y o f c o m p u t a b ilit y" , P roceedings of the YSU,
P hysical and M athematical Sciences, n o .1 , p p .5 2 -6 0 , 2 0 1 5 .

[3 ] S . A . N ig iya n a n d T.V .K h o n d ka r ya n , \ On c a n o n ic a l n o t io n o f ±-r e d u c t io n a n d o n t r a n s -
la t io n o f t yp e d ¸-t e r m s in t o u n t yp e d ¸-t e r m s " , P roceedings of the YSU, P hysical and
M athematical Sciences, n o . 1 , p p . 4 6 -5 2 , 2 0 1 7 .

[4 ] R . Y u . H a ko p ia n , \ On p r o c e d u r a l s e m a n t ic s o f s t r o n g t yp e d fu n c t io n a l p r o g r a m s " , P ro-
ceedings of YSU, Natural Sciences, ( in R u s s ia n ) , n o . 3 , p p .5 9 -6 9 , 2 0 0 8 .



D. Grigoryna 1 0 9

Submitted 10.10.2017, accepted 18.01.2018.

îÇåǽ³óí³Í ýáõÝÏóÇáÝ³É Íñ³·ñ»ñÇ ÇÝï»ñåñ»ï³ódzÛÇ
³É·áñÇÃÙÝ»ñÇ Ï³Ëí³ÍáõÃÛáõÝÁ ϳÝáÝÇÏ

±-黹áõÏódzÛÇ ·³Õ³÷³ñÇó

¸. ¶ñÇ·áñÛ³Ý

²Ù÷á÷áõÙ

²ß˳ï³ÝùáõÙ ¹Çï³ñÏí³Í »Ý ïÇåǽ³óí³Í ýáõÝÏóÇáÝ³É Íñ³·ñ»ñÇ ÇÝï»ñåñ»-
ï³ódzÛÇ ³É·áñÇÃÙÝ»ñÁ: ÆÝï»ñåñ»ï³ódzÛÇ ³É·áñÇÃÙÁ ÑÇÙÝí³Í ¿ ï»Õ³¹ñÙ³Ý, ¯-
黹áõÏódzÛÇ ¨ ϳÝáÝÇÏ ±-黹áõÏódzÛÇ ·áñÍáÕáõÃÛáõÝÝ»ñÇ íñ³: îÇåǽ³óí³Í ýáõÝÏ-
óÇáÝ³É Íñ³·ñ»ñÇ ÑÇÙÝ³Ï³Ý ë»Ù³ÝïÇÏ³Ý ³Ýáñáß ³ñ·áõÙ»ÝïÝ»ñáí ýáõÝÏódz ¿, áñÁ
÷áùñ³·áõÛÝ ÉáõÍÙ³Ý ÑÇÙÝ³Ï³Ý µ³Õ³¹ñÇãÝ ¿: ºÃ» ÑÇÙÝ³Ï³Ý ë»Ù³ÝïÇϳÛÇ ³ñÅ»ùÁ
áñáß ³ñÅ»ùÝ»ñÇ ¹»åùáõÙ ³Ýáñáß ¿, ³å³ ÇÝï»ñåñ»ï³ódzÛÇ ³É·áñÇÃÙÁ ϳ٠ϳݷ ¿
³éÝáõÙ ? ³ñÅ»ùáí, ϳ٠³ß˳ïáõÙ ¿ ³Ýí»ñç: òáõÛó ¿ ïñí³Í, áñ 7 ѳÛïÝÇ ÇÝï»ñ-
åñ»ï³ódzÛÇ ³É·áñÇÃÙÝ»ñÁ ?-ϳËí³Í »Ý ϳÝáÝÇÏ ±-黹áõÏódzÛÇ ·³Õ³÷³ñÇó: ²Û¹
³É·áñÇÃÙ»ñÁ Ñ»ï¨Û³ÉÝ »Ý` FS (ÉÇñí ï»Õ³¹ñÙ³Ý), PES (½áõ·³Ñ»é ³ñï³ùÇÝ ï»Õ³¹ñÙ³Ý),
LES (Ó³Ë ³ñï³ùÇÝ ï»Õ³¹ñÙ³Ý), PIS (½áõ·³Ñ»é Ý»ñùÇÝ ï»Õ³¹ñÙ³Ý), LIS (Ó³Ë Ý»ñùÇÝ
ï»Õ³¹ñÙ³Ý), ACT (³ÏïÇí ³É·áñÇÃÙ), PAS (å³ëÇí ³É·áñÇÃÙ).

Î çàâèñèìîñòè àëãîðèòìîâ èíòåðïðåòàöèè òèïèçèðîâàííûõ
ôóíêöèîíàëüíûõ ïðîãðàìì îò êàíîíè÷åñêîãî ïîíÿòèÿ

±-ðåäóêöèè
Ä. Ãðèãîðÿí

Àííîòàöèÿ

 äàííîé ðàáîòå ðàññìàòðèâàþòñÿ èíòåðïðåòàòîðû òèïèçèðîâàííûõ ôóíê-
öèîíàëüíûõ ïðîãðàìì. Àëãîðèòì èíòåðïðåòàöèè îñíîâàí íà ïîäñòàíîâêàõ, ¯-
ðåäóêöèè è êàíîíè÷åñêîé ±-ðåäóêöèè. Îñíîâíàÿ ñåìàíòèêà òèïèçèðîâàííûõ
ôóíêöèîíàëüíûõ ïðîãðàìì åñòü ôóíêöèÿ ñ íåîïðåäåëåííûìè çíà÷åíèÿìè àðãó-
ìåíòîâ, êîòîðàÿ ÿâëÿåòñÿ ãëàâíîé êîìïîíåíòîé åå íàèìåíüøåãî ðåøåíèÿ. Åñëè
çíà÷åíèå îñíîâíîé ñåìàíòèêè, äëÿ íåêîòîðûõ çíà÷åíèé àðãóìåíòîâ, åñòü íåîï-
ðåäåëåííîñòü, òî àëãîðèòì èíòåðïðåòàöèè ëèáî îñòàíàâëèâàåòñÿ ñî çíà÷åíèåì
?, ëèáî ðàáîòàåò áåñêîíå÷íî. Ïîêàçàíî, ÷òî ñåìü èçâåñòíûõ àëãîðèòìîâ èíòåð-
ïðåòàöèè ?-çàâèñÿò îò êàíîíè÷åñêîãî ïîíÿòèÿ ±-ðåäóêöèè. Âîò ýòè àëãîðèòìû:
FS (ïîëíîé ïîäñòàíîâêè), PES (ïàðàëëåëüíîé âíåøíåé ïîäñòàíîâêè), LES (ëåâîé
âíåøíåé ïîäñòàíîâêè), PIS (ïàðàëëåëüíîé âíóòðåííåé ïîäñòàíîâêè), LIS (ëåâîé
âíóòðåííåé ïîäñòàíîâêè), ACT (àêòèâíûé àëãîðèòì), PAS (ïàññèâíûé àëãîðèòì).