Article_DAVIT.DVI


Mathematical Problems of Computer Science 50, 81-87, 2018.

On Chur ch-Rosser P r oper ty of N otion of ¯±-Reduction

for Canonical N otion of ±-Reduction

D a vit A . Gr ig o r ya n

Department of Informatics and Applied Mathematics
Yerevan State University

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

Abstract

In this paper the canonical notions of ±-reduction for typed ¸-terms are considered.
Typed ¸-terms use variables of any order and constants of order · 1, where constants
of order 1 are strongly computable, monotonic functions with indeterminate values of
arguments. The canonical notions of ±-reduction are the notions of ±-reduction that are
used in the implementations of functional programming languages. It is shown that for
the main canonical notion of ±-reduction the notion of ¯±-reduction has the Church-
Rosser property. It is also shown that there exists a canonical notion of ±-reduction
such that the notion of ¯±-reduction does not have Church-Rosser property.

Keywords: Canonical notion of ±-reduction, Church-Rosser property, ¯±-reduction.

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

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 ]{ [4 ]. 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 , a n d 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 ? a n d it s e lf. 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 Typ e s ) .

1 . M 2 T ypes,

2 . If ¯,®1,...,®k 2 Typ e s ( 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 Typ e s .

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( ® ) = 1 + max( ord( ®1 ) ; :::; ord( ®k ) ; ord ( ¯ ) ) . 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 t h e in fo llo win g wa y:

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 ¤ ®,

8 1



8 2 On Church-Rosser Property of Notion of ¯±-Reduction for Canonical Notion of ±-Reduction

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 ) ,

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 ) .

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 .

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, s e e [2 ].
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 ly 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 ly 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 va lu e f ( m1; :::; mk ) 2 M fo r a ll m1; :::; mk 2 M, s e e [1 ].

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 s u b s t it u t io n is
s a id t o b e a d m is s ib le if a ll fr e e va r ia b le s o f t h e t e r m b e in g s u b s t it u t e d r e m a in fr e e a ft e r t h e
s u b s t it u t io n . W e will c o n s id e r o n ly a d m is s ib le s u b s t it u t io n s .

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.

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 ( !! ) 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 .



D. Grigoryan 8 3

De¯nition 1: [2] 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: [2] F or every recursive set of strong computable, monotonic functions with
indeterminate values of arguments there exists a canonical notion of ±-reduction.

2 . Ma in Ca n o n ic a l N o t io n o f ±-R e d u c t io n , Ch u r c h -R o s s e r P r o p e r t y

L e t C b e a r e c u r s ive s e t o f s t r o n g ly 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 . L e t u s ¯ x t h e fo llo win g n o t io n o f ±-r e d u c t io n , wh ic h c o n t a in s o n ly t h e
fo llo win g p a ir s , wh e r e fo r e ve r y f 2 C; f : M k ! M; k ¸ 1 we h a ve :

1 . if f ( m1; :::; mk ) = m, wh e r e m; m1; :::; mk 2 M; m 6= ?, t h e n ( f ( ¹1; :::; ¹k ) ; m ) 2 ±,
wh e r e ¹i = mi if mi 6= ?, a n d ¹i ´ ti; ti 2 ¤ M if mi = ?; i = 1 ; :::; k; k ¸ 1 .

2 . if f ( m1; :::; mk ) = ?, wh e r e m1; :::; mk 2 M , t h e n ( f ( m1; :::; mk ) ; ?) 2 ±.
Fr o m t h e p r o o f o f Th e o r e m 1 it fo llo ws t h a t t h e ± 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 .

Th e ± is c a lle d a m a in c a n o n ic a l n o t io n o f ±-r e d u c t io n .

De¯nition 2: The term t 2 ¤ is said to be strongly normalizable, if the length of each
¯±-reduction chain from the term t is ¯nite.

T heor em 2: [3] E very term is strongly normalizable.

T heor em 3: [3] F or every term t 2 ¤ , if t !!¯ t0; t !!¯ t00 and t0; t00 2 ¯-NF then
t0 ´ t00.

