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.


--

2 comments:

  1. Hello, I'm currently learning the lambda-calculus and found your example very helpful. However the large text files appear missing. Will they be fixed soon?

    ReplyDelete
    Replies
    1. I'm glad you like it, Shaun. The files are just moved on http://kazimirmajorinc.com, currently under the "Programs".

      Delete