Some differences between lambda-calculus and Lisp (2).



; This is the second part of  previous post .
;
;
;
;                4. Evaluation in Lisp vs.
;    reduction to normal form in lambda-calculus
;
;
; As noted in previous post, in Lisp, evaluation of the function
; application is defined recursively:
;
;      1.  evaluation of the function arguments is performed
;      2.  resulting values are assigned to the parameters of
;          the function
;      2.  evaluation of the function body is performed
;
; In lambda calculus, beta-reductions do not recurse on that way.
; There is no "automatic" beta-reductions of the argument of the
; application.
;
; Because of that, in general case, one applies reductions many
; times to achieve similar effect. How many times? Typically,
; until further reduction is impossible; in that case, it is
; said that expression is reduced to normal form.
;
; There are few differences between evaluation in Lisp and
; reduction to normal form in lambda-calculus:
;
;
;              4.1. Order of reductions in
;            lambda-calculus is not defined
;
;
; Lambda-calculus is not an algorithm. It is a "formal system". One
; who performs reductions - human or computer - can pick the order of
; reductions by any criteria.
;
;
;     4.2. Lisp evaluation strategy is not the best for
;                     lambda-calculus
;
;
; In Lisp, order of evaluations is "from inside"; if application
; is evaluated, for example,
;
;          ((lambda(x)(+ x x)) ((lambda(x)(* x x)) 3) 2)
;
; then inner left argument, in this case
;
;                     ((lambda(x)(* x x)) 3)
;
; is evaluated first. That order is called "applicative order".
; In lambda-calculus, some expressions cannot be reduced applying
; that order of reductions. For example,
;
;               ((^x.a) ((^x.(x x)) (^x.(x x))))
;
; would be reduced indefinitely, because reduction of
;
;                   ((^x.(x x)) (^x.(x x)))
;
; doesn't terminate. Some other evaluation strategies, for example,
; "normal order", "from outside", as defined in lambda-Church, terminate:
;
(println ((lambda-Church (x) a) ((lambda-Church(x)(x x))
                                 (lambda-Church(x)(x x)))))
                                 