De¯nition 3: L et t 2 ¤ ®; ® 2 T ypes and t ´ t1 ! ::: ! tn; n ¸ 1 , where ti 2 ¤ ®; i =
1 ; :::; n, then the sequence t1; :::; tn is called the inference of the term tn from the term t and
n is called the length of that inference.

De¯nition 4: The inference tree of the term t is an oriented tree with the root t and if a
term ¿ is some node of the tree and ¿1; :::; ¿k; k ¸ 0 are all ¯±-redexes of ¿ , then ¿¿01 ; :::; ¿¿ 0k
are all descendants of the node ¿ , where ¿ 0i is the convolution of ¿i; i = 1 ; :::; k.

It is e a s y t o s e e t h a t e a c h n o d e in t h e in fe r e n c e t r e e o f t h e t e r m t h a s a ¯ n it e n u m b e r o f
d e s c e n d a n t s a n d if ¿ is a le a f o f t h a t t r e e , t h e n ¿ 2 NF . Th e h e ig h t o f a n in fe r e n c e t r e e o f
t h e t e r m t is t h e le n g t h o f t h e lo n g e s t p a t h fr o m t h e r o o t t t o a le a f. Th e s e t o f a ll t e r m s ,
t h e h e ig h t o f t h e in fe r e n c e t r e e o f wh ic h is e qu ia l t o n ¡ 1 , is d e n o t e d b y ¤ (n); n ¸ 1 .

De¯nition 5: The notion of ¯±-reduction has the Church-R osser property (CR -property) if
for every term t 2 ¤ ®; ® 2 T ypes, if t !! t1 and t !! t2, t1; t2 2 ¤ ®, then there exists a
term t0 2 ¤ ® such that t1 !! t0 and t2 !! t0.

T heor em 4: F or the main canonical notion of ±-reduction the notion of ¯±-reduction has
the Church-R osser property.



8 4 On Church-Rosser Property of Notion of ¯±-Reduction for Canonical Notion of ±-Reduction

P r oof. L e t t 2 ¤ (1), t h e n t 2 NF a n d t ´ t1 ´ t2 ´ t0. N o w, le t u s s u p p o s e t h a t
CR -p r o p e r t y h o ld s fo r e ve r y t e r m ¿ 2 ¤ (k); k · n ¡ 1 ; n ¸ 2 a n d s h o w t h a t it h o ld s fo r
e ve r y t e r m t 2 ¤ (n). If t ´ t1, t h e n t1 !! t2 a n d t0 ´ t2. If t ´ t2, t h e n t2 !! t1 a n d
t0 ´ t1. If t1 6´ t a n d t2 6´ t, t h e n t h e r e e xis t t e r m s t01; t02 2 ¤ , s u c h t h a t t ! t01 !! t1 a n d
t ! t02 !! t2. Th e r e fo r e , t h e r e e xis t ¯±-r e d e xe s ¿1; ¿2 2 ¤ s u c h t h a t t ´ t¿1 ´ t¿2, t01 ´ t¿01
a n d t02 ´ t¿ 02, wh e r e t e r m s ¿

0
1; ¿

0
2 a r e t h e c o n vo lu t io n s o f ¿1 a n d ¿2, a c c o r d in g ly. L e t u s s h o w

t h a t t h e r e e xis t s a t e r m t0 s u c h t h a t t01 !! t0 a n d t02 !! t0.
If ¿1 is n o t a s u b t e r m o f ¿2 a n d ¿2 is n o t a s u b t e r m o f ¿1, t h e n t¿1;¿2 ! t¿ 01;¿2 ! t¿ 01;¿02 a n d

t¿1;¿2 ! t¿1;¿ 02 ! t¿ 01;¿ 02. Th e r e fo r e t
0 ´ t¿ 0

1
;¿ 0

2
.

If ¿2 is a s u b t e r m o f ¿1 o r ¿1 is a s u b t e r m o f ¿2, 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 ) ¿1 a n d ¿2 a r e b o t h ±-r e d e xe s . W it h o u t lo s s o f g e n e r a lit y we s u p p o s e t h a t ¿2 is a

