Kazimir Majorinc's Lisp Programming Blog.

Gödel Numbers of Symbolic Expressions and Missing Missing Element.

2011-12-28T18:52:00.018+01:00

Gödel Numbers of Symbolic Expressions and Missing Missing Element

Kazimir Majorinc
kazimir at chem pmf hr

0. Introduction

Austrian mathematician Kurt Gödel is known for his theorem on 'incompleteness' of the formal arithmetics expressed in the first order predicate calculus. In proof of the theorem, Gödel defined encoding of logical expressions into natural numbers that allowedhim to express sentences about formal arithmetics as sentences of formal arithmetics.

Symbolic expressions are similar to logical expressions. It is not surprise, since symbolic expressions are designed explicitly to represent logical expressions in McCarthy's program Advice Taker. In this post,Gödel's encoding based on products of prime numbers is applied on symbolic expressions. That particular encoding is slightly simpler than original, due to convenient reasoning about symbolic expressions as lists. It is discussed how to redefine symbolic expressions so described gödelization is bijection, i.e. not only every symbolic expression has its code, but also every natural number is code of some symbolic expression.

1. Gödel's encoding of logical formulas

Natural numbers are assigned to all "primitive sings" allowed in logical formulas: 11 is assigned to left parenthesis, 13 is assigned to right parenthesis, 7 is assigned to logical connective ∨. Prime numbers larger than thirteen: 17, 19, 23, ... are assigned to variables x₁, y₁, z₁, ... Logical formulas, as sequences of "primitive signs," are associated to sequences of natural numbers. For instance, (x₁∨x₂) is associated to sequence 11, 17, 7, 19, 13. The sequences of natural numbers are associated to single natural numbers using elements of sequence as exponents of prime numbers. For instance, 11, 17, 7, 19, 13 is associated to

2¹¹·3¹⁷·5⁷·7¹⁹·11¹³ = 8131093970737510569553529892960700268640000000.

Hence, all logical formulas are associated to natural numbers. Furthermore, different logical formulas are associated to different numbers.

2. Gödel numbers of symbolic expressions

Gödel numbers can be assigned to symbolic expressions without encoding of individual characters as parentheses.

Symbols. Let us assume that symbols are only atoms in symbolic expressions, and that symbols consist only of small letters. These restrictions are not essential. Then, all symbols can be ordered first in groups of the same lengths; inside groups by alphabetical order. Such sequence would look like

a, b, c, ..., z, aa, ab, ac, ..., zz, aaa, ...

Then, these symbols are enumerated with prime numbers; a → 3, b → 5, c → 7, ...

Non-atomic symbolic expressions. If e₁, ..., e_n, n ≥ 0 are symbolic expressions with respective Gödel numbers g1, ..., gn then symbolic expression (e₁ ... e_n) is encoded to

2^g1·3^g2·... ·p_n^gn,

where p_n is n-th prime number. Specially, () is encoded to 1, (()) is encoded to 2 etc. Different symbolic expressions are encoded to different natural numbers. For each natural number that is Gödel number of some symbolic expression, original symbolic expression can be reconstructed. IfGödel number is prime number, then it is code of some symbol. If it is not prime number, then it can be represented as product of the form 2^g1·3^g2·... ·p_n^gn, hence it is code of (e₁ ... e_n), where e₁, ..., e_n are reconstructed from Gödel numbers g1, ..., gn.

For instance, Gödel number of(a b) is 2³·3⁵ = 1944.

3. Redefining symbolic expressions

Described encoding is simple and natural. However, it is not bijection. Some natural numbers are not codes of any symbolic expressions. For instance, 27 = 2⁰·3³ cannot be code of any symbolic expression, because there is no symbolic expression such that its code is 0. Let us introduce new symbolic expression, denoted with _ such that its Gödel number is 0. Then, Gödel number of (_ a) is exactly 2⁰·3³ = 27. As every natural number can be presented as product

2^g1·3^g2·... ·p_n^gn,

where p_n is n-th prime number, g1, g2, ..., gn ≥ 0, then every natural number is code of some symbolic expression.

Unfortunately, with such definition, Gödel numbers are not unique any more. There are two problems; it appears neither one is essential.

First, symbolic expression _ on the end of list does not influence encoding. Gödel numbers of all symbolic expressions (_ a),(_ a _),(_ a _ _) ... are

2⁰·3³ = 2⁰·3³ ·5⁰ = 2⁰·3³·5⁰·7⁰ = ... = 27.

However, there is an interpretation of _ that allows natural identification of these symbolic expressions:_ could denote that element is "missing." For instance, symbolic expression(_ a) doesn't have first element, just second one;_ on the end of the symbolic expressions is irrelevant. Implementation of symbolic expressions as maps, as in important experimental Lisp dialect MISC, developed by Will Thimbleby might be suitable.

Second, Gödel numbers of symbolsa,b, ... are same as Gödel numbers ofsymbolic expressions

(_ ()), (_ _ ()), ...

That problem is avoided if symbols are seen as shortens of respective symbolic expressions, like'x is shorten for (quote x) in many Lisp dialects.

References

Gödel, K., "On formally undecidable propositions of Principia Mathematica and related Systems I", in S. Feferman, Kurt Gödel, Collected Works, Vol. I., Oxford University Press, 1986, pp. 145-95.
McCarthy, J., Programs with Common Sense, In Proceedings of the Teddington Conference on the Mechanization of Thought Processes, London, Her Majesty's Stationery Office, 1959, pp. 756-91.
Thimbleby, W., MISC, retrieved 28 December 2011.

Automated theorem finding in propositional calculus

2011-11-20T01:09:00.024+01:00

Automated Theorem Finding in Propositional Calculus

Kazimir Majorinc
kazimir at chem pmf hr

0. Introduction

Automated theorem finding is, according to Larry Wos, one of the basic research problems of automated reasoning. Its objective is search for new, interesting or important mathematical theorems, in contrast to more popular automated theorem proving, i.e. search for proofs of given theorems. See, for instance, Simon Colton's and Alex Bundy's survey of previous work.

Propositional calculus is important formal theory. However, individual theorems are of little interest for mathematicians; the theorems are too simple and it is too easy to find proofs. Maybe that is the reason that propositional calculus didn't inspired many attempts for automated theorem finding. Hao Wang's article "Toward mechanical mathematics" appears to be sole published description of the experiment with automated theorem finding in propositional calculus. Wang's Program II. generated formulas of propositional sequent calculus. Generated sequents were equivalent to propositional formulas (F → G),(not (F and G)),(F or G) in notation used in this post. The formulas F and G had exactly six symbols (variables and operators.) The sequents that could be obtained by variables renaming and the sequents such that at least one of the formulas F and G is theorem were excluded as trivial. Nearly half million of the formulas satisfied these criteria; roughly 1/14 of these were theorems. Wang concluded that "the result was disappointing in so far as too few theorems were excluded as being trivial, because the principles of triviality actually included in the program were too crude."

Two programs for automated theorem finding in propositional calculus are presented in this blog post. The first one implements arguably simplest possible, brute force algorithm for derivation of theorems from axioms. The second program has few improvements. Both programs, and the results of their executions: one hundred thousand of theorems and proofs for each are attached.

1. Axioms

Definitions of the basic notions of propositional calculus (variables, well formed formulas etc.) are omitted in this post. It is assumed that reader is already familiar with these or he is able to understand post without such formal introduction. Used system of axioms is variation of standard L₄ system from Elliott Mendelson's classical textbook.

(A → (B → A))
((A → (B → C)) → ((A → B) → (A → C)))
((A and B) → A)
((A and B) → B)
(A → (B → (A and B)))
(A → (A or B))
(B → (A or B))
((A → B) → ((B → C) → ((A or B) → C)))
((A → B) → ((A → (not B)) → (not A)))
((not (not A)) → A)

Originally, these are schemes of axioms: each formula represents infinite family of axioms obtained by substitution of formulas for A, B, C. Here, these formulas are individual axioms.

2. Rules of inference

Usual rules of inference are modus ponens and substitution.

Modus ponens or detachment. If F and(F →G) are theorems of propositional calculus, where F and G are propositional formulas then G is the theorem of propositional calculus. For instance, (A → A) and ((A → A) → (B → (A → A))) are theorems of propositional calculus. By modus ponens, the formula(B → (A → A)) is also theorem of propositional calculus. The formulas F and(F →G) are called premise minor and premise major respectively.

Substitution. If F is a theorem of propositional calculus, A₁,..., A_n are variables and F₁, ..., F_n are formulas of propositional calculus then formula F(F₁/A₁, ...,F_n/A_n) obtained by simultaneous substitution of F₁ for A₁, ..., F_n for A_n in F is also the theorem of propositional calculus. For instance, (A → A) is a theorem of propositional calculus; by substitution of (A → B) for A, the formula ((A → B) → (A → B)) is also theorem of propositional calculus.

Substitution can be applied on any theorem and used for derivation of infinitely many theorems. All theorems derived by substitution are less interesting than original one, however, they can be used in some application of modus ponens. Because of that, these two rules are integrated in one, more suitable for automated theorem finding.