;        => a
;
;
;
;        4.3. Reduction to normal form is more
;           extensive than single evaluation
;
;
; 1. In Lisp, function, like
;
;              (lambda(x)((lambda(y)y) x)),
;
;    if evaluated is either evaluated to some "compiled value",
;    i.e. it is not S-expression any more - or evaluates to
;    itself, as in Newlisp.
;    
;    In lambda-calculus, reduction is performed inside the function
;    body. For example,
;
;               (^x.((^y.y) x)) => (^x.x).
;
; 2. In Lisp, result of the evaluation of the S-expression is frequently
;    in form that allows further evaluation.
;
;               ((lambda(x)(list '+ 1 2 x)) 3) => '(+ 1 2 3)
;
;But, it is not evaluated automatically.

;
;
; To be continued ...


Some differences between lambda-calculus and Lisp (1).



;                        0. Introduction
;
;
; At the first sight, Lisp dialects appear like extensions of the
; lambda-calculus. Syntax of the two is especially similar. For
; instance,
;
;                          ((^ x . x) y)
;
; in lambda-calculus is very similar to
;
;                         ((lambda(x)x) y)
;
; in Lisp. However, it turns that there are many important
; differences between lambda-calculus and Lisp, some of these
; are obvious, and others are quite subtle. In this post, I'll
; list and comment few of these I've find to be interesting and
; important. The post is not tutorial on lambda-calculus, but
; another view that might be interesting to those who already
; know lambda-calculus, but maybe also - to some extent - to those
; who do not know it yet.
;
;
;
;        1. The notion of lambda-expression
;
;
; There is significant difference even in basic terminology.
; For instance, this is definition of lambda-expression in Common
; Lisp Hyperspec:
;
;    "lambda expression n. a list which can be used in place of a
;     function name in certain contexts to denote a function by
;     directly describing its behavior rather than indirectly by
;     referring to the name of an established function; its name
;     derives from the fact that its first element is the symbol
;     lambda."
;
; In lambda-calculus, lambda-expression is the name used for
; all allowed expressions of lambda-calculus. According to definition,
; lambda expressions are:
;
;       1. variables: a, b, c, d ... a1, a2, ...
;       2. functions: (^ v . F), where v is any variable, F any lambda-expr.
;       3. applications: (E F), where E and F are lambda-expressions.
;
; This difference, although not essential is very confusing one.
;
;
;
;                 2. Evaluation vs. reduction
;
;
; In Lisp, expressions are "evaluated." For instance,
;
;            ((lambda(x)x) y) => value of y.
;
; In lambda-calculus, expressions are "reduced". Reduction
; doesn't require replacement of the variables with values, so
;
;                   ((^ x . x) y) => y
;
; and not
;
;                   ((^ x . x) y) => value of y.
;
; If we remember high school math, some of the exercises were of
; the form "simplify" or "expand", and didn't required knowledge
; about value of the variables to be solved.
;
;           (x+1)^2 -1 ==> (x^2+2x+1) -1 = x(x+2)
;
; Other group of exercises clearly required evaluation:
;
;       "Find the area of the rhomboid with sides
;        a=4, b=3, and angle of 30° between them."
;
;
;
;       3. Recursiveness of evaluation in Lisp
;                                 vs.
;           non-recursiveness of beta-reduction
;                     in lambda-calculus
;
;
; There are three reductions in lambda-calculus; only short
; resume here - formal definition find somewhere else.
;
;     1. Beta-reduction: the application of the function
;  
;                ((^x.x) a) => a,
;                ((^x.(x x)) a) => (a a).
;  
;     2. Alpha-reduction: renaming of the bounded variables
;      
;                (^x.x) => (^y.y).
;      
;     3. Eta-reduction: elimination of the redundant function
;      
;                (^x.((^y.y)x)) => (^y.y).
;      
;        (eta-reduction is not essential; it can be replaced
;         with other two.)
;
; Beta-reduction is very similar to function application
; in Lisp. However, there are significant differences.
;

;
; In Lisp, evaluation of the function application, for instance,
;
;                  ((lambda(x)(x x)) (a b))
;
; is performed on the following way:
;    
;    - argument (here (a b)) is evaluated;
;    - result is assigned to the parameter (here x), and
;    - body of the function, (here (x x)) is evaluated.
;    - the result is returned as the result of  evaluation of
;      whole expression.
;
;
; In lambda-calculus, beta-reduction of the application,
; for instance,
;
;                    ((^x.(x x)) (a b))
;
; is performed on a following way:
;
;     - argument (here (a b)) is substituted for parameter (here x)
;       in the body of the function (here (x x)).
;     - the result of the substitution is result of beta-reduction.
;
; The result of the two is significantly different.
;
;     Note that beta reduction does significantly less than
;     evaluation. Beta-reduction doesn't apply itself recursively
;     on y and on (x x), while evaluation in Lisp does - it requires
;     evaluation of
;
;
;
;      3.1. Example: Church's lambda in Newlisp
;
;
; I'll use previous discussion to define
;
;                        lambda-Church
;    
; in Newlisp, so expressions using it are evaluated just like
; lambda-expressions are beta reduced in lambda-calculus. For
; instance, I want
;
;                   ((lambda-Church (x) (x x)) (a b))
;
; to evalute to
;
;                      ((a b)(a b)).
;
; What should I do? In Newlisp, because it has fexprs, its easy.
; Expression
;
;                     (lambda-Church (x) (x x))
;
; should be evaluated to
;
;               (lambda-macro(x)(expand (quote (x x))
;                                       (quote x)))
;
; and that's all.

(define-macro (lambda-Church head body)
  (let ((var (first head)))
     (expand (lambda-macro(var)(expand (quote body)
                                       (quote var)))
             (quote body)
             (quote var))))

; Let's test it.

(println (lambda-Church (x)(x x)))

;    ==> (lambda-macro (x) (expand (quote (x x)) (quote x)))

(println ((lambda-Church (x)(x x)) (a b)))

;    ==> ((a b) (a b))
;
; It works. In future, lambda-Church expressions can
; be freely mixed with other Newlisp expressions.
;
;
;
; To be  continued  ...
;


---

Find Your Way Through Lisp Labyrinth.



The programmer who wants to start using Lisp -- not because of practical reasons, but because he is intrigued with language itself -- is frequently in doubt where to start. I made one proposal he might follow; that proposal reflects my values - other Lisp users might make different proposals. I'd like to hear your comments.




If you like this post, you might be interested in

 When were the best days for Lisp 

Why they say this is the most important metacircular blog post?

What? Why they say this is the most important metacircular blog post? I have not the slightest clue. Let us ask Google!

When Were The Best Days for Lisp?


Another question that can be answered by some Google graphs.
According to Google Ngrams, for Lisp (whole family) in late 1980's;
for Scheme alone quite a bit later.
I'm surprised that the loss of the popularity is so great.

Google ngram


if you like this post, you might be interested in following posts:

  Why you do not use Lisp? The results of the poll.  

  Relative popularity of Lisp dialects.  

Relative Popularity of Lisp Dialects and Some Trends, According to Google.




Relative Popularity of Lisp Dialects and Some Trends, According to Google

Kazimir Majorinc
kazimir at chem pmf hr



Following graphs show relative popularity of some Lisp dialects, according to Google, on the base of counting Google searches. I had to play for some time to find suitable graphs; some of the programming languages have names related to other notions as well - and it includes generic Lisp and Scheme, but also popular Java, while C++ contains unacceptable characters. Cobol and Fortran are useful, because C# alone is so popular than it cannot be compared directly with any Lisp dialect. Also, Cobol and Fortran are about as old as Lisp .

Although all these programming languages -- except Clojure and perhaps Picolisp -- appear to lose popularity, note that popularity is relative to the total number of Google searches, so graph is influenced by increasing ratio of non-programmers vs. programmers among Google users. However, the comparison between different programming languages and dialects should be still valid.

These graphs should be "alive" when you click; it doesn't always work, but usually it does.

Make your own conclusions!





If you like this post, maybe you'll like  Another difference between C++ and C#  or  Why you do not use Lisp - the results of the poll .



--

Lambda Calculus Interpreter (2).






Use of "reduce^" from Newlisp REPL


(setf [println.supressed] true [print.supressed] true)
(load "http://instprog.com/Instprog.default-library.lsp" )
(setf [println.supressed] nil [print.supressed] nil)

;---------------------------------------------------------------
; Interpreter for lambda-calculus, described in recent posts is now
; integrated in my library for Newlisp, as function "reduce^".
;
; Here is example demonstrating how it works. If you want to see
; implementatition details, check the library. Check the previous
; posts also.

(println  (reduce^ '((^ x . (x (x x))) (^ y . (y (y y)))) ;lambda-expression

                        10   ;maximal number of reductions,
                             ;useful for non-terminating lambda-expressions

                        true ;true if you want reduction steps are printed on screen
                             ;nil if you want "silent" interpretation
                        ))
                      
(println  (reduce^ '((^ x . x) (^ x . x))

                        10   
                        
                        true
                        
                        ))

(println (reduce^ '((^ x . (x x)) (^ x . (x x)))
                   
                        10
                        
                        true
                        ))

               
(exit)

; OUTPUT:
;
;   1. ==[ start ]==> ((^x.(x (x x)))(^y.(y (y y))))
;   2. ==[ beta  ]==> ((^y.(y (y y)))((^y.(y (y y)))(^y.(y (y y)))))
;   3. ==[ alpha ]==> ((^x.(x (x x)))((^y.(y (y y)))(^z.(z (z z)))))
; ...
;
;      UNREDUCED: maximal number of reductions reached.
;
; (unreduced ((((^ y . (y (y y))) ((^ y . (y (y y))) (^ y . (y (y y))))) (((^ z . (
;        z
;        (z z)))
;      (^ x1 . (x1 (x1 x1))))
;     ((^ y1 . (y1 (y1 y1))) (^ z1 . (z1 (z1 z1))))))
;   (((^ x2 . (x2 (x2 x2))) (^ y2 . (y2 (y2 y2)))) ((^ z2 . (z2 (z2 z2))) (^ x3 . (
;       x3
;       (x3 x3)))))) 10)
;
;   1. ==[ start ]==> ((^x.x)(^x.x))
;   2. ==[ alpha ]==> ((^x.x)(^y.y))
;   3. ==[ beta  ]==> (^y.y)
;   4. ==[ alpha ]==> (^x.x)
;
;      REDUCED to normal form.
;
; (reduced (^ x . x) 4)
;
;   1. ==[ start ]==> ((^x.(x x))(^x.(x x)))
;   2. ==[ alpha ]==> ((^x.(x x))(^y.(y y)))
;   3. ==[ beta  ]==> ((^y.(y y))(^y.(y y)))
;   4. ==[ alpha ]==> ((^x.(x x))(^y.(y y)))
;
;      IRREDUCIBLE: cycle.
;
; (irreducible ((^ x . (x x)) (^ y . (y y))) 4)
;
;
;



If you like this post, you'll probably like


 Almost two hundred thousand reduced lambda-expressions. 


--

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.


--

Enumeration of Lambda-Expressions.



(setf [println.supressed] true [print.supressed] true)
(load "http://instprog.com//Instprog.default-library.lsp")
(setf [println.supressed] nil [print.supressed] nil)

; The lambda-expressions are defined on following way:
;
; (a) a, b, c, ... are lambda-expressions. These lambda expressions
;     are named "variables".
;
; (b) if X is variable and E is lambda-expression, then
;
;                            (^ X . E)
;
;     is lambda-expression as well. These lambda-expressions are
;     named "functions".
;
; (c) if E and F are lambda-expressions, then (E F) is lambda-
;     expression as well. These lambda expressions are named
;     "applications."
;
; Using functions for Cantor's enumeration developed in last few
; posts, now in my library, I'll define functions for enumeration
; of all lambda-expressions, i.e. bijective function
;
;                    lam: N -> all lambda-exprsions
;
; Enumerations of variables, functions, and applications will be
; defined independently.
;
;       var1, var2, ..., varn, ...
;       fun1, fun2, ..., funn, ...
;       app1, app2, ..., appn, ...
;
; After that, all lambda expressions will be enumerated on following
; way:
;
;       var1, fun1, app1, var2, fun2, app2, ...
;
;---------------------------------------------------------------
;
; First - enumeration of variables; and inverse enumeration.
;
; If alphabet is, for example, "xyz", I'll enumerate variables
; on following way:
;
;       x, y, z, x1, y1, z1, x2, y2, z2 ...
;
; It slightly complicates enumeration, but it looks better than
;
;       x0, y0, z0, x1, y1, ...

(setf var (lambda(n alphabet)
             (letn((l (length alphabet))
                   (first-char (alphabet (% (- n 1) l)))
                   (rest-chars (let((n1 (/ (- n 1) l)))
                               (if (= n1 0) "" (string n1)))))
                  (sym (append first-char rest-chars)))))
                                   
(setf var-inverse (lambda(v alphabet)
                     (letn((l (length alphabet))
                           (first-char (first (string v)))
                           (rest-chars (rest (string v))))
                          (when (= rest-chars "")
                                (setf rest-chars "0"))
                          (+ (* (int rest-chars) l)
                             (find first-char alphabet) 1))))
;
;---------------------------------------------------------------
;
; Second, enumeration of functions - and inverse enumeration.
;
; Every function has form (^ <var> <lambda-expression>), where
; any variable and lambda-expression is allowed. All pairs of
; variables and lambda-expressions can be enumerated using
; Cantor's enumeration:

(setf fun (lambda(n alphabet)
             (list '^
                   (var (cantors-row n) alphabet)
                   '.
                   (lam (cantors-column n) alphabet))))
                        
(setf fun-inverse
  (lambda(f alphabet)
     (cantors-enumeration-inverse (var-inverse (f 1) alphabet)
                                  (lam-inverse (f 3) alphabet))))
;
;---------------------------------------------------------------
;
; Third, enumeration of applications - and inverse enumeration.
;
; Every application has form (<lambda-expression1> <lambda-expression2>),
; For enumeration of pairs of lambda-expressions, we need Cantors
; enumeration again.

(setf app (lambda(n alphabet)
            (list (lam (cantors-row n) alphabet)
                  (lam (cantors-column n) alphabet))))
                  
(setf app-inverse
  (lambda(a alphabet)
    (cantors-enumeration-inverse (lam-inverse (first a) alphabet)
                                 (lam-inverse (last a) alphabet))))

;
;---------------------------------------------------------------
;
; Finally, enumeration of lambda expressions - and inverse enumeration:

(setf lam (lambda(n alphabet)
            (letn((n1 (- n 1))
                  (row (+ (% n1 3) 1))
                  (column (+ (/ n1 3) 1)))

              (case row (1 (var column alphabet))
                        (2 (fun column alphabet))
                        (3 (app column alphabet))))))

; For lam-inverse, I need few helper predicates:

(setf var? (lambda(l)(symbol? l)))   
(setf fun? (lambda(l)(and (list? l) (= (length l) 4))))
(setf app? (lambda(l)(and (list? l) (= (length l) 2))))

(setf lam-inverse
      (lambda(l alphabet)
         (local(row column)
           (cond ((var? l)(setf row 1)
                          (setf column (var-inverse l alphabet)))
                 ((fun? l)(setf row 2)
                          (setf column (fun-inverse l alphabet)))
                 ((app? l)(setf row 3)
                          (setf column (app-inverse l alphabet))))
            (+ (* 3 (- column 1)) row))))

;---------------------------------------------------------------
;
;                          TEST

(for(i1 1 10)
  (letn((i2 (lam i1 "xyz"))
       (i3 (lam-inverse i2 "xyz")))
       (println i1 " -> " i2 " => " i3)))

; Here is output - ten nice lambda expressions

; 1 -> x => 1
; 2 -> (^ x . x) => 2
; 3 -> (x x) => 3
; 4 -> y => 4
; 5 -> (^ x . (^ x . x)) => 5
; 6 -> (x (^ x . x)) => 6
; 7 -> z => 7
; 8 -> (^ y . x) => 8
; 9 -> ((^ x . x) x) => 9
; 10 -> x1 => 10
;
; In case you like these, here is one million lambda-expressions.
;
;
; (set 'out-file (open "C://lambda-expressions.txt" "write"))
; (for(i1 1 1000000)
;   (letn((i2 (lam i1 "xyz"))
;         (i3 (append (string i1) ".  " (string i2))))
;        (write-line out-file i3)))
; (close out-file)
;

(exit)

Cantor's Enumerations (3)



; Grand finale of these few posts on Cantor's enumerations is
; enumeration of all finite sequences of natural numbers - including
; singles. Same Cantor's trick, but this time on more abstract
; level, can be used:
;
;    a11, a12, .... is enumerated list of all singles
;    a21, a22, .... is enumerated list of all pairs
;    a31, a32, .... is enumerated list of all triplets
;    ...
;    
; It doesn't matter that aij's are the result of the Cantor's enumeration;
; Same Cantor's enumeration can be applied again:
;    a11, a12, a21, a31, a22, a32 ...
;
; After such enumeration, all finite sequences will be on our list, enumerated.
;
; What might be the next step - enumerating all infinite sequences?
; Unfortunately, it is impossible.
;
; If you want to run this post as program, you need to cut and paste
; previous two posts on the beginning. Alternatively, you can simply
; read the posts and believe me about results.

(println)

(define cantors-enumeration-finite
        (lambda(n)
          (cantors-enumeration (cantors-row n) (cantors-column n))))
          
(define cantors-enumeration-finite-inverse
        (lambda()
          (let((arguments (args)))
            (cantors-enumeration-inverse (length arguments)
                                         (apply cantors-enumeration-inverse arguments)))))
                                         
; Test

(for(i1 1 45)
  (letn((i2 (cantors-enumeration-finite i1))
        (i3 (apply cantors-enumeration-finite-inverse i2)))
        (println (format "%2d" i1) " -> " i2 " -> " (format "%2d" i3))))

; The result is pretty:
        
 1 -> (1) ->  1
 2 -> (2) ->  2
 3 -> (1 1) ->  3
 4 -> (3) ->  4
 5 -> (1 2) ->  5
 6 -> (1 1 1) ->  6
 7 -> (4) ->  7
 8 -> (2 1) ->  8
 9 -> (1 1 2) ->  9
10 -> (1 1 1 1) -> 10
11 -> (5) -> 11
12 -> (1 3) -> 12
13 -> (2 1 1) -> 13
14 -> (1 1 1 2) -> 14
15 -> (1 1 1 1 1) -> 15
16 -> (6) -> 16
17 -> (2 2) -> 17
18 -> (1 2 1) -> 18
19 -> (2 1 1 1) -> 19
20 -> (1 1 1 1 2) -> 20
21 -> (1 1 1 1 1 1) -> 21
22 -> (7) -> 22
23 -> (3 1) -> 23
24 -> (2 1 2) -> 24
25 -> (1 2 1 1) -> 25
26 -> (2 1 1 1 1) -> 26
27 -> (1 1 1 1 1 2) -> 27
28 -> (1 1 1 1 1 1 1) -> 28
29 -> (8) -> 29
30 -> (1 4) -> 30
31 -> (3 1 1) -> 31
32 -> (2 1 1 2) -> 32
33 -> (1 2 1 1 1) -> 33
34 -> (2 1 1 1 1 1) -> 34
35 -> (1 1 1 1 1 1 2) -> 35
36 -> (1 1 1 1 1 1 1 1) -> 36
37 -> (9) -> 37
38 -> (2 3) -> 38
39 -> (1 1 3) -> 39
40 -> (3 1 1 1) -> 40
41 -> (2 1 1 1 2) -> 41
42 -> (1 2 1 1 1 1) -> 42
43 -> (2 1 1 1 1 1 1) -> 43
44 -> (1 1 1 1 1 1 1 2) -> 44
45 -> (1 1 1 1 1 1 1 1 1) -> 45