s u b t e r m o f ¿1 ( ¿1 ´ ¿1¿2 ) . L e t ¿1¿2 ´ f ( ¹1; :::; ¹j ¿2 ; :::; ¹k ) ; f 2 [M
k ! M]; ti 2 ¤ M ; i =

1 ; :::; k; 1 · j · k. S in c e ¿2 is a ±-r e d e x, t h e n ¹j ¿2 =2 M a n d s in c e ¿1 is a ±-r e d e x, t h e n fr o m
D e ¯ n it io n 2 it fo llo ws t h a t t h e r e e xis t s m 2 M; m 6= ? s u c h t h a t ( ¿1; m ) 2 ±. Th e r e fo r e
¿1 !± m. S in c e ¹j ¿2 =2 M a n d ( ¿1; m ) 2 ±, wh e r e m 6= ?, t h e n fr o m D e ¯ n it io n 2 it fo llo ws
t h a t f ( ¹1; :::; ¹; :::; ¹k ) 2 ± fo r e ve r y ¹ 2 ¤ M . Th e r e fo r e ( f ( ¹1; :::; ¹j ¿02 ; :::; tk ) ; m) 2 ± a n d
¿1¿02 !± m. Th e r e fo r e , t¿1¿2 !± t¿01 ´ tm a n d t¿1¿2 !± t¿1¿ 02 !± tm, wh e r e m 2 Mnf?g a n d
t0 ´ tm.

2 ) ¿1 a n d ¿2 a r e b o t h ¯-r e d e xe s . Fr o m Th e o r e m 2 it fo llo ws t h a t t h e r e e xis t t e r m s
t01; t

0
2 2 ¯ ¡ NF s u c h t h a t t !¯ t1 !!¯ t01 a n d t !¯ t2 !!¯ t02. Th e r e fo r e fr o m Th e o r e m

3 it fo llo ws t h a t t01 ´ t02 ´ t0.
3 ) ¿1 is ±-r e d e x a n d ¿2 is ¯-r e d e x o r ¿1 is ¯-r e d e x a n d ¿2 is ±-r e d e x. W it h o u t lo s e o f

g e n e r a lit y we s u p p o s e t h a t ¿1 is ±-r e d e x a n d ¿2 is ¯-r e d e x. L e t ¿2 ´ ¸x1; :::; xn[¿ [x1; :::
; xn]]( ¹1; :::; ¹n ) , ¿ 2 ¤ ; xi 2 V®i ; ®i 2 T ypes, i = 1 ; :::; n. Th e fo llo win g c a s e s a r e p o s s ib le :

3 .1 ) ¿1 ´ ¿1¿2. It c a n b e s h o wn t h a t ¿1 ! m a n d ¿1¿02 ! m a s s h o wn in c a s e 2 . Th e r e fo r e
t¿1¿2 !± t¿ 01 ´ tm a n d t¿1¿2 !¯ t¿1¿02 !± tm, wh e r e m 2 Mnf?g. Th e r e fo r e t

0 ´ tm.
3 .2 ) ¿2 ´ ¸x1:::xn[¿¿1[x1; :::; xn]]( ¹1; :::; ¹n ) , t h e n it is e a s y t o s e e , t h a t if ¿1[x1; :::; xk] !± ¿ 01

t h e n ¿1[¹1; :::; ¹k] !± ¿ 01 a n d we h a ve :
µ´¸x1:::xn[¿¿1[x1; :::; xn]]( ¹1; :::; ¹n ) !± ¸x1:::xn[¿¿01 [x1; :::; xn]]( ¹1; :::; ¹n ) ´µ1 !¯ ¿¿ 01[¹1; :::; ¹n];
µ ´ ¸x1:::xn[¿¿1[x1; :::; xn]]( ¹1; :::; ¹n ) !¯ ¿¿1 [¹1; :::; ¹n] ´ µ2 !± ¿¿ 01[¹1; :::; ¹n];
Th e r e fo r e t0 ´ t¿¿0

