AnalyzeReductionLengthsMPCS.DVI


Mathematical Problems of Computer Science 29, 2007, 5{15.

Analysis of B ounds for Lengths of Reductions

in T yped ¸-calculus

Tig r a n M. Ga lo ya n

Institue for Informatics and Automation Problems of NAS of RA

e-mail: tigran.galoyan@gmail.com

Abstract

We analyze bounds for the lengths of arbitrary reduction sequences of terms in
typed ¸-calculus, consider some estimates obtained by the other authors and compare
these estimates. The cut elimination and normalization algorithms are also investigated
in this paper. Thereafter we re¯ne the estimates achieved in [3] (for pure implicational
logic only) by supplement of ´-conversion and then we extend evaluations to ¯rst-order
logic.

Refer ences

[1 ] B a a z , M., L e it s c h , A .: Cu t -E lim in a t io n a n d R e d u n d a n c y-E lim in a t io n b y R e s o lu t io n .
Jo u r n a l o f S ym b o lic Co m p u t a t io n , 2 9 :1 4 9 { 1 7 6 , 2 0 0 0 .

[2 ] B e c km a n n , A ., W e ie r m a n n , A .: A n a lyz in g GÄo d e l's T via e xp a n d e d h e a d r e d u c t io n t r e e s .
Ma t h e m a t ic a l L o g ic s Qu a r t e r ly, 4 6 :5 1 7 { 5 3 6 , 2 0 0 0 .

[3 ] B e c km a n n , A .: E xa c t b o u n d s fo r le n g t h s o f r e d u c t io n s in t yp e d la m b d a -c a lc u lu s . J.
S ym b o lic L o g ic , 6 6 :1 2 7 7 -1 2 8 5 , 2 0 0 1 .

[4 ] Ga lo ya n , T.: S t r o n g n o r m a liz a t io n fo r ¯ r s t -o r d e r lo g ic . Tr a n s a c t io n s o f t h e In s t it u t e fo r
In fo r m a t ic s a n d A u t o m a t io n P r o b le m s o f t h e N A S o f R A . Ma t h e m a t ic a l P r o b le m s o f
Co m p u t e r S c ie n c e 2 8 , p p . 4 5 -5 0 , 2 0 0 7 .

[5 ] K le e n e , S .: In t r o d u c t io n t o Me t a m a t h e m a t ic s . D . va n N o s t r a n d , N e w Y o r k, 1 9 5 2 .

[6 ] S c h wic h t e n b e r g , H .: N o r m a liz a t io n . In F.L . B a u e r , e d it o r , L o g ic , A lg e b r a a n d Co m p u -
t a t io n . P r o c e e d in g s o f t h e In t e r n a t io n a l S u m m e r S c h o o l Ma r kt o b e r d o r f, Ge r m a n y, Ju ly
2 5 - A u g u s t 6 , 1 9 8 9 , S e r ie s F: Co m p u t e r a n d S ys t e m s S c ie n c e s , V o l. 7 9 , p a g e s 2 0 1 -2 3 7 .
N A TO A d va n c e d S t u d y In s t it u t e , S p r in g e r V e r la g , B e r lin , H e id e lb e r g , N e w Y o r k, 1 9 9 1 .

[7 ] S c h wic h t e n b e r g , H .: A n u p p e r b o u n d fo r r e d u c t io n s e qu e n c e s in t h e t yp e d la m b d a -
c a lc u lu s . A r c h ive fo r Ma t h e m a t ic a l L o g ic , 3 0 :4 0 5 -4 0 8 , 1 9 9 1 .

[8 ] S c h wic h t e n b e r g , H .: P r o o f t h e o r y. L e c t u r e n o t e s , Ma t h e m a t is c h e s In s t it u t d e r U n ive r s it Äa t
MÄu n c h e n , Ge r m a n y, 1 9 9 4 .

5



6 Analysis of Bounds for Lengths of Reductions in Typed ¸-calculus

軹áõÏóÇáÝ Ñ³çáñ¹³Ï³ÝáõÃÛáõÝÝ»ñÇ »ñϳñáõÃÛ³Ý ë³ÑÙ³ÝÝ»ñÇ
í»ñÉáõÍáõÃÛáõÝÁ ïÇå³Ï³Ý³óí³Í ¸-ѳßíáõÙ

î. Ø. ¶³ÉáÛ³Ý

²Ù÷á÷áõÙ

²ß˳ï³ÝùáõÙ áõëáõÙݳëÇñíáõÙ »Ý 黹áõÏóÇáÝ Ñ³çáñ¹³Ï³ÝáõÃÛáõÝÝ»ñÇ »ñϳñáõÃ-
Û³Ý ·Ý³Ñ³ï³Ï³ÝÝ»ñÁ ïÇå³Ï³Ý³óí³Í ¸-ѳßíÇ Ã»ñÙ»ñÇ Ñ³Ù³ñ£ ¸Çï³ñÏíáõÙ ¨
ѳٻٳïíáõÙ »Ý ³ÛÉ Ñ»ÕÇݳÏÝ»ñÇ ÏáÕÙÇó ïñí³Í ·Ý³Ñ³ï³Ï³ÝÝ»ñÁ£ Ò¨³÷áËíáõÙ
¿ [3]-áõÙ ïñí³Í ·Ý³Ñ³ï³Ï³ÝÇ ³å³óáõÛóÁ (Ù³ùáõñ ÇÙåÉÇϳóÇáÝ ïñ³Ù³µ³ÝáõÃÛ³Ý
ѳٳñ)ª Áݹ·ñÏ»Éáí ݳ¨ ´-黹áõÏódzÛÇ Ï³ÝáÝÁ£ ²ÛÝáõÑ»ï¨ ëï³óí³Í ³ñ¹ÛáõÝùÁ
ÁݹѳÝñ³óíáõÙ ¿ ³é³çÇÝ Ï³ñ·Ç ïñ³Ù³µ³ÝáõÃÛ³Ý Ñ³Ù³ñ£ ²ß˳ï³Ýùáõ٠ѻﳽáï-
íáõÙ »Ý ݳ¨ Ïñ׳ïÙ³Ý ·áñÍáÕáõÃÛ³Ý ³ñï³ùëÙ³Ý ¨ ÝáñٳɳóÙ³Ý ³É·áñÇÃÙÝ»ñÁ£