Combined rule. If F and (G → H) are theorems of propositional calculus, where F, G and H are formulas of propositional calculus and there is a substitution u, such that u is unification ofF and G, i.e. u(F) = u(G), then u(H) is also theorem of the propositional calculus. Without loss of generality it is required that u(H) is in canonic form, i.e. the variables occur in alphabetical order. For instance, the formula((B → (A → B)) is not in canonic form and the formula ((A → (B → A)) is in canonic form.

3. Program 1.

The theorems of propositional calculus are derived sequentially.

Theorems T₁, T₂, ..., T₁₀ are axioms.
Theorems T₁₁, T₁₂, ... are derived by single application of the combined rule on pairs of thorems (T_i, T_j), i, j = 1, 2, ... by order of Cantor's enumeration: (T₁, T₁), (T₂, T₁), (T₂, T₂), (T₁, T₂) ...

The algorithm is arguably the simplest possible algorithm for automated theorem finding in propositional calculus. It is complete: all theorems of the propositional calculus (in canonic form) will occur at some place in infinite sequence. It can be said even more: all theorems will occur infinitely many times in that sequence: if F is a theorem, then for every theoremG, formula (G →F) is also theorem and F can be derived from these two. However, duplicates can be simply omitted from the sequence of theorems.

The algorithm is implemented in newLISP dialect of Lisp. Propositional formulas are naturally represented as Lisp symbolic expressions and some frequently needed operations, like unification, are supported.

The program is executed until first 100 000 theorems are derived. Application of the combined rule is attempted 1 127 490 times. Application of combined rule failed in 50% of attempts because premise major wasn't implication. In 34% of attempts unification of antecedent in premise major and premise minor wasn't possible. In 16% of attempts unification succeeded and conclusion is developed. In 7% of attempts, conclusion was already derived earlier during executions of the program. In 9% of all attempts, conclusion was previously unknown.

Following table contains the list of all theorems of the size (defined as number of operator and variable occurrences) five or less derived by program, with some related data.

	i	T_i	d(T_i)	\|T_i\|	\|proof(T_i)\|	\|\|proof(T_i)\|\|	c(T_i)
1	86	(A → A)	410	3	33	5	3.21
2	1	(A → (B → A))	1679	5	5	1	1.38
3	3	((A and B) → A)	1679	5	5	1	1.38
4	4	((A and B) → B)	1679	5	5	1	1.38
5	6	(A → (A or B))	1678	5	5	1	1.38
6	7	(A → (B or A))	1678	5	5	1	1.38
7	10	((not (not A)) → A)	1074	5	5	1	1.38
8	1190	(not (A and (not A)))	1	5	37	5	2.06
9	1210	(not ((not A) and A))	1	5	37	5	2.06
10	2222	(A → (A and A))	2	5	67	9	2.32
11	2230	(A or (B → B))	1	5	43	7	2.12
12	2231	((A → A) or B)	1	5	43	7	2.12
13	2234	(A → (B → B))	3	5	43	7	2.12

The data in columns of the table are:

i	ordinal number of derived theorem,
T_i	theorem,
d(T_i)	number of times the theorem is derived during execution of the program,
\|T_i\|	size of the theorem, defined as number of operators and variables,
\|proof(T_i)\|	size of the proof, defined as sum of the sizes of the theorems in proof, including derived theorem,
\|\|proof(T_i)\|\|	number of steps in proof of the theorem (1 for axioms) and
c(T_i)	coefficient defined with \|T_i\|^c(T_i) = \|proof(T_i)\|.

Coefficient c(T_i) is attempt for quantification of the intuition that interesting theorems are "deep" theorems, i.e. short theorems with long proofs.

For instance, the shortest theorem of propositional calculus, (A → A)is derived as 86. theorem; the proof is printed out in following form:

tm-2.   ((A → (B → C)) → ((A → B) → (A → C))), axiom
 tm-1.   (A → (B → A)), axiom
 tm-12.  ((A → B) → (A → A)), M:tm-2, m:tm-1
 tm-86.  (A → A), M:tm-12, m:tm-11

Premise major and premise minor used in proving each steps are denoted with M and m respectively. Notation tm- is used for internal representation of theorem in program; for this particular algorithm, indexes are same. Original output of the program contains respective unifications as well.

Some disadvantages of the Program 1. are obvious. Some of derived theorems are instances of the already derived theorems. For example, theorem 89.,((A → B) → (A → B)) is an instance of the theorem 86. The algorithm doesn't prefer short theorems, although it appears that shorter theorems are of greater interest, from perspective of human reader and, perhaps, from computational complexity perspective.

Fig 1. Size of the theorems derived by Program 1.

Attachments

4. Program 2.

Described algorithm can be improved by rejection of instances and addition of preference for a shorter theorems, i.e. standard "best first" strategy.

Theorems T₁, T₂, ..., T₁₀ are the axioms of propositional calculus.
Theorem T_n+1 is the first theorem such that
1. it can be derived by single application of the combined rule on pairs of theorems T₁, T₂, ..., T_n,
2. it is not an instance of any of these theorems, and
3. there is no shorter theorem satisfying conditions a. and b.
for n = 11, 12, ... The theorems are derived by single application of the combined rule on the pairs of the theorems, ordered by Cantor's enumeration.

The program is developed in newLISP and executed for nearly two weeks onfew years old personal computer. Application of the combined rule is attempted 10 000 000 001 times. It failed in 51% of attempts because premise major wasn't implication. In 23% of attempts unification of antecendent in premise major and premise minor wasn't possible. In 26% of attempts unification succeeded and conclusion is developed. In 13% of attempts, conclusion was too long to be added to the theory in any reasonable time; it is unknown how many duplicates were among these. Nearly 13% attempts resulted in duplication of already derived theorems. Finally, 0.0065% attempts were successeful and 0.001% attempts resulted with 100 001 shortest theorems.

Following table contains the list of all theorems of the size (defined as number of operator and variable occurences) less or equal to five, derived by program, with some related data.

	i	T_i	d(T_i)	\|T_i\|	\|proof(T_i)\|	\|\|proof(T_i)\|\|	c(T_i)
1	13	(A → A)	431576	3	33	5	3.207534
2	38384	((not A) or A)	173362	4	468	57	4.651162
3	38385	(A or (not A))	173362	4	416	51	4.516202
4	1	(A → (B → A))	154928	5	5	1	1.37973
5	3	((A and B) → A)	150188	5	5	1	1.37973
6	4	((A and B) → B)	150188	5	5	1	1.37973
7	6	(A → (A or B))	150630	5	5	1	1.37973
8	7	(A → (B or A))	150630	5	5	1	1.37973
9	10	((not (not A)) → A)	149718	5	5	1	1.37973
10	14	(A or (B → B))	210089	5	43	7	2.121747
11	15	((A → A) or B)	210089	5	43	7	2.121747
12	16	(A → (B → B))	212851	5	43	7	2.121747
13	50	(A → (A and A))	158696	5	67	9	2.318542
14	80	((A or A) → A)	158513	5	93	13	2.475692
15	91	(not (not (A → A)))	204846	5	101	15	2.51689
16	708	(not (A and (not A)))	156264	5	37	5	2.058924
17	763	(not ((not A) and A))	156284	5	37	5	2.058924
18	11142	(A → (not (not A)))	125517	5	214	27	2.92471

For instance, T₃₈₃₈₄, ((not A) or A) has following proof, as printed out by program:

tm-2.      ((A → (B → C)) → ((A → B) → (A → C))), axiom
tm-1.      (A → (B → A)), axiom
tm-11.     (A → (B → (C → B))), M:tm-1, m:tm-1
tm-61.     ((A → B) → (A → (C → B))), M:tm-2, m:tm-11
tm-10.     ((not (not A)) → A), axiom
tm-56.     (A → ((not (not B)) → B)), M:tm-1, m:tm-10
tm-171.    ((A → (not (not B))) → (A → B)), M:tm-2, m:tm-56
tm-3769.   ((A → (not (not B))) → (C → (A → B))), M:tm-61, m:tm-171
tm-12.     ((A → B) → (A → A)), M:tm-2, m:tm-1
tm-63.     (A → A), M:tm-12, m:tm-1
tm-79.     (((A → B) → A) → ((A → B) → B)), M:tm-2, m:tm-63
tm-80.     (A → (B → B)), M:tm-1, m:tm-63
tm-20224.  (((A → A) → B) → B), M:tm-79, m:tm-80
tm-20448.  (A → (((B → B) → C) → C)), M:tm-1, m:tm-20224
tm-21078.  ((A → ((B → B) → C)) → (A → C)), M:tm-2, m:tm-20448
tm-9.      ((A → B) → ((A → (not B)) → (not A))), axiom
tm-46593.  (((not A) → A) → (not (not A))), M:tm-21078, m:tm-9
tm-47470.  (A → (((not B) → B) → B)), M:tm-3769, m:tm-46593
tm-48685.  ((A → ((not B) → B)) → (A → B)), M:tm-2, m:tm-47470
tm-7.      (A → (B or A)), axiom
tm-36.     (A → (B → (C or B))), M:tm-1, m:tm-7
tm-157.    ((A → B) → (A → (C or B))), M:tm-2, m:tm-36
tm-2963.   ((not (not A)) → (B or A)), M:tm-157, m:tm-10
tm-3583.   (A → ((not (not B)) → (C or B))), M:tm-1, m:tm-2963
tm-13238.  ((A → (not (not B))) → (A → (C or B))), M:tm-2, m:tm-3583
tm-58849.  (((not (A or B)) → (not (not B))) → (A or B)), M:tm-48685, m:tm-13238
tm-6.      (A → (A or B)), axiom
tm-46.     ((A → (not (A or B))) → (not A)), M:tm-9, m:tm-6
tm-780.    (A → ((B → (not (B or C))) → (not B))), M:tm-1, m:tm-46
tm-23987.  ((A → (B → (not (B or C)))) → (A → (not B))), M:tm-2, m:tm-780
tm-203206. ((not (A or B)) → (not A)), M:tm-23987, m:tm-1
tm-203408. ((not A) or A), M:tm-58849, m:tm-203206

Notation tm- stands for internal representation of theorems in program. For instance, T₃₈₃₈₄ is tm-203408.

Fig 2. Size of the theorems derived by Program 2.

The graph shows that derived theorems are much shorter than those derived with Program 1. It is clearly visible which theorems are relatively short, yet they are derived relatively lately. Theorems T₃₈₃₈₄ and T₃₈₃₈₅, for instance, are among these. Some short theorems are used in futher derivation of short theorems. It is seen on graph as dent in graph; for instance, between T₃₈₃₈₃ and T₅₄₄₈₂. The width, depth and area of the dent suggest the importance of the theorem a posteriori. It appears that there is a correlation with size of proof as measure of the importance oftheorem a priori.

Fig. 3. Size of the proofs of theorems derived by Program 2.

Few weaknesses of Program 2. are obvious. Although derived theorems are not instances of previously derived theorems, human can recognize that many of these theorems are weak. For instance, theorems containing double negation; theorems of the form (F or G), where at least one of the formulas F and G is a theorem; theorems with subformulas of the form (F or F), (F and F), where F is any formula; thorems that could be obtained by application of commutativity and associativity of operations or and and and so forth. It is not obvious what might be the best approach for removing these.

Attachments

5. Conclusion

The program should be extended to reject more trivial variations of already derived theorems, as humans do. The results obtained so far appear to be interesting enough to justify further experiments.

References

Colton, S. and Bundy, A., "On the Notion of Interestingness in Automated Mathematical Discovery" in Proceedings of the AISB'99 Symposium on AI and Scientific Discovery, Edinburgh, UK, 1999.
Mendelson, E., Introduction to Mathematical Logic, many editions.
Poincare, H., Science and Method, Dover Publications, Mineola, 2003.
Wang, H., Toward Mechanical Mathematics, IBM Journal of Research and Development, Vol. 4 No. 1, January 1960, pp. 2-22.
Wang, H., Survey of Mathematical Logic, Nort Holland, Amsterdam, 1963.
Wos, L., Automated Reasoning: 33 Basic Research Problem, Prentice-Hall, 1988.
Wos, L., The Problem of Automated Theorem Finding, Journal of Automated Reasoning, Vol. 10 No. 1, 1993, pp. 137-8.

Lisp Demotivational Poster.

2011-09-05T02:13:00.003+02:00

Missing Link between Code and Data.

2011-08-22T16:10:00.004+02:00

Missing Link Between Code and Data

Here it is: configuration file. Is it code or data? Well, both. Furthermore, hypothesis is that every configuration file has a tendency to develop to the point it is written in Turing complete programming language. This interesting idea can be generalized and varied on many ways. It is not my idea, it is part of the folklore in my local hacker community. Thanks to Marcell Mars who contributed to its formulation and brought it to my attention.

The Similarities Between Axioms of Natural Numbers and Axioms of S-expressions.

2011-08-12T06:31:00.051+02:00

The Similarities Between Axioms of Natural Numbers and Axioms of S-expressions

In last post, it was shown that in Lisp practice, the term "symbolic expression", shorter "s-expression", "sepxr", "sexp" is used on few different, although similar meanings.

It is not unusual. Other terms, even mathematical ones, like "lines" or "numbers" are not uniquely defined as well. Ambiguity usually motivates the search for the essence of the discussed entities; the result of the search is axiomatic theory. For example, the axioms of natural numbers are developed in late 1880's by R. Dedekind and G. Peano.

Axioms of Natural Numbers

There is a set N ("numbers"), distinctive element of the N denoted with 1 ("base", "initial number") and mapping

successor: N → N

such that

all numbers, except 1, are successors of some numbers, i.e.

{ successor(n) | n ∈ N } = N \ {1};
the successor function is injection, or

successor(n) = successor(m) => n = m;
if S is a set of numbers such that
1. S contains all initial numbers (i.e. 1);
2. if S contains n, then S contains successor(n);
then S contains all numbers.

Search for axioms of symbolic expressions might be equally justified. I designed following axioms (version in which lists are only shorter way of writing "dotted pairs") to emphasize the similarities to axioms of natural numbers.

Axioms of Symbolic Expressions

There is a set SEXPR ("symbolic expressions"), infinite set of distinct elements of the SEXPR denoted with A ("atoms") and mapping

cons: SEXPR × SEXPR → SEXPR

such that

all symbolic expressions, except atoms, are conses, i.e.

{ cons(x, y) | x, y ∈ SEXPR } = SEXPR \ A;
the function cons is injection, i.e.

cons(n, p) = cons(m, q) => n = m and p = q;
if S is a set of symbolic expressions such that
1. S contains all atoms;
2. if S contains n and p then S contains cons(n, p);
then S contains all symbolic expressions.

Symbolic expressions in all three meanings satisfy the axioms; cons structures satisfy axiom (3) only if cyclic structures are not allowed, like in original, McCarthy's Lisp. I'm not aware of unintended, perverse models that satisfy given axioms; but I am not sure that such models do not exist.

There are only two differences between these axiom systems.

There is one "base element" for numbers and infinitely many for S-expressions.
The function "successor" is function of a single variable; the function "cons" is function of two variables.

It is not obvious that symbolic expressions require infinitely many atoms; it could be only convenience. Perhaps S-expressions like (A . (B . (C . D))) can be used instead of symbols like ABCD, eliminating need for infinitely many atoms.

It remains unclear why these two systems of axioms are so similar.

Three Meanings of The Term 'S-expression.'

2011-08-07T21:03:00.051+02:00

Three meanings of the term 'S-expression'

"Symbolic expressions" or "S-expressions" are the basic data type in Lisp. Particularly, Lisp programs are S-expressions as well. The notion has immense importance in Lisp community. 

Surprisingly, designers of recent Lisp dialects avoid the term "symbolic expression" or "S-expression". It is used once in Picolisp documentation; only twice, almost accidentally, in CLtL2, and it isn't used in CL Hyperspec or recent Scheme standards. Clojure, according to its web site "extends the code-as-data system beyond parenthesized lists (s-expressions) to vectors and maps." Only Newlisp documentation appear to regularly uses the term.

However, the term S-expression is still extensively used in daily communication and literature. Unfortunately, there is no universal, unique meaning. Inconsistent use is sometimes noted; for instance, in P. Siebel's "Practical Common Lisp." More frequently, it is ignored. 

For J. McCarthy, S-expression is finite sequence consisting of dots and parentheses and symbols. The symbols, truly atomic, cannot be analysed on characters. For instance, S-expression (left.right) is sequence of five elements: (, left, ., right and ). 

More often1, S-expression is seen as sequence of characters. In that meaning, S-expression (left . right) is sequence consisting of 14 elements.

The most usually2, S-expression is data structure, perhaps tree consisting of cons cells and symbols. In that meaning S-expression (left . right) is cons cell, containing adresses of symbols left and right in memory. 

1  For instance, in E. Shaphiro, "Common Lisp - an interactive approach"; F. Turbak and D. Gifford, "Design concept of programming languages." 

2  For instance, in J. and G. Sussman and H. Abelson, "SICP"; D. Touretsky, "Common Lisp - A gentle introduction to symbolic computation"; R. Finkel, "Advanced programming languages design".

Implementing Data Structures with Symbols.

2011-07-10T09:55:00.011+02:00

Implementing Data Structures with Symbols

Original Lisp had only symbols as atoms. Symbol names, if used on the same way variables are used in mathematics, are flexible enough to support wide variety (all?) data structures.

For instance, matrices 2 x 2 can be implemented with symbols as a11 instead of a[1,1] in some other language, or (a 1 1) in Lisp and names could be created as needed.

The code will be more complicated and less efficient than if matrices are directly supported by language, but neither one is essential problem - complexity of the code can be "abstracted away" with functions, and computational complexity is increased only for factor of constant * log n where n is the number of used symbols (if symbol reaching in Lisp is implemented efficiently.) Newlisp code follows.

(define (matrix-element m i j)

  (sym (append (string m) (string i) (string j))))



(define (set-matrix m m11 m12 m21 m22)

  (for(i 1 2)

    (for(j 1 2)

      (set (matrix-element m i j)

           (nth (+ (* 2 (- i 1)) (- j 1))

                (list m11 m12 m21 m22))))))

  

(define (println-matrix m)

  (for(i 1 2)

    (for(j 1 2)

       (println m "[" i "," j "]=" 

          (eval (matrix-element m i j))))))

          

(define (multiply-matrix a b c)

  (for(i 1 2)

    (for(j 1 2)

      (set (matrix-element c i j) 0)

      (for(k 1 2)

         (set (matrix-element c i j)

              (+ (eval (matrix-element c i j))

                 (* (eval (matrix-element a i k))

                    (eval (matrix-element b k j)))))))))



(set-matrix (quote X) 1 2 3 4)

(set-matrix (quote Y) 2 3 4 5)

(multiply-matrix (quote X) (quote Y) (quote Z))

(println-matrix (quote Z))



---------------------------

Program output



Z[1,1]=10

Z[1,2]=13

Z[2,1]=22

Z[2,2]=29

More on Another Encoding of S-expressions in Symbols.

2011-07-09T12:04:00.023+02:00

More on Another Encoding of S-expressions in Symbols

In previous post, I have shown another interesting method for encoding of S-expressions into symbols. In this post, I'll show how it can be implemented in Lisp dialects that print symbols on different way from S-expressions, i.e. encapsulated in vertical bars or other symbols (Common Lisp, ISLisp, Picolisp, some implementations of Scheme). This is, normally, good feature. However, repeated encoding of the symbols results in exponential growth. So, we must get rid of those vertical bars inside our symbols.

The code, here in Common Lisp, is sort of trickier than it is in Newlisp or it would be in Clojure.

(defun decode-deep (r)

  (cond ((symbolp r) (let((result (read-from-string (string r))))

                        (if (symbolp result)

                            result

                            (decode-deep result))))

        ((listp r) (mapcar (quote decode-deep) r))))



(defun sexpr->symbol (r) 

  (make-symbol (write-to-string (list 'q (decode-deep r)))))



(defun encode-deep (r)

  (cond ((symbolp r) r)

        ((listp r)(if (eq (first r) (quote q))

                      (make-symbol (write-to-string r))

                      (mapcar (quote encode-deep) r)))))



(defun strip-q (r) (first (rest r)))



(defun symbol->sexpr (r) 

  (encode-deep (strip-q (read-from-string (string r)))))



-------------



[43]> (setq q0 (sexpr->symbol (list (quote b) (quote c))))

#:|(Q (B C))|

[44]> (setq s (sexpr->symbol (list (quote a) q0)))

#:|(Q (A (Q (B C))))|

[45]> (setq s0 (symbol->sexpr s))

(A #:|(Q (B C))|)

Another Encoding of S-expressions in Symbols.

2011-07-09T00:17:00.025+02:00

Another Encoding of S-expressions in Symbols.

Unlike encoding from the last post, this one maintains form of S-expression. If e is S-expression, then its code is symbol (Q e).

Encoding is relatively simple, because built in functions for conversion of symbols and strings into symbols can be used; especially if symbols converted to strings are not encapsulated within vertical bars or quotation marks. Decoding is slightly more complicated. For instance, symbol

(Q (a (Q b)))

should be decoded into list (a (Q b)) where (Q b) isn't list, but symbol. Hence, built in conversion functions are not enough, but one must define his own "code walker." The code in Newlisp follows.

(define (sexpr->symbol r) (sym (string (list (quote Q) r))))



(define (qlist? r)

    (and (list? r)

         (not (empty? r))

         (= (first r) (quote Q))))

     

(define (symbol->sexpr r)

  (let((codewalker

         (lambda(r)

           (cond ((symbol? r) r)

                 ((qlist? r) (sym (string r)))

                 ((not (qlist? r)) (map codewalker r))))))

     (codewalker (last (read-expr (string r))))))

        

--------



> (setq s (sexpr->symbol (quote (a b))))

(Q (a b))

> (symbol? s)

true

> (setq q0 (sexpr->symbol (quote b)))

(Q b)

> (setq s (sexpr->symbol (list (quote a) q0)))

(Q (a (Q b)))

> (symbol? s)

true

> (setq s0 (symbol->sexpr s))

(a (Q b))

> (symbol? s0)

nil

> (symbol? (last s0))

true

Behaviour of Q strongly reminds on QUOTE.

More Sophisticated Encoding of S-exprs into Symbols.

2011-07-05T15:02:00.017+02:00

More Sophisticated Encoding of S-exprs into Symbols

Encoding of S-expressions into symbols is frequent topic of discussion in this blog. It is motivated by the idea that names should be equally flexible as S-expressions. (Actually, it might be the best if not only every symbol is S-expression, but also every S-expression is the symbol. OK, it is almost mystical statement.)

Trivial encoding was demonstrated in last post: S-expression is encoded in symbol which has exactly same characters as printed representation of S-expression. For instance, S-expression (+ a b) is encoded into symbol (+ a b). This trivial encoding has some limitations. For instance, if we look at symbol

((+ a b) c)

and try to decode it, we'll find that it cannot be determined whether (+ a b) is S-expression, or it is symbol. In some Lisp dialects (Common Lisp, Picolisp, ISLisp) there is no such problem. Symbol (+ a b) is written as |(+ a b)| so difference between S-expression and symbol is obvious. However, in these dialects, repeated encoding results in the symbols that grow exponentially.

In this post more sophisticated encoding, without that problem, is presented. Let us define encoding k, such that for every S-expression e, k(e) is defined as follows.

If e is symbol, then k(e) = e;
if e = (e₁ ... e_n) then k(e) = [k(e₁) k(e₂) ... k(e_n)];

Semi-colon is part of the symbol. For instance

k(a) = a;
k((a b)) = [k(a) k(b)]; = [a;b;];

If only codes of the S-expressions contain characters [, ] and ;, then encoding k is injection, i.e. for two S-expressions e and f,

k( e ) = k( f ) => e = f.

Furthermore, there is no exponential explosion in case of multiple encoding. For instance,

k((a b)) = [a;b;];
k(k((a b))) = [a;b;];;
k(k(k((a b)))) = [a;b];;;

Here is implementation of encoding and decoding in R⁵RS Scheme.

(define (sexpr->string L)

  (string-append

     (if (symbol? L) (symbol->string L)

                     (string-append

                        "["

                        (apply string-append

                               (map sexpr->string L))

                        "]"))

     ";"))

     

(define (sexpr->symbol L)

  (string->symbol (sexpr->string L)))

  

(define (string->sexpr S)

  (let((S1 (substring S 0 (- (string-length S) 1))))

    (if (equal? (string-ref  S1 (- (string-length S1) 1)) #\])

      (let((substring-begin 1)

           (level 0)

           (result (list)))

        (do ((i 1 (+ i 1)))

            ((= i (string-length S1)) result)

          (if (and (= level 0)

                   (equal? (string-ref S1 i) #\;)

                   (not (equal? (string-ref S1 (+ i 1)) #\;)))

            (begin

              (set! result

                    (append result

                            (list (string->sexpr

                                    (substring S1

                                               substring-begin

                                               (+ i 1))))))

              (set! substring-begin (+ i 1))))

          (cond ((equal? (string-ref S1 i) #\[)

                 (set! level (+ level 1)))

                ((equal? (string-ref S1 i) #\])

                 (set! level (- level 1))))))

      (string->symbol (substring S 0 (- (string-length S) 1))))))

      

(define (symbol->sexpr s)

  (string->sexpr (symbol->string s)))



-------------------------



> (sexpr->symbol (quote (a b)))

|[a;b;];|

> (define s2 (sexpr->symbol (quote (|[a;b;];| c))))

> s2

|[[a;b;];;c;];|

> (symbol->sexpr s2)

(|[a;b;];| c)

Exponential Explosion of Escape Characters.

2011-06-27T18:11:00.010+02:00

Exponential Explosion of Escape Characters

This time, Common Lisp:

? (setf q nil)

NIL

? (setf q (make-symbol (write-to-string q)))

#:NIL

? (setf q (make-symbol (write-to-string q)))

#:|#:NIL|

? (setf q (make-symbol (write-to-string q)))

#:|#:\|#:NIL\||

? (setf q (make-symbol (write-to-string q)))

#:|#:\|#:\\\|#:NIL\\\|\||

? (setf q (make-symbol (write-to-string q)))

#:|#:\|#:\\\|#:\\\\\\\|#:NIL\\\\\\\|\\\|\||

? (setf q (make-symbol (write-to-string q)))

#:|#:\|#:\\\|#:\\\\\\\|#:\\\\\\\\\\\\\\\|#:NIL\\\\\\\\\\\\\\\|\\\\\\\|\\\|\||

? (setf q (make-symbol (write-to-string q)))

#:|#:\|#:\\\|#:\\\\\\\|#:\\\\\\\\\\\\\\\|#:\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\|#:NIL

\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\|\\\\\\\\\\\\\\\|\\\\\\\|\\\|\||

? (setf q (make-symbol (write-to-string q)))

#:|#:\|#:\\\|#:\\\\\\\|#:\\\\\\\\\\\\\\\|#:\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\|#:\\\

\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\|#:NIL\\\\\\\\\\\\\\

\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\|\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\

\|\\\\\\\\\\\\\\\|\\\\\\\|\\\|\||

? (setf q (make-symbol (write-to-string q)))

#:|#:\|#:\\\|#:\\\\\\\|#:\\\\\\\\\\\\\\\|#:\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\|#:\\\

\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\|#:\\\\\\\\\\\\\\\\\

\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\

\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\|#:NIL\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\

\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\

\\\|\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\|\\\\\\\\\\\\

\\\\\\\\\\\\\\\\\\\|\\\\\\\\\\\\\\\|\\\\\\\|\\\|\||

? (setf q (make-symbol (write-to-string q)))

#:|#:\|#:\\\|#:\\\\\\\|#:\\\\\\\\\\\\\\\|#:\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\|#:\\\

\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\|#:\\\\\\\\\\\\\\\\\

\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\

\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\|#:\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\

\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\

\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\

\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\|#:NIL\\\\\\\\\\\\\\\\\\\\\\\\\\

\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\

\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\

\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\|\\\\\\\\\\

\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\

\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\|\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\

\\\\\\\\\\\\\\\\\\\\\|\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\|\\\\\\\\\\\\\\\|\\\\\\\|\\

\|\||

Tangent.

2011-05-07T23:20:00.035+02:00

Tangent

The specificity of Lisp is, maybe, best visible on problems that require processing of data naturally represented as S-expressions. An example of such problem is "Probability that random propositional formula is tautology." In this post, the variation of classical example - symbolic differentiation - is presented: newLISP (and it is very similar in other Lisps) program that computes the tangent of the graph of the function f of single variable, defined as composition of elementary functions (+, -, sin, cos ...) in given point x₀. The tangent of the function f in x₀is defined as linear function

y(x) = a·(x - x₀) + b,

where a = f '(x₀) and b = f(x₀). The program consists of:

The function tangent that accepts two arguments: the function f in form of lambda list and the floating point number x0. The function tangent analyzes the code of the function f, calculates the values a and b according to mathematical definition of tangent (see above) and constructs the code of the function

(lambda(x)(+. (*. a (-. x x0)) b))

where symbols a, b and x0 are replaced with their respective values; that function is then returned as result of the function tangent. The implementation is very short, but it delegates main part of the work to the function d.
The function d accepts two arguments: formula and variable. It returns the expression obtained by symbolic differentiation of the formula for given variable. It is main function in this program, typical recursive "code walking" through formula. Simple "domain specific language" is used for descriptions of the rules for symbolic differentiation that should be applied, for example

(+. (*. df g) (*. f dg))

for multiplication. The application of rules for symbolic differentiation frequently give result that can be simplified. For instance, derivation of (*. 2 x) is

(+. (*. 0 x) (*. 2 1))

so function simplify is called when appropriate.
The function simplify accepts only one argument: symbolic expression formula. It analyzes and simplify formula, again, using typical recursive "code walking". For instance, S-expression (- x x) is simplified to 0. There are infinitely many possible rules for simplification; the function performs only few of these. The function uses eval at one place: if some expression contains only operators and constants, but not variables then the easisest way to simplify it is to eval it. (One might speculate that simplify is generalized eval.) Simplification is, actually, not necessary for computation of the tangent. However, its use in the context of symbolic differentiation is reasonable.

Few operators from my library are used; function expand// i.e. parallel expand, fexpr println= for convenient printing and floating point arithmetic operators +., -., *. and /., synonymous for built-in add, sub, mul and div. These functions are not essential.

The graph of the complicated function and tangent on the curve suggests that program, generally, works.

(setf f0 (lambda(x)
           (+. (sin (*. 12 x))
               (cos (*. 32 x))
               (tan (*. x 1.4))
               (asin x)
               (acos  x)
               (atan x)
               (*. x (cos (/. 7 x)))
               (sqrt (/. 9 x))
               (pow x x)
               (*. x (sinh x))
               (*. x (cosh x))
               (asinh x)
               (sin (acosh (+. x 1)))
               (atanh x))))
(setf x0 0.4)
(println= (tangent f0 x0))
; (tangent f0 x0)=(lambda (x) (+. (*. -21.491 (-. x 0.4)) 10.252))

Finally, the code:

(setf [print.supressed] true [println.supressed] true)

(load "http://www.instprog.com/Instprog.default-library.lsp")

(setf [print.supressed] nil [println.supressed] nil)



(define (tangent f x0)

   (letn((variable           (first (first f)))

         (expression         (last f))

         (derived-expression (d expression variable))

         

         (a                  (eval (expand derived-expression

                                           (list (list variable x0)))))

         (b                  (f x0)))

        

       (expand// '(lambda(x)(+. (*. a (-. x x0)) b))

                  'a 'b 'x0)))



(define (d formula variable)

  (simplify 

    (cond 

      ((= formula variable) 1)

      ((atom? formula) 0)

      ((list? formula)

       (letn((operator (first formula))

             (operands (rest formula))

             (lexpand 

               (lambda(expr)

                 (letn((flatexpr (flat expr))

                       (f  (if (find 'f  flatexpr)(operands 0)))

                       (df (if (find 'df flatexpr)(d f variable)))

                       (g  (if (find 'g  flatexpr)(operands 1)))

                       (dg (if (find 'dg flatexpr)(d g variable))))

                   (expand// expr 'f 'df 'g 'dg)))))



         (case operator 



           (+. (cons '+. (map (lambda(op)(d op variable)) operands)))

           (-. (cons '-. (map (lambda(op)(d op variable)) operands)))



           (*. (case (length operands)

                 (1    (lexpand 'df))

                 (2    (lexpand '(+. (*. df g) (*. f dg))))

                 (true (d (list '*. (first operands)

                                    (cons '*. (rest operands)))

                           variable))))



           (/. (case (length operands)

                 (1    (d (list '/. 1 (first operands)) variable)) 

                 (2    (lexpand '(/. (-. (*. df g) (*. f dg)) (*. g g))))

                 (true (d (list '/.  (first operands)

                                     (cons '*. (rest operands)))

                       variable))))



           (pow (d (lexpand '(exp (*. g (log f)))) variable))

           (exp (lexpand '(*. f df)))

           (log (if (= (length operands) 1)

                    (lexpand '(/. df f))

                    (d (lexpand '(/. (log f) (log g))) variable)))



           (sqrt  (lexpand '(*. 0.5 df (/. 1 (sqrt f)))))

           (sin   (lexpand '(*. (cos f) df)))

           (cos   (lexpand '(*. (-. (sin f)) df)))

           (tan   (lexpand '(/. df (pow (cos f) 2))))

            (asin (lexpand '(/. df (sqrt (-. 1 (*. f f))))))

           (acos  (lexpand '(-. (/. df (sqrt (-. 1 (*. f f)))))))

           (atan  (lexpand '(/. df (+. 1 (*. f f)))))

           (sinh  (lexpand '(*. (cosh f) df)))

           (cosh  (lexpand '(*. (sinh f) df)))

           (tanh  (lexpand '(*. (-. 1 (pow (tanh f) 2)) df)))

           (asinh (lexpand '(/. df (sqrt (+.(*. f f) 1)))))

           (acosh (lexpand '(/. df (sqrt (-. (*. f f) 1)))))

           (atanh (lexpand '(/. df (-. 1 (*. f f)))))



           ))))))



(define (simplify formula)

  (cond 

    ((atom? formula) formula)

    ((list? formula)

     (letn((operator (first formula))

           (operands (map simplify (rest formula)))

           (formula (cons operator operands)))



       (cond 

       

         ; if all operands are constants, then 

         ; simplified formula is evaluated formula

   

         ((for-all number? operands)(eval formula))

   

         ; (*. x), (+. x) => x

         

         ((and (or (= operator '*.) (= operator '+.)) 

               (= (length operands) 1))

           (first operands))

           

         ; (*. ... 0 ...) => 0  

           

         ((and (= operator '*.) (find 0 operands)) 0)

         

         ; (*. ... 1 ...) => (*. ...)

         

         ((and (= operator '*.) (find 1 operands))

          (simplify (clean (curry = 1) formula)))

         

         ; (+. ... 0 ...) => 0

         

         ((and (= operator '+.) (find 0 operands))

          (simplify (clean zero? formula)))

          

         ; (-. (-. ...)) => ...

         

         ((match '(-. (-. ?)) formula)

           (last (last formula)))

           

         ; (-. minuend ...)

         

         ((and (= operator '-.) (> (length operands) 1))

               

          (letn((minuend (first operands))

                (subtrahends (rest operands))

                (subtrahend  (simplify (cons '+. subtrahends))))

                

            (cond ((zero? minuend)        (simplify (list '-. 

                                                          subtrahend)))

                  ((zero? subtrahend)     minuend)

                  ((= minuend subtrahend) 0)

                  (true                   (list '-. minuend 

                                                    subtrahend)))))

                     

         ; (/. (/. ...))

               

         ((match '(/. (/. ?)) formula) (last (last formula)))

         

         ; (/. dividend ...)

         

         ((and (= operator '/.) (> (length operands) 1))

          (letn((dividend (first operands))

                (divisors (rest operands))

                (divisor  (simplify (cons '*. divisors))))

            

            (cond ((zero? dividend)     0)

                  ((= divisor 1)        dividend)

                  ((= divisor -1)       (simplify (list '-. dividend)))

                  ((= dividend divisor) 1)

                  (true                 (list '/. dividend divisor)))))

          

         (true formula))))))

Conflation of Subtraction and Additive Inverse in Lisp.

2011-05-03T15:17:00.015+02:00

Conflation of Subtraction and Additive Inverse in Lisp

In mathematics, the symbol - is used as name of two different operations: subtraction and additive inverse. For instance, that symbol has different meaning in the expressions (-3)+7 and (6-3)+7. There is no ambiguity. The edge case of subtraction

c - b₁ - b₂ - ... - b_n

for n = 0, i.e. subtraction with zero subtrahends, is c, which is clearly different than additive inverse of c: - c. However, in prefix notation use of the same symbol for two different operators will cause ambiguity so (- c) can be interpreted as both additive inverse of c and the edge case of subtraction with zero subtrahends. Designers of almost all Lisp dialects have chosen to keep the same symbol and implement both operations. The decision is based on the number of operands: if there is only one operand, operator - behaves as additive inverse; if there is two or more operands - behaves as subtraction.

This decision rarely causes any problems with "hand written" expressions because humans automatically, without much thinking, reduce edge case of subtraction to minuend, so, we'll not see the edge case of subtraction in any mathematical formulas. However, if expressions are processed by programs the reduction of the edge case doesn't happen automatically. For instance, the program that simplifies arithmetic expression could contain the function that deletes zeroes from subtrahends. That function should accept expression as

(- c b1 0 b2 0 0  0)

as argument and return expression

(- c b1 b2).

However, simple implementation like this one in Newlisp

(define (simplify E)

  (let ((operator (first E))

        (minuend (first (rest E)))

        (subtrahends (rest (rest E))))

       (setf new-subtrahends (clean zero? subtrahends))

       (append (list operator)

               (list minuend)

               new-subtrahends)))

will not work correctly, because, for instance, (- 3 0) will be reduced into (- 3) and these two expressions have not the same value. Explicit treatment of the edge case is required:

(define (simplify E)

  (let ((operator (first E))

        (minuend (first (rest E)))

        (subtrahends (rest (rest E))))

       (setf new-subtrahends (clean zero? subtrahends))

       (if (empty? new-subtrahends)

           minuend

           (append (list operator)

                   (list minuend)

                   new-subtrahends))))

The second definition is significantly (~ 15%) larger and less consistent: one can get rid of subtrahends equal to zero only if he removes whole subtraction. On the other hand, edge cases for some other operations like addition are well supported in all Lisp dialects: not only that (+ a 0) can be safely simplified to (+ a), but even (+ 0 0) can be simplified to (+).

Hence, merging of the two operators into one could be design mistake. It would be, arguably, better to

define new operator for additive inverse and
extend definition of subtraction on special case with zero subtrahends.

Of course, S-expressions would look even less similar to arithmetic expressions, however, clarity and consistency over convenience is, I think, the element of the philosophy of Lisp.

It is even more surprising that this merging is generalized: division operator, / which is not used as divisional inverse in mathematical expressions is used on the way analogous to - in almost all Lisp dialects.

It is hard to expect change in existing Lisp dialects because lot of existing code uses "conflated operator", although I think that such changes should be, gradually, done: the past is finite and future is infinite. However, I think that for future Lisp dialects it would be better to keep the difference between subtraction (division) and additive (multiplicative) inverse.

Parallel "expand".

2011-04-26T19:09:00.004+02:00

Parallel "Expand"

Almost all Lisp dialects support both "parallel" and "serial" assignment operators like let and letn in Newlisp. For example

(setf y 1)

(let((y 2)(x y)) x) ==> 1 (parallel)

but

(setf y 1)

(letn((y 2)(x y)) x) ==> 2 (serial)

Expand-expression in Newlisp

(expand '(x y) 'x 'y)

results in replacement of x and y in (x y) with values of x and y. Expand-expression in other form:

(expand '(x y) ((x <value1>)(y <value2>)))

results in replacement of x and y in (x y) with <value1> and <value2>.

In both cases, the replacement is performed in serial fashion. For example,

(expand '(x y) '((x y)(y 3))) ==> (3 3)

In this post I present the implementation of parallel expand, expand// in Newlisp; two slashes in name remind on parallel lines such that, for instance

(expand// '(x y) '((x y)(y 3))) ==> (y 3).

Parallel expand expression can be reduced to serial expand with introduction of new variables.

(expand// <expr> '((<var1> <val1>)...(<varn> <valn>))) =

(expand <expr> '((<var1> expand//1) ... (<varn> expand//<n>)

(expand//1 <val1> ) ... (expand//n <valn>)))

Fexpr expand// can use always the same temporary variables expand//1, ..., expand//n, without need for generating fresh variables each time expand// is called. Other form of expand//,

(expand// <expr> '<var0> ... '<varn>)

can be reduced on form

(expand <expr>

'((<var0> expand//0) ... (<varn> expand//<n>)

(expand//0 <value of var0>) ... (expand//<n> <value of var<n>>))).

Using that idea, the implementation is not very technical

(define (expand// expr)

  (letn((a (args))

        (expand//sym (lambda(n)(sym (append "expand//" (string n)))))

        (expandlist 

       

    (if (empty? a)

        (throw-error "expand//: arguments missing.")





        (cond ((symbol? (first a))

               (append (map (lambda(i)(list i (expand//sym $idx))) a)

                       (map (lambda(i)(list (expand//sym $idx) (eval i))) a)))

                 

              ((list? (first a))

               (append (map (lambda(i)(list (i 0) (expand//sym $idx))) (first a))

                       (map (lambda(i)(list (expand//sym $idx) (i 1))) (first a))))))))

                



       (println "expandlist=" expandlist)

       (expand expr expandlist)))

       



(setf x 'y)

(setf y 3)

(println (expand '(x y) 'x 'y))           ; => (3 3)

(println (expand// '(x y) 'x 'y))         ; => (y 3)

(println (expand '(x y) '((x y)(y 3))))   ; => (3 3)

(println (expand// '(x y) '((x y)(y 3)))) ; => (y 3)





(exit)

"Nothing Will Happen" in Belgrade, April 2011

2011-04-23T16:20:00.008+02:00

Nothing Will Happen in Belgrade, April 2011

I returned from another "Ništa se neće dogoditi" (Nothing will happen) hacker conference, this time in Belgrade, Serbia. As usually, the program was made on place on the base of existing supply and demand. No attendance fee. Lot of fun and enthusiasm. I didn't prepared presentation but as there was some interest in Lisp, I discussed some of the most popular topics discussed in this blog.

I forgot my camera, so I borrow few photos made by other participants.

Thanks to organizers.

Waiting for the start. I'm third from the left.

One presentation held in "Magacin."

One presentation held in bar.

See also "Nothing will Happen", Split, August 2010

One Picolisp Snippet.

2011-04-08T00:11:00.018+02:00

One Picolisp Snippet

I had presentation on Picolisp in Hacklab "Mama" in Zagreb few weeks ago.

Not that I'm expert in Picolisp, but I think I understand it well enough for short introduction. Picolisp is somehow Spartan dialect of Lisp - for example, it doesn't support floating point numbers, and it is not available on Windows - except by using VirtualBox or something like that. But it is dynamically scoped, and it supports some powerful and interesting features as fexprs, coroutines and anonymous symbols, integrated Prolog and database. It is particularly interesting that Picolisp doesn't have strings - the symbols are used for that purpose. On the first sight, absence doesn't look like advantage, but it is, because all usual functions defined on strings now work directly on symbols, without need for conversion.

As a bonus, Picolisp might be the fastest Lisp interpreter, written entirely (in 64 bit version) in assembly language.

The author of Picolisp is Alexander Burger; as Picolisp is, in spirit, very similar to Newlisp, we can almost speak about German school of Lisp. OK, maybe another similar Lisp "made in Germany" is needed for that.

The reactions on Picolisp and presentation were positive; Zagreb is one of the places where Lispers encourage each other, no matter of dialect. We had three days of "Clojure Fest" few months ago (unfortunately collided with swine flue fest.)

I don't want to allow you to go home without any code, so this was the most liked example from presentation.

: (setq my '(list 1 2))

-> (list 1 2)

: (intern (name (zap 'list) "popis"))  # not a string

-> popis

: (popis 1 2 3)                      

-> (1 2 3)

: my           

-> (popis 1 2)

Variable Definitions Supported in Clojure, Common Lisp, ISLisp, newLISP, Picolisp and Scheme.

2011-04-06T09:15:00.008+02:00

Variable Definitions Supported in Clojure, Common Lisp, ISLisp, newLISP, Picolisp and Scheme

		variable	constant ("immutable variable")
global	lexical	ISLisp (defglobal) Scheme (define)
global	dynamic	Clojure (def) CL (defvar, defparameter) ISLisp (defdynamic) Picolisp (de) Newlisp (define)	CL (defconstant) ISLisp (defconstant) Newlisp (define + constant)
local	lexical	CL (let, let) ISLisp (let, let) Scheme (let, let, letrec, letrec)	Clojure (let, let*)
local	dynamic	Clojure (def + binding) CL (let + declare special, def... + let) ISLisp (dynamic-let) Newlisp (let, letn) Picolisp (let)

If I forgot something or made mistake, please, let me know.

Symmetric Support for Lexical and Dynamic Scope (Binding) in ISLisp.

2011-04-04T22:40:00.009+02:00

In ISLisp, all combinations of global/local and lexical/dynamic 

operators for definition of variables are supported.



If operator contains word "dynamic", then the binding will be dynamic. 

The operator 'dynamic' is needed for reference of such variables.

Hence, ISLisp is only dialect of Lisp that allows all versions of 

standard example for explanation of difference between lexical

and dynamic scope. 



1. Variable x is defined with lexical/dynamic global binding and

   value 1. The function f=(lambda()x) is defined on top level.



2. Variable x is defined with lexical/dynamic local binding and  

   value 2. The function f is called from the scope of that binding. 

  

There are four combinations:



                                 global binding of x in

                              place of function definition 



                               |  lexical  |  dynamic

local            --------------+ ----------+-----------         

binding of x         lexical   |     1     |    1

in place of      --------------+-----------+-----------

function call        dynamic   |     1     |    2

                 --------------+-----------+-----------

           



Here is the code: 



;-----------------



(defglobal x 1)

(defun f()x)



(let((x 2))

  (print (f)))       ;=>1



;-----------------



(defglobal x 1)

(defun f()x)



(dynamic-let((x 2))

  (print (f)))       ;=>1



;-----------------



(defdynamic x 1)

(defun f()(dynamic x))



(let((x 2))

  (print (f)))       ;=>1



;-----------------



(defdynamic x 1)

(defun f()(dynamic x))



(dynamic-let((x 2))

  (print (f)))       ;=>2

  

;-----------------



ISLisp itself is simplified and on few places, like this one, improved 

Common Lisp. I must recommend its most well known implementation: 

Christian Jullien's Eligis OpenLisp. It is commercial Lisp compiler 

which supports more than 90 architectures - from 16 bit MSDOS to 

IBM mainframe; there is also an interpreter, which is free for 

personal use, and so well implemented that on my EVAL test it is second 

only to in assembly language written Picolisp, so OpenLisp can be 

attractive to those who like dynamic scope and eval. Support is excellent. 



Check it. It definitely deserves more attention.

OpenLisp site

--

Lambda Calculus Meta-variables Supported in my Newlisp Library.

2011-02-07T23:50:00.006+01:00

Lambda calculus is very small and still "Turing complete" language. However, because of its simplicity and small size, it is very hard to write real programs - even harder than in assembly language. Most of the materials demonstrating programming in lambda calculus> use meta-variables. For instance, TRUE is defined as

'(^ x .(^ y . x))),
and after that, TRUE is used instead of given expression. If such meta-variables are used, lambda-expressions are much shorter and more readable, however, there is no essential difference, since before reduction, all meta-variables are "expanded" into real lambda-expressions.

I already implemented support for reduction of lambda expressions in my Newlisp library. The code that deals with meta-variables is rather simple. It is just recursive substitution of meta-variable's value for meta-variable itself.

You can see how it works in my previous post, now updated.

Some Basic Concepts Implemented and Reduced in Lambda-calculus.

2011-02-05T21:49:00.009+01:00

; After support for meta-variables in lambda-calculus is integrated
; in my Newlisp library, I can easily demonstrate few fundamental
; concepts: Boolean constants, integers, IF, predecessor, successor,
; multiplication and recursion are implemented in lambda calculus
; and how reduction of the expressions really looks like.
;
; At the end, factorial function is implemented - this time without
; full reduction, because even reduction of (FACTORIAL 0) is too
; large to be published in blog. However, you can try it for yourself.
;
; Watch out: it is frequently said this can be done, but it is
; rarely actually done.
;
;                    LOADING LIBRARY
;

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

;---------------------------------------------------------------

(setf TRUE '(^ x .(^ y . x)))

    (expand-and-reduce^ '((TRUE a) b) ; <- lambda-expression
                         5000         ; <- max number of expansions
                                      ;    and reductions
                         true)        ; <- true if output is needed

;---------------------------------------------------------------
;
;        EXPANSION AND REDUCTION OF ((TRUE a) b)
;
;     1. ==[ original ]==> ((TRUE a) b)
;     2. ==[ expanded ]==> (((^x.(^y.x)) a) b)
;
;        META-VARIABLES EXPANDED.
;
;     1. ==[ start    ]==> (((^x.(^y.x)) a) b)
;     2. ==[ beta     ]==> ((^y.a) b)
;     3. ==[ alpha    ]==> ((^x.a) b)
;     4. ==[ beta     ]==> a
;
;        REDUCED TO NORMAL FORM.
;
;---------------------------------------------------------------

(setf FALSE '(^ x . (^ y . y)))

     (expand-and-reduce^ '((FALSE a) b)
                         5000
                         true)

;---------------------------------------------------------------
;
;        EXPANSION AND REDUCTION OF ((FALSE a) b)
;
;     1. ==[ original ]==> ((FALSE a) b)
;     2. ==[ expanded ]==> (((^x.(^y.y)) a) b)
;
;        META-VARIABLES EXPANDED.
;
;     1. ==[ start    ]==> (((^x.(^y.y)) a) b)
;     2. ==[ beta     ]==> ((^y.y) b)
;     3. ==[ alpha    ]==> ((^x.x) b)
;     4. ==[ beta     ]==> b
;
;        REDUCED TO NORMAL FORM.
;
;---------------------------------------------------------------

(setf IF '(^ v .(^ t . (^ f . ((v t) f)))))

     (expand-and-reduce^ '(((IF a) b) c)
                         5000
                         true)

;---------------------------------------------------------------
;
;        EXPANSION AND REDUCTION OF (((IF a) b) c)
;
;     1. ==[ original ]==> (((IF a) b) c)
;     2. ==[ expanded ]==> ((((^v.(^t.(^f.((v t) f)))) a) b) c)
;
;        META-VARIABLES EXPANDED.
;
;     1. ==[ start    ]==> ((((^v.(^t.(^f.((v t) f)))) a) b) c)
;     2. ==[ alpha    ]==> ((((^x.(^y.(^z.((x y) z)))) a) b) c)
;     3. ==[ eta      ]==> ((((^x.(^y.(x y))) a) b) c)
;     4. ==[ eta      ]==> ((((^x.x) a) b) c)
;     5. ==[ beta     ]==> ((a b) c)
;
;        REDUCED TO NORMAL FORM.
;
;---------------------------------------------------------------

     (expand-and-reduce^ '(((IF TRUE) a) b)
                          5000
                          true)
;---------------------------------------------------------------

;
;        EXPANSION AND REDUCTION OF (((IF TRUE) a) b)
;
;     1. ==[ original ]==> (((IF TRUE) a) b)
;     2. ==[ expanded ]==> ((((^v.(^t.(^f.((v t) f))))(^x.(^y.x))) a) b)
;
;        META-VARIABLES EXPANDED.
;
;     1. ==[ start    ]==> ((((^v.(^t.(^f.((v t) f))))(^x.(^y.x))) a) b)
;     2. ==[ alpha    ]==> ((((^x.(^y.(^z.((x y) z))))(^u.(^v.u))) a) b)
;     3. ==[ eta      ]==> ((((^x.(^y.(x y)))(^u.(^v.u))) a) b)
;     4. ==[ alpha    ]==> ((((^x.(^y.(x y)))(^z.(^u.z))) a) b)
;     5. ==[ eta      ]==> ((((^x.x)(^z.(^u.z))) a) b)
;     6. ==[ alpha    ]==> ((((^x.x)(^y.(^z.y))) a) b)
;     7. ==[ beta     ]==> (((^y.(^z.y)) a) b)
;     8. ==[ alpha    ]==> (((^x.(^y.x)) a) b)
;     9. ==[ beta     ]==> ((^y.a) b)
;    10. ==[ alpha    ]==> ((^x.a) b)
;    11. ==[ beta     ]==> a
;
;        REDUCED TO NORMAL FORM.
;

;---------------------------------------------------------------

     (expand-and-reduce^ '(((IF FALSE) a) b)
                          5000
                          true)
;---------------------------------------------------------------

;
;        EXPANSION AND REDUCTION OF (((IF FALSE) a) b)
;
;     1. ==[ original ]==> (((IF FALSE) a) b)
;     2. ==[ expanded ]==> ((((^v.(^t.(^f.((v t) f))))(^x.(^y.y))) a) b)
;
;        META-VARIABLES EXPANDED.
;
;     1. ==[ start    ]==> ((((^v.(^t.(^f.((v t) f))))(^x.(^y.y))) a) b)
;     2. ==[ alpha    ]==> ((((^x.(^y.(^z.((x y) z))))(^u.(^v.v))) a) b)
;     3. ==[ eta      ]==> ((((^x.(^y.(x y)))(^u.(^v.v))) a) b)
;     4. ==[ alpha    ]==> ((((^x.(^y.(x y)))(^z.(^u.u))) a) b)
;     5. ==[ eta      ]==> ((((^x.x)(^z.(^u.u))) a) b)
;     6. ==[ alpha    ]==> ((((^x.x)(^y.(^z.z))) a) b)
;     7. ==[ beta     ]==> (((^y.(^z.z)) a) b)
;     8. ==[ alpha    ]==> (((^x.(^y.y)) a) b)
;     9. ==[ beta     ]==> ((^y.y) b)
;    10. ==[ alpha    ]==> ((^x.x) b)
;    11. ==[ beta     ]==> b
;
;        REDUCED TO NORMAL FORM.
;

;---------------------------------------------------------------
(setf APPLY '(^ v .(^ f . (v f))))

     (expand-and-reduce^ '((APPLY a) b)
                          5000
                          true)

;----------------------------------------------------------------
;
;        EXPANSION AND REDUCTION OF ((APPLY a) b)
;
;     1. ==[ original ]==> ((APPLY a) b)
;     2. ==[ expanded ]==> (((^v.(^f.(v f))) a) b)
;
;        META-VARIABLES EXPANDED.
;
;     1. ==[ start    ]==> (((^v.(^f.(v f))) a) b)
;     2. ==[ alpha    ]==> (((^x.(^y.(x y))) a) b)
;     3. ==[ eta      ]==> (((^x.x) a) b)
;     4. ==[ beta     ]==> (a b)
;
;        REDUCED TO NORMAL FORM.
;
;----------------------------------------------------------------

; Y-combinator is tool that could be used for implementation of
; recursion

(setf Y '(^ f . ((^ x . (f (x x))) (^ x . (f (x x))))))

     (expand-and-reduce^ '(Y g)
                         12
                         true)
;---------------------------------------------------------------

;
;        EXPANSION AND REDUCTION OF (Y g)
;
;     1. ==[ original ]==> (Y g)
;     2. ==[ expanded ]==> ((^f.((^x.(f (x x)))(^x.(f (x x))))) g)
;
;        META-VARIABLES EXPANDED.
;
;     1. ==[ start    ]==> ((^f.((^x.(f (x x)))(^x.(f (x x))))) g)
;     2. ==[ alpha    ]==> ((^x.((^y.(x (y y)))(^z.(x (z z))))) g)
;     3. ==[ beta     ]==> ((^y.(g (y y)))(^z.(g (z z))))
;     4. ==[ alpha    ]==> ((^x.(g (x x)))(^y.(g (y y))))
;     5. ==[ beta     ]==> (g ((^y.(g (y y)))(^y.(g (y y)))))
;     6. ==[ alpha    ]==> (g ((^x.(g (x x)))(^y.(g (y y)))))
;     7. ==[ beta     ]==> (g (g ((^y.(g (y y)))(^y.(g (y y))))))
;     8. ==[ alpha    ]==> (g (g ((^x.(g (x x)))(^y.(g (y y))))))
;     9. ==[ beta     ]==> (g (g (g ((^y.(g (y y)))(^y.(g (y y)))))))
;    10. ==[ alpha    ]==> (g (g (g ((^x.(g (x x)))(^y.(g (y y)))))))
;    11. ==[ beta     ]==> (g (g (g (g ((^y.(g (y y)))(^y.(g (y y))))))))
;    12. ==[ alpha    ]==> (g (g (g (g ((^x.(g (x x)))(^y.(g (y y))))))))
;
;        UNREDUCED: MAX NUMBER OF REDUCTIONS REACHED.
;
; Take a look on the way "reduced" lambda-expression looks like;
;
; (Y g) is reduced to (g (Y g))! If we use some more complicated
; formula instead of g, and normal order of reduction, then
; g will be evaluated first.
;

;---------------------------------------------------------------
(setf ZERO '(^ f . (^ x . x)))

   (expand-and-reduce^ ZERO
                       5000
                       true)

;---------------------------------------------------------------
;
;        EXPANSION AND REDUCTION OF (^f.(^x.x))
;
;     1. ==[ original ]==> (^f.(^x.x))
;
;        META-VARIABLES EXPANDED.
;
;     1. ==[ start    ]==> (^f.(^x.x))
;     2. ==[ alpha    ]==> (^x.(^y.y))
;
;        REDUCED TO NORMAL FORM.
;
;---------------------------------------------------------------

(setf SUCCESSOR '(^ n . (^ f . (^ x . (f ((n f) x))))))

   (expand-and-reduce^ '(SUCCESSOR ZERO)
                        5000
                        true)
;---------------------------------------------------------------

;
;        EXPANSION AND REDUCTION OF (SUCCESSOR ZERO)
;
;     1. ==[ original ]==> (SUCCESSOR ZERO)
;     2. ==[ expanded ]==> ((^n.(^f.(^x.(f ((n f) x)))))(^f.(^x.x)))
;
;        META-VARIABLES EXPANDED.
;
;     1. ==[ start    ]==> ((^n.(^f.(^x.(f ((n f) x)))))(^f.(^x.x)))
;     2. ==[ alpha    ]==> ((^x.(^y.(^z.(y ((x y) z)))))(^u.(^v.v)))
;     3. ==[ beta     ]==> (^y.(^z.(y (((^u.(^v.v)) y) z))))
;     4. ==[ alpha    ]==> (^x.(^y.(x (((^z.(^u.u)) x) y))))
;     5. ==[ beta     ]==> (^x.(^y.(x ((^u.u) y))))
;     6. ==[ alpha    ]==> (^x.(^y.(x ((^z.z) y))))
;     7. ==[ beta     ]==> (^x.(^y.(x y)))
;     8. ==[ eta      ]==> (^x.x)
;
;        REDUCED TO NORMAL FORM.
;

;---------------------------------------------------------------
(setf ONE '(^ x . x))

   (expand-and-reduce^ '(SUCCESSOR (SUCCESSOR ZERO))
                       5000
                       true)
;---------------------------------------------------------------

;
;        EXPANSION AND REDUCTION OF (SUCCESSOR (SUCCESSOR ZERO))
;
;     1. ==[ original ]==> (SUCCESSOR (SUCCESSOR ZERO))
;     2. ==[ expanded ]==> ((^n.(^f.(^x.(f ((n f) x)))))((^n.(^f.(^x.(f ((n f) x)))))(^f.(^x.x))))
;
;        META-VARIABLES EXPANDED.
;
;     1. ==[ start    ]==> ((^n.(^f.(^x.(f ((n f) x)))))((^n.(^f.(^x.(f ((n f) x)))))(^f.(^x.x))))
;     2. ==[ alpha    ]==> ((^x.(^y.(^z.(y ((x y) z)))))((^u.(^v.(^w.(v ((u v) w)))))(^p.(^q.q))))
;     3. ==[ beta     ]==> (^y.(^z.(y ((((^u.(^v.(^w.(v ((u v) w)))))(^p.(^q.q))) y) z))))
;     4. ==[ alpha    ]==> (^x.(^y.(x ((((^z.(^u.(^v.(u ((z u) v)))))(^w.(^p.p))) x) y))))
;     5. ==[ beta     ]==> (^x.(^y.(x (((^u.(^v.(u (((^w.(^p.p)) u) v)))) x) y))))
;     6. ==[ alpha    ]==> (^x.(^y.(x (((^z.(^u.(z (((^v.(^w.w)) z) u)))) x) y))))
;     7. ==[ beta     ]==> (^x.(^y.(x ((^u.(x (((^v.(^w.w)) x) u))) y))))
;     8. ==[ alpha    ]==> (^x.(^y.(x ((^z.(x (((^u.(^v.v)) x) z))) y))))
;     9. ==[ beta     ]==> (^x.(^y.(x (x (((^u.(^v.v)) x) y)))))
;    10. ==[ alpha    ]==> (^x.(^y.(x (x (((^z.(^u.u)) x) y)))))
;    11. ==[ beta     ]==> (^x.(^y.(x (x ((^u.u) y)))))
;    12. ==[ alpha    ]==> (^x.(^y.(x (x ((^z.z) y)))))
;    13. ==[ beta     ]==> (^x.(^y.(x (x y))))
;
;        REDUCED TO NORMAL FORM.
;

;---------------------------------------------------------------
(setf ZERO? '(^ n . ((n (TRUE FALSE)) TRUE)))

   (expand-and-reduce^ '(ZERO? ZERO)
                       5000
                       true)
;---------------------------------------------------------------

;
;        EXPANSION AND REDUCTION OF (ZERO? ZERO)
;
;     1. ==[ original ]==> (ZERO? ZERO)
;     2. ==[ expanded ]==> ((^n.((n (TRUE FALSE)) TRUE))(^f.(^x.x)))
;     3. ==[ expanded ]==> ((^n.((n ((^x.(^y.x))(^x.(^y.y))))(^x.(^y.x))))(^f.(^x.x)))
;
;        META-VARIABLES EXPANDED.
;
;     1. ==[ start    ]==> ((^n.((n ((^x.(^y.x))(^x.(^y.y))))(^x.(^y.x))))(^f.(^x.x)))
;     2. ==[ alpha    ]==> ((^x.((x ((^y.(^z.y))(^u.(^v.v))))(^w.(^p.w))))(^q.(^r.r)))
;     3. ==[ beta     ]==> (((^q.(^r.r))((^y.(^z.y))(^u.(^v.v))))(^w.(^p.w)))
;     4. ==[ alpha    ]==> (((^x.(^y.y))((^z.(^u.z))(^v.(^w.w))))(^p.(^q.p)))
;     5. ==[ beta     ]==> ((^y.y)(^p.(^q.p)))
;     6. ==[ alpha    ]==> ((^x.x)(^y.(^z.y)))
;     7. ==[ beta     ]==> (^y.(^z.y))
;     8. ==[ alpha    ]==> (^x.(^y.x))
;
;        REDUCED TO NORMAL FORM.
;

;---------------------------------------------------------------

   (expand-and-reduce^ '(ZERO? (SUCCESSOR ZERO))
                       5000
                       true)
;---------------------------------------------------------------

;
;        EXPANSION AND REDUCTION OF (ZERO? (SUCCESSOR ZERO))
;
;     1. ==[ original ]==> (ZERO? (SUCCESSOR ZERO))
;     2. ==[ expanded ]==> ((^n.((n (TRUE FALSE)) TRUE))((^n.(^f.(^x.(f ((n f) x)))))(^f.(^x.x))))
;     3. ==[ expanded ]==> ((^n.((n ((^x.(^y.x))(^x.(^y.y))))(^x.(^y.x))))((^n.(^f.(^x.(f ((n f) x)))))(^f.(^x.x))))
;
;        META-VARIABLES EXPANDED.
;
;     1. ==[ start    ]==> ((^n.((n ((^x.(^y.x))(^x.(^y.y))))(^x.(^y.x))))((^n.(^f.(^x.(f ((n f) x)))))(^f.(^x.x))))
;     2. ==[ alpha    ]==> ((^x.((x ((^y.(^z.y))(^u.(^v.v))))(^w.(^p.w))))((^q.(^r.(^x1.(r ((q r) x1)))))(^y1.(^z1.z1))))
;     3. ==[ beta     ]==> ((((^q.(^r.(^x1.(r ((q r) x1)))))(^y1.(^z1.z1)))((^y.(^z.y))(^u.(^v.v))))(^w.(^p.w)))
;     4. ==[ alpha    ]==> ((((^x.(^y.(^z.(y ((x y) z)))))(^u.(^v.v)))((^w.(^p.w))(^q.(^r.r))))(^x1.(^y1.x1)))
;     5. ==[ beta     ]==> (((^y.(^z.(y (((^u.(^v.v)) y) z))))((^w.(^p.w))(^q.(^r.r))))(^x1.(^y1.x1)))
;     6. ==[ alpha    ]==> (((^x.(^y.(x (((^z.(^u.u)) x) y))))((^v.(^w.v))(^p.(^q.q))))(^r.(^x1.r)))
;     7. ==[ beta     ]==> ((^y.(((^v.(^w.v))(^p.(^q.q)))(((^z.(^u.u))((^v.(^w.v))(^p.(^q.q)))) y)))(^r.(^x1.r)))
;     8. ==[ alpha    ]==> ((^x.(((^y.(^z.y))(^u.(^v.v)))(((^w.(^p.p))((^q.(^r.q))(^x1.(^y1.y1)))) x)))(^z1.(^u1.z1)))
;     9. ==[ beta     ]==> (((^y.(^z.y))(^u.(^v.v)))(((^w.(^p.p))((^q.(^r.q))(^x1.(^y1.y1))))(^z1.(^u1.z1))))
;    10. ==[ alpha    ]==> (((^x.(^y.x))(^z.(^u.u)))(((^v.(^w.w))((^p.(^q.p))(^r.(^x1.x1))))(^y1.(^z1.y1))))
;    11. ==[ beta     ]==> ((^y.(^z.(^u.u)))(((^v.(^w.w))((^p.(^q.p))(^r.(^x1.x1))))(^y1.(^z1.y1))))
;    12. ==[ alpha    ]==> ((^x.(^y.(^z.z)))(((^u.(^v.v))((^w.(^p.w))(^q.(^r.r))))(^x1.(^y1.x1))))
;    13. ==[ beta     ]==> (^y.(^z.z))
;    14. ==[ alpha    ]==> (^x.(^y.y))
;
;        REDUCED TO NORMAL FORM.
;

;---------------------------------------------------------------
(setf MULTIPLY '(^ m . (^ n . (^ f . (m (n f))))))

   (expand-and-reduce^ '((MULTIPLY (SUCCESSOR (SUCCESSOR ZERO)))
                                   (SUCCESSOR (SUCCESSOR ZERO)))
                        5000
                        true)
;---------------------------------------------------------------

;
;        EXPANSION AND REDUCTION OF ((MULTIPLY (SUCCESSOR (SUCCESSOR ZERO)))(SUCCESSOR (SUCCESSOR ZERO)))
;
;     1. ==[ original ]==> ((MULTIPLY (SUCCESSOR (SUCCESSOR ZERO)))(SUCCESSOR (SUCCESSOR ZERO)))
;     2. ==[ expanded ]==> (((^m.(^n.(^f.(m (n f)))))((^n.(^f.(^x.(f ((n f) x)))))((^n.(^f.(^x.(f ((n f) x)))))(^f.(^x.x)))))((^n.(^f.(^x.(f ((n f) x)))))((^n.(^f.(^x.(f ((n f) x)))))(^f.(^x.x)))))
;
;        META-VARIABLES EXPANDED.
;
;     1. ==[ start    ]==> (((^m.(^n.(^f.(m (n f)))))((^n.(^f.(^x.(f ((n f) x)))))((^n.(^f.(^x.(f ((n f) x)))))(^f.(^x.x)))))((^n.(^f.(^x.(f ((n f) x)))))((^n.(^f.(^x.(f ((n f) x)))))(^f.(^x.x)))))
;     2. ==[ alpha    ]==> (((^x.(^y.(^z.(x (y z)))))((^u.(^v.(^w.(v ((u v) w)))))((^p.(^q.(^r.(q ((p q) r)))))(^x1.(^y1.y1)))))((^z1.(^u1.(^v1.(u1 ((z1 u1) v1)))))((^w1.(^p1.(^q1.(p1 ((w1 p1) q1)))))(^r1.(^x2.x2)))))
;     3. ==[ beta     ]==> ((^y.(^z.(((^u.(^v.(^w.(v ((u v) w)))))((^p.(^q.(^r.(q ((p q) r)))))(^x1.(^y1.y1))))(y z))))((^z1.(^u1.(^v1.(u1 ((z1 u1) v1)))))((^w1.(^p1.(^q1.(p1 ((w1 p1) q1)))))(^r1.(^x2.x2)))))
;     4. ==[ alpha    ]==> ((^x.(^y.(((^z.(^u.(^v.(u ((z u) v)))))((^w.(^p.(^q.(p ((w p) q)))))(^r.(^x1.x1))))(x y))))((^y1.(^z1.(^u1.(z1 ((y1 z1) u1)))))((^v1.(^w1.(^p1.(w1 ((v1 w1) p1)))))(^q1.(^r1.r1)))))
;     5. ==[ beta     ]==> (^y.(((^z.(^u.(^v.(u ((z u) v)))))((^w.(^p.(^q.(p ((w p) q)))))(^r.(^x1.x1))))(((^y1.(^z1.(^u1.(z1 ((y1 z1) u1)))))((^v1.(^w1.(^p1.(w1 ((v1 w1) p1)))))(^q1.(^r1.r1)))) y)))
;     6. ==[ alpha    ]==> (^x.(((^y.(^z.(^u.(z ((y z) u)))))((^v.(^w.(^p.(w ((v w) p)))))(^q.(^r.r))))(((^x1.(^y1.(^z1.(y1 ((x1 y1) z1)))))((^u1.(^v1.(^w1.(v1 ((u1 v1) w1)))))(^p1.(^q1.q1)))) x)))
;     7. ==[ beta     ]==> (^x.((^z.(^u.(z ((((^v.(^w.(^p.(w ((v w) p)))))(^q.(^r.r))) z) u))))(((^x1.(^y1.(^z1.(y1 ((x1 y1) z1)))))((^u1.(^v1.(^w1.(v1 ((u1 v1) w1)))))(^p1.(^q1.q1)))) x)))
;     8. ==[ alpha    ]==> (^x.((^y.(^z.(y ((((^u.(^v.(^w.(v ((u v) w)))))(^p.(^q.q))) y) z))))(((^r.(^x1.(^y1.(x1 ((r x1) y1)))))((^z1.(^u1.(^v1.(u1 ((z1 u1) v1)))))(^w1.(^p1.p1)))) x)))
;     9. ==[ beta     ]==> (^x.(^z.((((^r.(^x1.(^y1.(x1 ((r x1) y1)))))((^z1.(^u1.(^v1.(u1 ((z1 u1) v1)))))(^w1.(^p1.p1)))) x)((((^u.(^v.(^w.(v ((u v) w)))))(^p.(^q.q)))(((^r.(^x1.(^y1.(x1 ((r x1) y1)))))((^z1.(^u1.(^v1.(u1 ((z1 u1) v1)))))(^w1.(^p1.p1)))) x)) z))))
;    10. ==[ alpha    ]==> (^x.(^y.((((^z.(^u.(^v.(u ((z u) v)))))((^w.(^p.(^q.(p ((w p) q)))))(^r.(^x1.x1)))) x)((((^y1.(^z1.(^u1.(z1 ((y1 z1) u1)))))(^v1.(^w1.w1)))(((^p1.(^q1.(^r1.(q1 ((p1 q1) r1)))))((^x2.(^y2.(^z2.(y2 ((x2 y2) z2)))))(^u2.(^v2.v2)))) x)) y))))
;    11. ==[ beta     ]==> (^x.(^y.(((^u.(^v.(u ((((^w.(^p.(^q.(p ((w p) q)))))(^r.(^x1.x1))) u) v)))) x)((((^y1.(^z1.(^u1.(z1 ((y1 z1) u1)))))(^v1.(^w1.w1)))(((^p1.(^q1.(^r1.(q1 ((p1 q1) r1)))))((^x2.(^y2.(^z2.(y2 ((x2 y2) z2)))))(^u2.(^v2.v2)))) x)) y))))
;    12. ==[ alpha    ]==> (^x.(^y.(((^z.(^u.(z ((((^v.(^w.(^p.(w ((v w) p)))))(^q.(^r.r))) z) u)))) x)((((^x1.(^y1.(^z1.(y1 ((x1 y1) z1)))))(^u1.(^v1.v1)))(((^w1.(^p1.(^q1.(p1 ((w1 p1) q1)))))((^r1.(^x2.(^y2.(x2 ((r1 x2) y2)))))(^z2.(^u2.u2)))) x)) y))))
;    13. ==[ beta     ]==> (^x.(^y.((^u.(x ((((^v.(^w.(^p.(w ((v w) p)))))(^q.(^r.r))) x) u)))((((^x1.(^y1.(^z1.(y1 ((x1 y1) z1)))))(^u1.(^v1.v1)))(((^w1.(^p1.(^q1.(p1 ((w1 p1) q1)))))((^r1.(^x2.(^y2.(x2 ((r1 x2) y2)))))(^z2.(^u2.u2)))) x)) y))))
;    14. ==[ alpha    ]==> (^x.(^y.((^z.(x ((((^u.(^v.(^w.(v ((u v) w)))))(^p.(^q.q))) x) z)))((((^r.(^x1.(^y1.(x1 ((r x1) y1)))))(^z1.(^u1.u1)))(((^v1.(^w1.(^p1.(w1 ((v1 w1) p1)))))((^q1.(^r1.(^x2.(r1 ((q1 r1) x2)))))(^y2.(^z2.z2)))) x)) y))))
;    15. ==[ beta     ]==> (^x.(^y.(x ((((^u.(^v.(^w.(v ((u v) w)))))(^p.(^q.q))) x)((((^r.(^x1.(^y1.(x1 ((r x1) y1)))))(^z1.(^u1.u1)))(((^v1.(^w1.(^p1.(w1 ((v1 w1) p1)))))((^q1.(^r1.(^x2.(r1 ((q1 r1) x2)))))(^y2.(^z2.z2)))) x)) y)))))
;    16. ==[ alpha    ]==> (^x.(^y.(x ((((^z.(^u.(^v.(u ((z u) v)))))(^w.(^p.p))) x)((((^q.(^r.(^x1.(r ((q r) x1)))))(^y1.(^z1.z1)))(((^u1.(^v1.(^w1.(v1 ((u1 v1) w1)))))((^p1.(^q1.(^r1.(q1 ((p1 q1) r1)))))(^x2.(^y2.y2)))) x)) y)))))
;    17. ==[ beta     ]==> (^x.(^y.(x (((^u.(^v.(u (((^w.(^p.p)) u) v)))) x)((((^q.(^r.(^x1.(r ((q r) x1)))))(^y1.(^z1.z1)))(((^u1.(^v1.(^w1.(v1 ((u1 v1) w1)))))((^p1.(^q1.(^r1.(q1 ((p1 q1) r1)))))(^x2.(^y2.y2)))) x)) y)))))
;    18. ==[ alpha    ]==> (^x.(^y.(x (((^z.(^u.(z (((^v.(^w.w)) z) u)))) x)((((^p.(^q.(^r.(q ((p q) r)))))(^x1.(^y1.y1)))(((^z1.(^u1.(^v1.(u1 ((z1 u1) v1)))))((^w1.(^p1.(^q1.(p1 ((w1 p1) q1)))))(^r1.(^x2.x2)))) x)) y)))))
;    19. ==[ beta     ]==> (^x.(^y.(x ((^u.(x (((^v.(^w.w)) x) u)))((((^p.(^q.(^r.(q ((p q) r)))))(^x1.(^y1.y1)))(((^z1.(^u1.(^v1.(u1 ((z1 u1) v1)))))((^w1.(^p1.(^q1.(p1 ((w1 p1) q1)))))(^r1.(^x2.x2)))) x)) y)))))
;    20. ==[ alpha    ]==> (^x.(^y.(x ((^z.(x (((^u.(^v.v)) x) z)))((((^w.(^p.(^q.(p ((w p) q)))))(^r.(^x1.x1)))(((^y1.(^z1.(^u1.(z1 ((y1 z1) u1)))))((^v1.(^w1.(^p1.(w1 ((v1 w1) p1)))))(^q1.(^r1.r1)))) x)) y)))))
;    21. ==[ beta     ]==> (^x.(^y.(x (x (((^u.(^v.v)) x)((((^w.(^p.(^q.(p ((w p) q)))))(^r.(^x1.x1)))(((^y1.(^z1.(^u1.(z1 ((y1 z1) u1)))))((^v1.(^w1.(^p1.(w1 ((v1 w1) p1)))))(^q1.(^r1.r1)))) x)) y))))))
;    22. ==[ alpha    ]==> (^x.(^y.(x (x (((^z.(^u.u)) x)((((^v.(^w.(^p.(w ((v w) p)))))(^q.(^r.r)))(((^x1.(^y1.(^z1.(y1 ((x1 y1) z1)))))((^u1.(^v1.(^w1.(v1 ((u1 v1) w1)))))(^p1.(^q1.q1)))) x)) y))))))
;    23. ==[ beta     ]==> (^x.(^y.(x (x ((^u.u)((((^v.(^w.(^p.(w ((v w) p)))))(^q.(^r.r)))(((^x1.(^y1.(^z1.(y1 ((x1 y1) z1)))))((^u1.(^v1.(^w1.(v1 ((u1 v1) w1)))))(^p1.(^q1.q1)))) x)) y))))))
;    24. ==[ alpha    ]==> (^x.(^y.(x (x ((^z.z)((((^u.(^v.(^w.(v ((u v) w)))))(^p.(^q.q)))(((^r.(^x1.(^y1.(x1 ((r x1) y1)))))((^z1.(^u1.(^v1.(u1 ((z1 u1) v1)))))(^w1.(^p1.p1)))) x)) y))))))
;    25. ==[ beta     ]==> (^x.(^y.(x (x ((((^u.(^v.(^w.(v ((u v) w)))))(^p.(^q.q)))(((^r.(^x1.(^y1.(x1 ((r x1) y1)))))((^z1.(^u1.(^v1.(u1 ((z1 u1) v1)))))(^w1.(^p1.p1)))) x)) y)))))
;    26. ==[ alpha    ]==> (^x.(^y.(x (x ((((^z.(^u.(^v.(u ((z u) v)))))(^w.(^p.p)))(((^q.(^r.(^x1.(r ((q r) x1)))))((^y1.(^z1.(^u1.(z1 ((y1 z1) u1)))))(^v1.(^w1.w1)))) x)) y)))))
;    27. ==[ beta     ]==> (^x.(^y.(x (x (((^u.(^v.(u (((^w.(^p.p)) u) v))))(((^q.(^r.(^x1.(r ((q r) x1)))))((^y1.(^z1.(^u1.(z1 ((y1 z1) u1)))))(^v1.(^w1.w1)))) x)) y)))))
;    28. ==[ alpha    ]==> (^x.(^y.(x (x (((^z.(^u.(z (((^v.(^w.w)) z) u))))(((^p.(^q.(^r.(q ((p q) r)))))((^x1.(^y1.(^z1.(y1 ((x1 y1) z1)))))(^u1.(^v1.v1)))) x)) y)))))
;    29. ==[ beta     ]==> (^x.(^y.(x (x ((^u.((((^p.(^q.(^r.(q ((p q) r)))))((^x1.(^y1.(^z1.(y1 ((x1 y1) z1)))))(^u1.(^v1.v1)))) x)(((^v.(^w.w))(((^p.(^q.(^r.(q ((p q) r)))))((^x1.(^y1.(^z1.(y1 ((x1 y1) z1)))))(^u1.(^v1.v1)))) x)) u))) y)))))
;    30. ==[ alpha    ]==> (^x.(^y.(x (x ((^z.((((^u.(^v.(^w.(v ((u v) w)))))((^p.(^q.(^r.(q ((p q) r)))))(^x1.(^y1.y1)))) x)(((^z1.(^u1.u1))(((^v1.(^w1.(^p1.(w1 ((v1 w1) p1)))))((^q1.(^r1.(^x2.(r1 ((q1 r1) x2)))))(^y2.(^z2.z2)))) x)) z))) y)))))
;    31. ==[ beta     ]==> (^x.(^y.(x (x ((((^u.(^v.(^w.(v ((u v) w)))))((^p.(^q.(^r.(q ((p q) r)))))(^x1.(^y1.y1)))) x)(((^z1.(^u1.u1))(((^v1.(^w1.(^p1.(w1 ((v1 w1) p1)))))((^q1.(^r1.(^x2.(r1 ((q1 r1) x2)))))(^y2.(^z2.z2)))) x)) y))))))
;    32. ==[ alpha    ]==> (^x.(^y.(x (x ((((^z.(^u.(^v.(u ((z u) v)))))((^w.(^p.(^q.(p ((w p) q)))))(^r.(^x1.x1)))) x)(((^y1.(^z1.z1))(((^u1.(^v1.(^w1.(v1 ((u1 v1) w1)))))((^p1.(^q1.(^r1.(q1 ((p1 q1) r1)))))(^x2.(^y2.y2)))) x)) y))))))
;    33. ==[ beta     ]==> (^x.(^y.(x (x (((^u.(^v.(u ((((^w.(^p.(^q.(p ((w p) q)))))(^r.(^x1.x1))) u) v)))) x)(((^y1.(^z1.z1))(((^u1.(^v1.(^w1.(v1 ((u1 v1) w1)))))((^p1.(^q1.(^r1.(q1 ((p1 q1) r1)))))(^x2.(^y2.y2)))) x)) y))))))
;    34. ==[ alpha    ]==> (^x.(^y.(x (x (((^z.(^u.(z ((((^v.(^w.(^p.(w ((v w) p)))))(^q.(^r.r))) z) u)))) x)(((^x1.(^y1.y1))(((^z1.(^u1.(^v1.(u1 ((z1 u1) v1)))))((^w1.(^p1.(^q1.(p1 ((w1 p1) q1)))))(^r1.(^x2.x2)))) x)) y))))))
;    35. ==[ beta     ]==> (^x.(^y.(x (x ((^u.(x ((((^v.(^w.(^p.(w ((v w) p)))))(^q.(^r.r))) x) u)))(((^x1.(^y1.y1))(((^z1.(^u1.(^v1.(u1 ((z1 u1) v1)))))((^w1.(^p1.(^q1.(p1 ((w1 p1) q1)))))(^r1.(^x2.x2)))) x)) y))))))
;    36. ==[ alpha    ]==> (^x.(^y.(x (x ((^z.(x ((((^u.(^v.(^w.(v ((u v) w)))))(^p.(^q.q))) x) z)))(((^r.(^x1.x1))(((^y1.(^z1.(^u1.(z1 ((y1 z1) u1)))))((^v1.(^w1.(^p1.(w1 ((v1 w1) p1)))))(^q1.(^r1.r1)))) x)) y))))))
;    37. ==[ beta     ]==> (^x.(^y.(x (x (x ((((^u.(^v.(^w.(v ((u v) w)))))(^p.(^q.q))) x)(((^r.(^x1.x1))(((^y1.(^z1.(^u1.(z1 ((y1 z1) u1)))))((^v1.(^w1.(^p1.(w1 ((v1 w1) p1)))))(^q1.(^r1.r1)))) x)) y)))))))
;    38. ==[ alpha    ]==> (^x.(^y.(x (x (x ((((^z.(^u.(^v.(u ((z u) v)))))(^w.(^p.p))) x)(((^q.(^r.r))(((^x1.(^y1.(^z1.(y1 ((x1 y1) z1)))))((^u1.(^v1.(^w1.(v1 ((u1 v1) w1)))))(^p1.(^q1.q1)))) x)) y)))))))
;    39. ==[ beta     ]==> (^x.(^y.(x (x (x (((^u.(^v.(u (((^w.(^p.p)) u) v)))) x)(((^q.(^r.r))(((^x1.(^y1.(^z1.(y1 ((x1 y1) z1)))))((^u1.(^v1.(^w1.(v1 ((u1 v1) w1)))))(^p1.(^q1.q1)))) x)) y)))))))
;    40. ==[ alpha    ]==> (^x.(^y.(x (x (x (((^z.(^u.(z (((^v.(^w.w)) z) u)))) x)(((^p.(^q.q))(((^r.(^x1.(^y1.(x1 ((r x1) y1)))))((^z1.(^u1.(^v1.(u1 ((z1 u1) v1)))))(^w1.(^p1.p1)))) x)) y)))))))
;    41. ==[ beta     ]==> (^x.(^y.(x (x (x ((^u.(x (((^v.(^w.w)) x) u)))(((^p.(^q.q))(((^r.(^x1.(^y1.(x1 ((r x1) y1)))))((^z1.(^u1.(^v1.(u1 ((z1 u1) v1)))))(^w1.(^p1.p1)))) x)) y)))))))
;    42. ==[ alpha    ]==> (^x.(^y.(x (x (x ((^z.(x (((^u.(^v.v)) x) z)))(((^w.(^p.p))(((^q.(^r.(^x1.(r ((q r) x1)))))((^y1.(^z1.(^u1.(z1 ((y1 z1) u1)))))(^v1.(^w1.w1)))) x)) y)))))))
;    43. ==[ beta     ]==> (^x.(^y.(x (x (x (x (((^u.(^v.v)) x)(((^w.(^p.p))(((^q.(^r.(^x1.(r ((q r) x1)))))((^y1.(^z1.(^u1.(z1 ((y1 z1) u1)))))(^v1.(^w1.w1)))) x)) y))))))))
;    44. ==[ alpha    ]==> (^x.(^y.(x (x (x (x (((^z.(^u.u)) x)(((^v.(^w.w))(((^p.(^q.(^r.(q ((p q) r)))))((^x1.(^y1.(^z1.(y1 ((x1 y1) z1)))))(^u1.(^v1.v1)))) x)) y))))))))
;    45. ==[ beta     ]==> (^x.(^y.(x (x (x (x ((^u.u)(((^v.(^w.w))(((^p.(^q.(^r.(q ((p q) r)))))((^x1.(^y1.(^z1.(y1 ((x1 y1) z1)))))(^u1.(^v1.v1)))) x)) y))))))))
;    46. ==[ alpha    ]==> (^x.(^y.(x (x (x (x ((^z.z)(((^u.(^v.v))(((^w.(^p.(^q.(p ((w p) q)))))((^r.(^x1.(^y1.(x1 ((r x1) y1)))))(^z1.(^u1.u1)))) x)) y))))))))
;    47. ==[ beta     ]==> (^x.(^y.(x (x (x (x (((^u.(^v.v))(((^w.(^p.(^q.(p ((w p) q)))))((^r.(^x1.(^y1.(x1 ((r x1) y1)))))(^z1.(^u1.u1)))) x)) y)))))))
;    48. ==[ alpha    ]==> (^x.(^y.(x (x (x (x (((^z.(^u.u))(((^v.(^w.(^p.(w ((v w) p)))))((^q.(^r.(^x1.(r ((q r) x1)))))(^y1.(^z1.z1)))) x)) y)))))))
;    49. ==[ beta     ]==> (^x.(^y.(x (x (x (x ((^u.u) y)))))))
;    50. ==[ alpha    ]==> (^x.(^y.(x (x (x (x ((^z.z) y)))))))
;    51. ==[ beta     ]==> (^x.(^y.(x (x (x (x y))))))
;
;        REDUCED TO NORMAL FORM.
;

;---------------------------------------------------------------
(setf PREDECESSOR '(^ n . (((n (^ p . (^ z . ((z (SUCCESSOR (p TRUE)))
                                              (p TRUE)))))
                             (^ z . ((z ZERO) ZERO)))
                           FALSE)))

    (expand-and-reduce^ '(PREDECESSOR ONE)
                        5000
                        true)
;---------------------------------------------------------------

;
;        EXPANSION AND REDUCTION OF (PREDECESSOR ONE)
;
;     1. ==[ original ]==> (PREDECESSOR ONE)
;     2. ==[ expanded ]==> ((^n.(((n (^p.(^z.((z (SUCCESSOR (p TRUE)))(p TRUE)))))(^z.((z ZERO) ZERO))) FALSE))(^x.x))
;     3. ==[ expanded ]==> ((^n.(((n (^p.(^z.((z ((^n.(^f.(^x.(f ((n f) x)))))(p (^x.(^y.x)))))(p (^x.(^y.x)))))))(^z.((z (^f.(^x.x)))(^f.(^x.x)))))(^x.(^y.y))))(^x.x))
;
;        META-VARIABLES EXPANDED.
;
;     1. ==[ start    ]==> ((^n.(((n (^p.(^z.((z ((^n.(^f.(^x.(f ((n f) x)))))(p (^x.(^y.x)))))(p (^x.(^y.x)))))))(^z.((z (^f.(^x.x)))(^f.(^x.x)))))(^x.(^y.y))))(^x.x))
;     2. ==[ alpha    ]==> ((^x.(((x (^y.(^z.((z ((^u.(^v.(^w.(v ((u v) w)))))(y (^p.(^q.p)))))(y (^r.(^x1.r)))))))(^y1.((y1 (^z1.(^u1.u1)))(^v1.(^w1.w1)))))(^p1.(^q1.q1))))(^r1.r1))
;     3. ==[ beta     ]==> ((((^r1.r1)(^y.(^z.((z ((^u.(^v.(^w.(v ((u v) w)))))(y (^p.(^q.p)))))(y (^r.(^x1.r)))))))(^y1.((y1 (^z1.(^u1.u1)))(^v1.(^w1.w1)))))(^p1.(^q1.q1)))
;     4. ==[ alpha    ]==> ((((^x.x)(^y.(^z.((z ((^u.(^v.(^w.(v ((u v) w)))))(y (^p.(^q.p)))))(y (^r.(^x1.r)))))))(^y1.((y1 (^z1.(^u1.u1)))(^v1.(^w1.w1)))))(^p1.(^q1.q1)))
;     5. ==[ beta     ]==> (((^y.(^z.((z ((^u.(^v.(^w.(v ((u v) w)))))(y (^p.(^q.p)))))(y (^r.(^x1.r))))))(^y1.((y1 (^z1.(^u1.u1)))(^v1.(^w1.w1)))))(^p1.(^q1.q1)))
;     6. ==[ alpha    ]==> (((^x.(^y.((y ((^z.(^u.(^v.(u ((z u) v)))))(x (^w.(^p.w)))))(x (^q.(^r.q))))))(^x1.((x1 (^y1.(^z1.z1)))(^u1.(^v1.v1)))))(^w1.(^p1.p1)))
;     7. ==[ beta     ]==> ((^y.((y ((^z.(^u.(^v.(u ((z u) v)))))((^x1.((x1 (^y1.(^z1.z1)))(^u1.(^v1.v1))))(^w.(^p.w)))))((^x1.((x1 (^y1.(^z1.z1)))(^u1.(^v1.v1))))(^q.(^r.q)))))(^w1.(^p1.p1)))
;     8. ==[ alpha    ]==> ((^x.((x ((^y.(^z.(^u.(z ((y z) u)))))((^v.((v (^w.(^p.p)))(^q.(^r.r))))(^x1.(^y1.x1)))))((^z1.((z1 (^u1.(^v1.v1)))(^w1.(^p1.p1))))(^q1.(^r1.q1)))))(^x2.(^y2.y2)))
;     9. ==[ beta     ]==> (((^x2.(^y2.y2))((^y.(^z.(^u.(z ((y z) u)))))((^v.((v (^w.(^p.p)))(^q.(^r.r))))(^x1.(^y1.x1)))))((^z1.((z1 (^u1.(^v1.v1)))(^w1.(^p1.p1))))(^q1.(^r1.q1))))
;    10. ==[ alpha    ]==> (((^x.(^y.y))((^z.(^u.(^v.(u ((z u) v)))))((^w.((w (^p.(^q.q)))(^r.(^x1.x1))))(^y1.(^z1.y1)))))((^u1.((u1 (^v1.(^w1.w1)))(^p1.(^q1.q1))))(^r1.(^x2.r1))))
;    11. ==[ beta     ]==> ((^y.y)((^u1.((u1 (^v1.(^w1.w1)))(^p1.(^q1.q1))))(^r1.(^x2.r1))))
;    12. ==[ alpha    ]==> ((^x.x)((^y.((y (^z.(^u.u)))(^v.(^w.w))))(^p.(^q.p))))
;    13. ==[ beta     ]==> ((^y.((y (^z.(^u.u)))(^v.(^w.w))))(^p.(^q.p)))
;    14. ==[ alpha    ]==> ((^x.((x (^y.(^z.z)))(^u.(^v.v))))(^w.(^p.w)))
;    15. ==[ beta     ]==> (((^w.(^p.w))(^y.(^z.z)))(^u.(^v.v)))
;    16. ==[ alpha    ]==> (((^x.(^y.x))(^z.(^u.u)))(^v.(^w.w)))
;    17. ==[ beta     ]==> ((^y.(^z.(^u.u)))(^v.(^w.w)))
;    18. ==[ alpha    ]==> ((^x.(^y.(^z.z)))(^u.(^v.v)))
;    19. ==[ beta     ]==> (^y.(^z.z))
;    20. ==[ alpha    ]==> (^x.(^y.y))
;
;        REDUCED TO NORMAL FORM.
;

;---------------------------------------------------------------

(setf FACTORIAL '(Y (^ f . (^ n .((((IF ZERO?) n) ONE)
                                   ((MULTIPLY n) (f (PREDECESSOR n))))))))

  (expand-and-reduce^ '(FACTORIAL (SUCCESSOR (SUCCESSOR ONE)))
                       5000
                       true)
;---------------------------------------------------------------

;
; Roughly ten minutes and 100000 of lines later, on my computer
;
; ...
;
; 2379. ==[ beta     ]==> (^x.(^y.(x (x (x (x (x (x ((^u.u) y)))))))))
; 2380. ==[ alpha    ]==> (^x.(^y.(x (x (x (x (x (x ((^z.z) y)))))))))
; 2381. ==[ beta     ]==> (^x.(^y.(x (x (x (x (x (x y))))))))
;
;       REDUCED TO NORMAL FORM.
;

;---------------------------------------------------------------
; EVERYTHING WORKS!

(exit)

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

2011-01-31T19:10:00.005+01:00

; 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 "formal system". One
; who performs reductions - human or computer - can pick order
; by any criteria.
;
;
;     4.2. Lisp evaluation strategy is not best for
;                     lambda-calculus
;
;
; In Lisp, orther 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).

2011-01-29T13:51:00.021+01:00

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

2011-01-25T14:28:00.003+01:00

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?

2011-01-24T10:51:00.001+01:00

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?

2011-01-23T14:34:00.002+01:00

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.

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.

2011-01-22T04:36:00.016+01:00

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