1
[¹1;:::;¹n] s in c e t !± tµ1 !¯ t¿¿0

1
[¹1;:::;¹n] a n d t !¯ tµ2 !± t¿¿ 0

1
[¹1;:::;¹n].

3 .3 ) ¿2 ´ ¸x1:::xn[¿[x1; :::; xn]]( ¹1; :::; ¹i¿i ; :::; ¹n ) . W it h o u t lo s s o f g e n e r a lit y we s u p p o s e
t h a t i = 1 .
µ ´ ¸x1:::xn[¿[x1; :::; xn]]( ¹1¿1; :::; ¹n ) !± ¸x1:::xn[¿ [x1; :::; xn]]( ¹1¿ 01; :::; ¹n )
´ µ1 !¯ ¿ [¹1¿ 0

1
; :::; ¹n] ´ µ0;

µ !¯ ¿ [¹1¿1; :::; ¹n] ´ µ2 !!± µ0;
Th e r e fo r e t !± tµ1 ´ t1 !¯ tµ0, t !¯ tµ2 ´ t2 !!± tµ0 a n d t0 ´ tµ0 .

S in c e t01 !! t1, t01 !! t0 a n d t01 2 ¤ (k1); 1 · k1 · n ¡ 1 , t h e n fr o m t h e in d u c t io n
h yp o t h e s is it fo llo ws t h a t t h e r e e xis t s a t e r m t001 s u c h t h a t t1 !! t001 a n d t0 !! t001. S in c e
t02 !! t2, t02 !! t0 a n d t02 2 ¤ (k2); 1 · k2 · n ¡ 1 , t h e n fr o m t h e in d u c t io n h yp o t h e s is
it fo llo ws t h a t t h e r e e xis t s a t e r m t002 s u c h t h a t t2 !! t002 a n d t0 !! t002 . S in c e t0 !! t001,
t0 !! t002 a n d t0 2 ¤ (k3); 1 · k3 · n ¡ 1 , t h e n fr o m t h e in d u c t io n h yp o t h e s is it fo llo ws
t h a t t h e r e e xis t s a t e r m t00 s u c h t h a t t001 !! t00 a n d t002 !! t00. Th e r e fo r e t1 !! t00 a n d
t2 !! t00.
T heor em 5: There exists a canonical notion of ±-reduction such that ¯±-reduction does not
have Church-R osser property.



D. Grigoryan 8 5

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 = fmin; decg wh e r e
dec 2 [M ! M ]; min 2 [M 2 ! M] a n d fo r e ve r y m; m1; m2 2 M we h a ve :

min( m1; m2 ) =

8
><
>:

m1; if m1; m2 2 N and m1 < m2
m2; if m1; m2 2 N and m1 ¸ m2
?; otherwise

dec( m) =

8
><
>:

0 ; if m = 0
m ¡ 1 ; if m 2 N and m 6= 0
?; otherwise

It is e a s y t o s e e t h a t min a n d dec a r e s t r o n g ly 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 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 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 ? ) . L e t u s c o n s id e r t h e
m a in 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 : ( min( n1; n2 ) ; n1 ) 2 ±; wh e r e n1; n2 2 N a n d n1 < n2

( min( n1; n2 ) ; n2 ) 2 ±; wh e r e n1; n2 2 N a n d n1 ¸ n2

( min( n; ? ) ; ? ) 2 ±; wh e r e n 2 N

( min( ?; n) ; ? ) 2 ±; wh e r e n 2 N

( min( ?; ? ) ; ?) 2 ±

( dec( 0 ) ; 0 ) 2 ±

( dec( n1 ) ; n2 ) 2 ±; wh e r e n1; n2 2 N a n d n1 > 0 ; n2 = n1 ¡ 1

( dec( ? ) ; ? ) 2 ±

L e t u s c o n s id e r t h e n o t io n o f ±-r e d u c t io n ±0.

±0 is : ( min( n1; n2 ) ; n1 ) 2 ±0; wh e r e n1; n2 2 N a n d n1 < n2

