199019 Reduced Lambda-Expressions.

; The function that enumerates all lambda-expressions and the ; functions that perform few well known reductions of lambda- ; expressions are described in last posts. Recently, I wrote ; the program that generates and attempts to reduce all lambda- ; expressions to normal. ; ; Lambda expressions are enumerated and generated using Cantor's style ; enumeration of all lambda-expressions described in previous posts. ; However, some lambda expressions generated that way are obviously ; redundant. For example, ; ;                           ((^a.a) b) ;                       ; and ;                           ((^b.b) a) ;                  ; differ only in names of variables. To avoid such redundancies, ; program attempted to reduce only lambda expressions such that ; variables occur in alphabetical order, i.e. ((^a.a) b), but ; not ((^a.a) c) or ((^b.b) a). Program is left to work long ; enough so ; ;    23 969 511 lambda-expressions are generated ; ;       200 000 of these were non-redundant in just defined sense, and ;               attempts for reduction of these lambda-expressions ;               to normal form is done. ;        ;       199 019 lambda-expressions are successefully reduced to ;               normal form, ;        ;           934 lambda-expressions are proven irreducible, because ;               cycle is discovered and ;            ;            47 lambda-expressions are not reduced: in 35 reductions ;               normal form wasn't reached, but cycle wasn't discovered ;               either. It appears that almost all of these ;               lambda-expressions grow infinitely. ; ; Standard lambda-reductions are used: ; ;    alpha reduction :  (^ x . x) <-> (^ y . y), i.e. bounded ;                       variables can be freely renamed. ;     ;    eta reduction:     (^ x . (F x)) -> F i.e. elimination of ;                       redundant function definition ; ;    beta reduction:    ((^ x . F) G) -> F[x:=G], i.e. substitution ;                       of G for x in F. Beta reduction is not defined ;                       if G contains x as free variable.   ; ; The reduction algorithm uses normal order of evaluation (i.e. ; like Lisp fexprs and Haskell functions), which is known to be ; superior to applicative order of evaluation (like functions in ; Lisp and in almost all other programming languages.) ; ; The program performs alpha-conversion after each reduction. Bounded ; variables are renamed to ; ;              x, y, z, x1, y1, z1, x2, ... ; ; The algorithm attempts to make eta-reduction before beta reduction.                         ; Although eta-reduction is prefered, it was done only 3047 times ; total, while beta-reduction is performed 304254 times, i.e. 100 ; times more frequently. ; ; Here is one of them: ; ;   ------  8167/277305. ------   ; ;   1. ==[ start ]==> ((^a.(a (a a)))((^a.(a a))(^a.a))) ;   2. ==[ alpha ]==> ((^x.(x (x x)))((^y.(y y))(^z.z))) ;   3. ==[ beta  ]==> (((^y.(y y))(^z.z))(((^y.(y y))(^z.z))((^y.(y y))(^z.z)))) ;   4. ==[ alpha ]==> (((^x.(x x))(^y.y))(((^z.(z z))(^x1.x1))((^y1.(y1 y1))(^z1.z1)))) ;   5. ==[ beta  ]==> (((^y.y)(^y.y))(((^z.(z z))(^x1.x1))((^y1.(y1 y1))(^z1.z1)))) ;   6. ==[ alpha ]==> (((^x.x)(^y.y))(((^z.(z z))(^x1.x1))((^y1.(y1 y1))(^z1.z1)))) ;   7. ==[ beta  ]==> ((^y.y)(((^z.(z z))(^x1.x1))((^y1.(y1 y1))(^z1.z1)))) ;   8. ==[ alpha ]==> ((^x.x)(((^y.(y y))(^z.z))((^x1.(x1 x1))(^y1.y1)))) ;   9. ==[ beta  ]==> (((^y.(y y))(^z.z))((^x1.(x1 x1))(^y1.y1))) ;  10. ==[ alpha ]==> (((^x.(x x))(^y.y))((^z.(z z))(^x1.x1))) ;  11. ==[ beta  ]==> (((^y.y)(^y.y))((^z.(z z))(^x1.x1))) ;  12. ==[ alpha ]==> (((^x.x)(^y.y))((^z.(z z))(^x1.x1))) ;  13. ==[ beta  ]==> ((^y.y)((^z.(z z))(^x1.x1))) ;  14. ==[ alpha ]==> ((^x.x)((^y.(y y))(^z.z))) ;  15. ==[ beta  ]==> ((^y.(y y))(^z.z)) ;  16. ==[ alpha ]==> ((^x.(x x))(^y.y)) ;  17. ==[ beta  ]==> ((^y.y)(^y.y)) ;  18. ==[ alpha ]==> ((^x.x)(^y.y)) ;  19. ==[ beta  ]==> (^y.y) ;  20. ==[ alpha ]==> (^x.x) ; ;      REDUCED to normal form. ; ; For others, go to ; ;      Reduced lambda-expressions       1 -  25 000  ;      Reduced lambda-expressions  25 001 -  50 000  ;      Reduced lambda-expressions  50 001 -  75 000  ;      Reduced lambda-expressions  75 001 - 100 000  ;      Reduced lambda-expressions 100 001 - 125 000  ;      Reduced lambda-expressions 125 001 - 150 000  ;      Reduced lambda-expressions 150 001 - 175 000  ;      Reduced lambda-expressions 175 001 - 200 000  ; ; Alternatively, 200 000 of reduced lambda expressions in one large text file: ; ;      200 000 Reduced lambda-expressions  ; ; Warning: that file is large: 60 MB.

--