( min( n1; n2 ) ; n2 ) 2 ±0; wh e r e n1; n2 2 N a n d n1 ¸ n2

( min( t; ? ) ; ? ) 2 ±0; wh e r e t 2 ¤

( min( ?; t ) ; ? ) 2 ±0; wh e r e t 2 ¤

( dec( 0 ) ; 0 ) 2 ±0

( dec( n1 ) ; n2 ) 2 ±0; wh e r e n1; n2 2 N a n d n1 > 0 ; n2 = n1 ¡ 1

( dec( ? ) ; ? ) 2 ±0

( min( dec( x ) ; x ) ; dec( x ) ) 2 ±0, wh e r e x 2 V



8 6 On Church-Rosser Property of Notion of ¯±-Reduction for Canonical Notion of ±-Reduction

It is e a s y t o s e e t h a t ±0 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 ±0 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 ± ½ ±0, wh ic h is o b vio u s .

L e t u s s h o w t h a t fo r t h e ±0 t h e n o t io n o f ¯±-r e d u c t io n d o e s n o t h a ve Ch u r c h -R o s s e r p r o p -
e r t y. Fo r t h e t e r m t ´ ¸x[min( dec( x ) ; x) ]( dec( y ) ) we h a ve :

¸x[min( dec( x ) ; x) ]( dec( y ) ) !¯ min( dec( dec( y ) ) ; dec( y ) ) 2 NF ;

¸x[min( dec( x ) ; x) ]( dec( y ) ) !±0 ¸x[dec( x ) ]( dec( y ) ) !¯ dec( dec( y ) ) 2 N F ;

L e t t1 ´ min( dec( dec( y ) ) ; dec( y ) ) a n d t2 ´ dec( dec( y ) ) . S in c e t1; t2 2 N F a n d t1 6´ t2,
t h e n t h e r e d o e s n o t e xis t a t e r m t0 s u c h t h a t t1 !! t0 a n d t2 !! t0. Th e r e fo r e , fo r ±0 t h e
n o t io n o f ¯±-r e d u c t io n d o e s n o t h a ve Ch u r c h -R o s s e r p r o p e r t y.

Refer ences

[1 ] S . A . N ig iya n , \ On N o n -c la s s ic a l Th e o r y o f Co 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 .

[2 ] 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 .

[3 ] L .E . B u d a g h ya n , \ Fo r m a liz in g t h e N o t io n o f ±-R e d u c t io n in Mo n o t o n ic Mo d e ls o f Typ e d
¸-Ca lc u lu s , Algebra, Geometry and Their Applications, vo l. 1 , Y S U P r e s s , p p . 4 8 { 5 7 ,
2 0 0 2 .

[4 ] H . B a r e n d r e g t , The L ambda Calculus. Its Syntax and Semantics, N o r t h -H o lla n d P u b -
lis h in g Co m p a n y, 1 9 8 1 .

Submitted 18.06.2018, accepted 28.11.2018.

γÝáÝÇÏ ±-黹áõÏódzÛÇ ·³Õ³÷³ñÇ ¹»åùáõÙ ¯±-黹áõÏódzÛÇ
·³Õ³÷³ñÇ âáñã-èáëë»ñÇ Ñ³ïÏáõÃÛ³Ý Ù³ëÇÝ

¸. ¶ñÇ·áñÛ³Ý

²Ù÷á÷áõÙ

²ß˳ï³ÝùáõÙ ¹Çï³ñÏíáõÙ ¿ ϳÝáÝÇÏ ±-黹áõÏódzÛÇ ·³Õ³÷³ñÁ ïÇåǽ³óí³Í
¸-ûñÙ»ñÇ Ñ³Ù³ñ: îÇåǽ³óí³Í ¸-ûñÙ»ñÁ û·ï³·áñÍáõÙ »Ý ó³Ýϳó³Í ϳñ·Ç ÷á-
÷á˳ϳÝÝ»ñ ¨ ѳëï³ïáõÝÝ»ñ, áñáÝó ϳñ·Á · 1 , áñï»Õ 1 -ÇÝ Ï³ñ·Ç ѳëï³ïáõÝÝ»ñÁ
ѳݹÇë³ÝáõÙ »Ý áõÅ»Õ Ñ³ßí³ñÏ»ÉÇ, ³ñ·áõÙ»ÝïÝ»ñÇ ³Ýáñáß ³ñÅ»ùÝ»ñáí ýáõÝÏódzݻñ:
γÝáÝÇÏ ±-黹áõÏódzÛÇ ·³Õ³÷³ñÁ ³ÛÝ ±-黹áõÏódzÛÇ ·³Õ³÷³ñÝ ¿, áñÝ û·ï³·áñÍíáõÙ
¿ ýáõÝÏóÇáÝ³É Íñ³·ñ³íáñÙ³Ý É»½áõÝ»ñÇ Çñ³Ï³Ý³óÙ³Ý Ù»ç: ²å³óáõóí³Í ¿, áñ ÑÇÙݳ-
Ï³Ý Ï³ÝáÝÇÏ ±-黹áõÏódzÛÇ ·³Õ³÷³ñÇ ¹»åùáõÙ ¯±-黹áõÏódzÛÇ ·³Õ³÷³ñÁ ûÅïí³Í



D. Grigoryan 8 7

¿ âáñã-èáëë»ñÇ Ñ³ïÏáõÃÛ³Ùµ: ²å³óáõóí³Í ¿ ݳ¨, áñ ·áÛáõÃÛáõÝ áõÝÇ Ï³ÝáÝÇÏ ±-
黹áõÏódzÛÇ ·³Õ³÷³ñ, áñÇ ¹»åùáõÙ ¯±-黹áõÏódzÛÇ ·³Õ³÷³ñÁ ûÅïí³Í ã¿ âáñã-
èáëë»ñÇ Ñ³ïÏáõÃÛ³Ùµ:

Î ñâîéñòâå ׸ð÷à-Ðîññåðà ïîíÿòèÿ ¯±-ðåäóêöèè â ñëó÷àå
êàíîíè÷åñêîì ïîíÿòèè ±-ðåäóêöèè

Ä. Ãðèãîðÿí

Àííîòàöèÿ

 äàííîé ðàáîòå ðàññìàòðèâàåòñÿ îñíîâíîå êàíîíè÷åñêîå ïîíÿòèå ±-ðåäóêöèè
äëÿ òèïèçèðîâàííûõ ¸-òåðìîâ. Òèïèçèðîâàííûå ¸ -òåðìû èñïîëüçóþò ïåðåìåí-
íûå ëþáûõ ïîðÿäêîâ è êîíñòàíòû, ïîðÿäîê êîòîðûõ · 1 , ïðè÷åì êîíñòàíòû
ïîðÿäêà 1 ÿâëÿþòñÿ ñèëüíî âû÷èñëèìûìè, ìîíîòîííûìè ôóíêöèÿìè ñ íåîïðåäå-
ëåíûìè çíà÷åíèÿìè àðãóìåíòîâ. Êàíîíè÷åñêîå ïîíÿòèå ±-ðåäóêöèè èñïîëüçóåòñÿ
ïðè ðåàëèçàöèè ôóíêöèîíàëüíûõ ÿçûêîâ ïðîãðàììèðîâàíèÿ. Äîêàçàíà, ÷òî â
ñëó÷àå îñíîâíîãî êàíîíè÷åñêîãî ïîíÿòèÿ ±-ðåäóêöèè ïîíÿòèå ¯±-ðåäóêöèè èìååò
ñâîéñòâî ׸ð÷à-Ðîññåðà. Äîêàçàíà, ÷òî ñóùåñòâóåò êàíîíè÷åñêîå ïîíÿòèå ±-
ðåäóêöèè, â ñëó÷àå êîòîðîãî ïîíÿòèå ¯±-ðåäóêöèè íå èìååò ñâîéñòâî ׸ð÷à-
Ðîññåðà.