Calchylus module examples

This is a Jupyter Notebook document introducing features, usage, and behaviour of calchylus module.

Calchylus module is a Lambda calculus evaluator written with Hy by Marko Manninen, 2017.

For full documentation see: http://calchylus.readthedocs.io

System configuration

First, let us see, what is the environment I'm running these examples:



In [1]:

    
(import hy sys)
(print (% "Hy version: %s" hy.__version__))
(print (% "Python %s" sys.version))









    



Hy version: 0.13.0
Python 3.6.2 | packaged by conda-forge | (default, Jul 23 2017, 22:58:45) [MSC v.1900 64 bit (AMD64)]

Download Calchylus

The next step is to download and install calchylus module from PyPi:

pip install calchylus

When that is done, we can run Hy and check calchylus module version:



In [2]:

    
(import calchylus)
(print (% "Hy version: %s" calchylus.__version__))









    



Hy version: v0.1.13

Import main evaluator

Finally, import calchylus module and initialize calchylus system by one of the with- macros:



In [3]:

    
(require (calchylus.lambdas [*]))
(with-alpha-conversion-and-macros 𝜆 \.)









    Out[3]:





<function <lambda> at 0x00000279ABA186A8>

Pretty print

For printing mathematical symbols nicely in the Jupyter Notebook document, I have defined some helper functions to the module. Note that these are not necessary for the Lambda calculus evaluation itself:

#§ pretty print Lambda expression as it is
#¤ pretty print Lambda expression and beta-reduced form of the expression
latex-output print quoted expressions (useful, when working with Lambda expression as a Hy variable)

Three components

Lambda expressions are formed by three components: variables, function abstractions, and function applications.

Variable is any symbol or Lambda expression that will acts as a parameter for the function. In pure untyped Lambda calculus, symbols do not have any special meaning or type by they own. Meaning is extracted from the functional application. Untyped systems have some advantages related to universality but that usually comes with a performance penalty.

Calchylus is far from being beneficial for heavy arithmetic processing. Rather, it is meant for inspecting theoretical foundations of arithmetics, programming languages, and logic.

Function abstraction consists of:

a function identifier, usually denoted by a Greek lambda letter 𝜆 or λ
an argument and a body delimitted by a symbol that is usually a dot . or a middle dot ·
parentheses for grouping an abstraction (and possibly body components) () or sometimes []

Due to the fact, that a dot belongs to the reserved symbols in Hy language, a dot will be escaped in the following examples like this: `\.`

Traditionally, Lambda function must have one and only one argument. At first, this seems very restricting, but in reality with a technique called currying multiary functions can be constructed. In other words, any number of arguments can be transformed to the single argument style expressions, and vice versa.

The body of the function will be the first expression after the delimitter. Body expression can be a parenthezised set of symbols or just a single symbol, where parentheses or a space before and after the symbol indicates the start and the end of the body.

Function application is a function abstraction together with an applicable variable / parameter. In many programming languages this is same as defining an anonymous function and applying it to the given argument(s).

Identity function

Let us start the lengthy introduction to the Lambda functions and define the function abstraction first. The following function is one of the simplest ones. It is called the identity function and has one argument x and a simple body x:



In [4]:

    
(𝜆 x \. x)









    Out[4]:





'(𝜆 x . x)'

In calchylus we need to have parentheses around the expression due to LISP like language specification of Hy. In common Lambda notation the outermost parentheses are often removed and the identity function is denoted similar to this:



In [5]:

    
#§(𝜆 x \. x)









    Out[5]:





$$\\\large 𝜆\ x\ .\ x\\$$

In native Hy, the identity function is constructed by an anonymous function accordingly:



In [6]:

    
(fn [x] x)









    Out[6]:





<function <lambda> at 0x00000279AA6B21E0>

We realize easily, that the difference between the anonymous function in Hy and the function abstraction in Lambda calculus is rather semantical so far. Lambda function indicator is fn (was actually the word lambda in the earlier versions of Hy). Arguments are inside brackets, because a function definition in Hy supports more complex argument initialization compared to the pure Lambda calculus. The rest of the expression is the body of the function.

The function abstraction, or you could call it a function definition, is waiting for one argument. And then, if an argument is given, the identity function simply "returns" the very same argument value intact.

In the function application, the identity function is applied to the given argument. You could say that the function abstraction is functioning only in the function application.

Passing parameters

There are actually two possible ways to pass parameters to the function in calchylus module.

by wrapping a function with parentheses and leaving the parameter outside of the wrapper
introducing a parameter inside a function as the last element after the body

Let us see, how the function application looks like in the first case:



In [7]:

    
#§((𝜆 x \. x) y)









    Out[7]:





$$\\\large (𝜆\ x\ .\ x)\ y\\$$

In case 2., the expression looks like this:



In [8]:

    
#§(𝜆 x \. x y)









    Out[8]:





$$\\\large 𝜆\ x\ .\ x\ y\\$$

Again, we can see a close resemblance to the native anonymous function in Hy. One could transform the above Lambda expression to the Hy code like this:

((fn [x] x) 'y)

Furthermore, there is a close resemblance with a Lambda calculus notation and a mathematical notation for the function definition.

Mathematical notation

For a demonstration, let us change the function identifier and the delimitter with calchylus module initializer macro and try the function abstraction again:



In [9]:

    
(with-alpha-conversion-and-macros ƒ: ↦)
#§(ƒ: x ↦ x)









    Out[9]:





$$\\\large ƒ:\ x\ ↦\ x\\$$

We are pretty close to the formal mathematical representation#Notation) of the function. We could even use a special escape character as a function identifier to leave out the from the visual presentation of the Lambda expression in the Jupyter Notebook environment:



In [10]:

    
(with-alpha-conversion-and-macros \ ↦)
#§(\ x ↦ x)









    Out[10]:





$$\\\large x\ ↦\ x\\$$

Evaluation

Calchylus module is not just for presenting Lambda calculus notation in different forms, but also for evaluation (beta-reduction) of the Lambda expressions. Evaluation process has some principles that are good to know:

evaluation process starts, when a parameter is given to the function abstraction
evaluation starts from the left-most parameter that is passed to the left-most function in the same level
evaluation continues passing free parameters from the left to the functions according to the principle 2.
when the normal form of the expression is achieved, meaning it cannot be further reduced, then reduction is once more started for sub expressions of the normal form, until head normal form is achieved

Consequence of this is that:

parameters are substituted to the body before they are evaluated

These principles all together are called call-by-value strategy or applicative order which is an important concept. It leads to the lazy evaluation contra to the most of the programming languages that eagerly evaluates parameters first before sending them to the function.

The last principle we have already seen in action is:

if evaluation reduces to the function abstration that can't be reduced anymore, then the function abstraction is returned as a final form

Otherwise we have a result where all arguments and parameters of the expression has been substituted.

Let us first see, how the identity function is applied to the parameter in a native Hy way:



In [11]:

    
((fn [x] x) 'y)









    Out[11]:





'y'

Note that there already is the identity function that you could also use in Hy: `(identity 'y)`

Now, compare that to the corresponding Lambda expression in the following example:



In [12]:

    
(with-alpha-conversion-and-macros λ \.)
#¤(λ x \. x y)









    Out[12]:





$$\\\large λ\ x\ .\ x\ y\\\large=_{\beta} \\\large y\\$$

This time both the original expression and the evaluated result are printed and their beta-reduced equality is indicated with $=_{β}$ symbol.

Shorthands

calchylus module provides a plenty of shorthands for common Lambda forms. IDENT is for the identity function and can be used in this manner:



In [13]:

    
#¤(IDENT y)









    Out[13]:





$$\\\large λ\ a\ .\ a\ y\\\large=_{\beta} \\\large y\\$$

We see that the argument name is a in this example, but the result is same (y) with the previous example. In Lambda calculus λ x . x and λ a . a are regarded as equal forms. The name of the argument can be anything because it is consistently used and substituted in the process of evaluation.

So far we have kept everything as simple as possible. The identity function is good for introducing basics elements of the Lambda calculus. Althought the identity function looks too simple for any real usage other than demonstration, or conceptual talk, it is good to remember that the predecessor function (PRED) fully utilizes it.

Before going deeper to the arithmetics, let's introduce one exciting property of the Lambda calculus, namely, higher-order functions.

Higher-order functions

When we really start to play with functions, there comes a moment, where you probably happened to pass a function to the function, or at least you wondered what happens, if you do so.

So, what happens when you apply the identity function to the identity function? In calchylus, we can investigate it with the next piece of code:



In [14]:

    
#¤(IDENT IDENT)









    Out[14]:





$$\\\large λ\ a\ .\ a\ (λ\ a\ .\ a)\\\large=_{\beta} \\\large λ\ a\ .\ a\\$$

If the identity function is given to the identity function, it returns (or beta-reduces to) the identity function. Returned function is an abstraction in this case and can't be reduced further. On the other hand, this means that we could pass a parameter to the result, which is exactly what we do next:



In [15]:

    
#¤((IDENT IDENT) y)









    Out[15]:





$$\\\large (λ\ a\ .\ a\ (λ\ a\ .\ a))\ y\\\large=_{\beta} \\\large y\\$$

With this simple maneuver we have moved to the realms of the higher-order functions. It means ability to send functions inside functions (apply functions to functions), or define nested functions, sometimes called functors.

Let us do one more thing with the identity function before moving on to the concepts of constants, scopes, and variable shadowing.

In the next example, rather than passing a function to the function, we construct the body of the function to be the identity function per se:



In [16]:

    
#¤((λ b \. IDENT b) y)









    Out[16]:





$$\\\large (λ\ b\ .\ (λ\ a\ .\ a)\ b)\ y\\\large=_{\beta} \\\large y\\$$

Again the result is y, maybe after a little bit twisting first.

This is a good place to take a breath before diving deeper to the variable substitution topic.

Constant function

Variable is an object, which value is changing. Constant is a value, that should keep static and permanent. In Lambda calculus it is possible to imitate constants by function notation. We simply take one parameter for the function argument, but don't use it at all. Instead a static body is returned. Say the function has an argument foo and the body bar in the following way:



In [17]:

    
(λ foo \. bar)









    Out[17]:





'(λ foo . bar)'

If any parameter, like baz, is passed to the function, it should stubbornly return the body bar:



In [18]:

    
(λ foo \. bar baz)









    Out[18]:





'bar'

In calchylus module we have a CONST macro to create constants. In practice we need to specify the argument name and the body separately because we can't have both using same symbol:



In [19]:

    
(CONST foo bar)









    Out[19]:





'(λ foo . bar)'

If the argument anme and the body is same symbol, then result is an identity function! Let's try once more the evaluated version of the constant with parameter baz:



In [20]:

    
#¤(CONST foo bar baz)









    Out[20]:





$$\\\large λ\ foo\ .\ bar\ baz\\\large=_{\beta} \\\large bar\\$$

`LET` and `LET*`

We have talked about variables, arguments, parameters, and constants. These terms are sometimes used interchangeably depending on what language level they are referring. calchylus module implementation, for example, has to protect argument names with automated variable name generation.

But if we talk in the level of calchylus module interface rather than implementation, with the variable term we refer to the LET and LET* constructors. Once again, these are macro shorthands or abbreviations for constructing certain Lambda expressions, namely variables. This time I want to show, althougt awfully late, the famous "Hello World" example:



In [21]:

    
#¤(LET x "World" (Hello, x !))









    Out[21]:





$$\\\large λ\ x\ .\ (Hello,\ x\ !)\ World\\\large=_{\beta} \\\large Hello,\ World\ !\\$$

Here (Hello, x !) is the function body. x is the argument name and World is the parameter. As a combination, because x is meant for a changing value, we have defined a variable x.

Multiple arguments

...

Scopes

It has become obvious now that the main operation in Lambda calculus is a substitution of argument names in the function body with the parameters given to the function application. Our examples has been easy so far. Natural question is, how substitution works when there are many nested functions, possibly with same argument names?

Well, every function also works as a scope to the arguments inside the function. So, every argument that is inside the body will get substituted until there is another function with same argument name. In that case, a function works as a protector and prevents for further substitution.

Let us see two exampless for this.

substitution over nested Lambda terms



In [22]:

    
#¤(λ x \. (λ y \. x) z)









    Out[22]:





$$\\\large λ\ x\ .\ (λ\ y\ .\ x)\ z\\\large=_{\beta} \\\large λ\ y\ .\ z\\$$

Note how x in the inner Lambda expression (λ y . x) got substituted by z.

substitution protected by argument shadowing



In [23]:

    
#¤(λ x \. (λ x \. x) z)









    Out[23]:





$$\\\large λ\ x\ .\ (λ\ x\ .\ x)\ z\\\large=_{\beta} \\\large λ\ x\ .\ x\\$$

Defining argument x again in the inner Lambda term (λ x . x) we have prevented substitution of x to take place anymore.

Collision detection

Let us then think of the possibility that the first parameter value y is same as the name of the argument of the inner function in the following manner:



In [24]:

    
#¤(λ x \. (λ y \. (x y)) y)









    Out[24]:





$$\\\large λ\ x\ .\ (λ\ y\ .\ (x\ y))\ y\\\large=_{\beta} \\\large λ\ y\ .\ (y\ y)\\$$

So far so good. Or is it really? What happens or should happen, if you pass a second parameter to the function abstraction we have left?

We can easily investigate it with calchylus module:



In [25]:

    
#¤(λ x \. (λ y \. (x y)) y z)









    Out[25]:





$$\\\large λ\ x\ .\ (λ\ y\ .\ (x\ y))\ y\ z\\\large=_{\beta} \\\large y\ z\\$$

Are you surprised, that the result is y z?

Name resolution

The standard convention in Lambda calculus is that argument names should be stable when they have been bound to the variables. When the first argument x has been substituted to the sub terms in the body with y, value of y should not change anymore.

Stableness is achieved by a process called alpha conversion which is happening behind the curtain in calchylus module. Argument names are changed momentarily to generated unique names so that they cannot overlap.

In calchylus module, however, we can switch on and off the alpha conversion phase and investigate, what happens if names get collided:



In [26]:

    
(with-alpha-conversion-nor-macros λ \.)
#¤(λ x \. (λ y \. (x y)) y z)









    Out[26]:





$$\\\large λ\ x\ .\ (λ\ y\ .\ (x\ y))\ y\ z\\\large=_{\beta} \\\large z\ z\\$$

This is set purely for inspection and not recommended as a real evaluation strategy. It can be shown that only with unique selection of names, real arithmetics can be achieved in Lambda calculus. Other way around the problem would be to introduce compile or run time exception system and tell the programmer, that there is a collision of variable names. That could indeed effect positively to the evaluation time of the program on the other hand, because in the final program, there would be no need for the alpha conversion!

For curious minds, this is what happens inside the module on the alpha conversion process:



In [27]:

    
(alpha-conversion '(λ x \. (λ y \. (x y)) y z))









    Out[27]:





['λ', :x_1257, '\\.', ['λ', :y_1258, '\\.', (:x_1257 :y_1258)], 'y', 'z']

More variables

Earlier we created a variable with LET macro. I didn't note yet that it is possible to construct several variables at once with that macro. Variable names and values must come in pairs and the last argument of the macro should be the body, where arguments are used.

Using this feature, I want to present other possible way of twisting variables. Here the first variable a is re-used in the second variable b:



In [28]:

    
(with-alpha-conversion-and-macros λ \.)
#¤(LET a c b a (a b))









    Out[28]:





$$\\\large λ\ a\ b\ .\ (a\ b)\ c\ a\\\large=_{\beta} \\\large c\ a\\$$

It seems that we are not quite getting it. LET macro made the Lambda expression (λ a b . (a b) c a) but someone might have expected that the value of variable b is same as the value of variable a. But we only got the name of the symbol a for b. It occures that it is not possible to use the value of arguments in the other following arguments.

But it is with other variable constructor, namely LET* macro. It works same way than LET but allows to use values of arguments in the other arguments, rather than only in the body of the function.



In [29]:

    
#¤(LET* a c b a (a b))









    Out[29]:





$$\\\large λ\ a\ .\ (λ\ b\ .\ (a\ b)\ a)\ c\\\large=_{\beta} \\\large c\ c\\$$

Notice, that the Lambda form is also a bit different in structure. We have actually shown that it is possible to present variable setters purely functional way. This may become as a small surprise for many programmer. We have created something that looks like causing all hatred side effects but is rather nullipotent in its true nature.

DO imperative

We can even do better and tremble the foundations and concepts of two different paradigms, the functional and imperative ones.

In calchylus there is a DO shorthand to alter the very same functionality that we already saw in LET and LET*. DO practically lets you to define variables with LET's and leave the final function body "outside" the LET macros.

By the next example we shall take one step closer to the next big area, where Lambda calculus is still studied and where Lambda calculus was primarily and originally intended to be used, as a universal mathematical language:



In [30]:

    
#¤
(DO
  (LET a 2)
  (LET b 3)
  (a ^ b + b ^ a))









    Out[30]:





$$\\\large λ\ a\ .\ (λ\ b\ .\ (a^ b\ +\ b^ a)\ 3)\ 2\\\large=_{\beta} \\\large 2^ 3\ +\ 3^ 2\\$$

If Lambda calculus is so great, why I am not showing the final result of the equation? The reason is, that symbols given, even they look like numbers (2, 3) and the addition (+), have no real meaning in Lambda calculus. They are just symbols to be substituted to the places where arguments are in the body.

In Lambda calculus we have to and try to construct everything from the three basic principles and substitution convention. So how should we present numbers, or the more basic boolean values then?

Boolean values

Curry Howard barber tale...



In [31]:

    
;(with-alpha-conversion-and-macros ƒ ↦)
;(setv c '(LET* x 2 y 2 a b b c (a ^ x b ^ y)))
;(macro-print c :result True)



In [32]:

    
(TRUE)









    Out[32]:





'(λ a . (λ b . a))'



In [ ]:



In [33]:

    
;(with-alpha-conversion-and-macros L ,)
;(APP (L a , (L b , e a) 1))
;(print (APP (((L a , (L b , e)) 1) 2)))



In [ ]:



In [34]:

    
; to be used like: #ℕ17 / #ℕ 17 -> (NUM 17) -> (L x , (L y , (x (x ..... (x y)))))
;(defsharp ℕ [n] `(NUM ~n))
;#ℕ 17



In [35]:

    
(with-macros L ,)
(L a , (L b , (L c , (a b c) b) a) 1)









    Out[35]:





'(1 1 1)'



In [36]:

    
(with-alpha-conversion-and-macros L ,)
(LET* a 1 b a c b (a b c))









    Out[36]:





'(1 1 1)'



In [37]:

    
(APP (x ((L x , x) y)))









    Out[37]:





'(x y)'



In [38]:

    
(L x , (L y , (L z , (x y z))) 1 2 3)









    Out[38]:





'(1 2 3)'



In [39]:

    
(L x y , (L z a , (x y z a)) 1 2 3 4)









    Out[39]:





'(1 2 3 4)'



In [40]:

    
;(macro-print '(SUMMATION THREE) 'small)

DOs



In [41]:

    
;(macro-print '(DO (LET a (𝜆 a b · a)) (LET b (𝜆 a b · b)) (a b)))



In [42]:

    
(APP (𝜆 a b · a (𝜆 a b · b)))









    Out[42]:





'(𝜆 a b · a (𝜆 a b · b))'



In [43]:

    
(with-alpha-conversion-and-macros 𝜆 ·)
(DO (LET a (𝜆 a b · a)) (LET b (𝜆 a b · b)) (a b))









    Out[43]:





'(𝜆 b · (𝜆 a b · b))'



In [44]:

    
(𝜆 a p · (p a) (𝜆 a b · a) (𝜆 a · (𝜆 b p · (p b) (𝜆 a b · b) (𝜆 b · (a b)))))









    Out[44]:





'(𝜆 b · (𝜆 a b · b))'



In [45]:

    
;(macro-print '(DO (LET a TRUE) (LET b FALSE) (a b)))



In [46]:

    
(DO (LET a TRUE) (LET b FALSE) (a b))









    Out[46]:





'(𝜆 b · (𝜆 a b · b))'



In [47]:

    
(DO (LET a TRUE b FALSE) (PAIR a b))









    Out[47]:





'(𝜆 s · (s (𝜆 a b · a) (𝜆 a b · b)))'

Lambda calculus language evaluator is written for easy to use, but configurable Hy macros. Two main macros are:

lambda macro, which character identifier can be defined on the fly
application sharp macro, that is Ÿ

Lambda macros

System is initialized by one of the four start up macros:

with-macros
with-alpha-conversion
with-alpha-conversion-nor-macros
with-alpha-conversion-and-macros

with-alpha-conversion-and-macros is recommended way of using the module, because it will provide automatic alpha conversion for variable names and import useful shorthands for several dozens of well known custom lambda forms.

There are two parameters you can use on initialization:

lambda character identifier
argument and body separator character

Usually we see the notation 𝜆x.x for lambda expressions where 𝜆 is the character identifier for the lambda function and . is the separator between lambda function arguments and the body. In the case of 𝜆x.x the first x before the dot is the argument name and the second x after the dot, is the body of the lambda function.

Lambda application in the simplest case could be: (𝜆x.x 1) where 1 is the value of the argument x. Evaluation, or better called beta-reduction is the process of substituting all instances of x in the body with the 1 in this case.

Initialize

So what we want to do next, is the initialization of the module with wanted lambda character and separation marker, let them be: 𝜆 and · in our case:



In [48]:

    
(with-alpha-conversion-nor-macros 𝜆 ·)









    Out[48]:





<function <lambda> at 0x00000279AB825048>

Because we are using simple examples in the following parts, we used with-alpha-conversion-nor-macros initializer, that doesn't provide alpha conversion nor custom macros.

Construct abstration

Now we are ready to construct the first lambda expression in Hy. We will call this the abstration or definition of the function:



In [49]:

    
(𝜆 x · x)









    Out[49]:





'(𝜆 x · x)'

Evaluation of the lambda form gave us back the same expression because we didn't provide any parameters to the lambda function. This is an anonymous function in common programming languages that waits for the caller. If parameter is provided, for example:



In [50]:

    
(𝜆 x · x 1)









    Out[50]:





1

then result would be as simple returning the same value. This is one of the most basic and the simplest forms, which is called identity function. It returns back what is provided as an argument. Note that the number 1 should not be regarded as a number however. It is just a character that has no actual meaning is the lambda calculus. This perhaps the first strange part you will face with lambda calculus. Different distinct forms and expressions have a meaning per se, not symbols that are used in the forms. For example: (𝜆 x · x) is same as (𝜆 y · y) because they will provide similar effect when argument is passed to the function. Take a look at this and compare to the previous code:



In [51]:

    
(𝜆 y · y 1)









    Out[51]:





1

Outcome is same. But is you would make it: (𝜆 y · x 1) then result would be different:



In [52]:

    
(𝜆 y · x 1)









    Out[52]:





'x'

In this case argument y has a value 1, but y is not used on the function body. Rather x is the body and because there is no substitution to the x, returned value is just the original x. We would call this a constant form because it will take one argument, but does nothing with it and rather gives a static value back.

Arguments

Normally we can provide only one argument in lambda function. If several arguments are needed, then they can be nested:



In [53]:

    
(𝜆 x · (𝜆 y · (x y)))









    Out[53]:





'(𝜆 x · (𝜆 y · (x y)))'

Arguments are passed, or lambda technically speaking curryed to the nested levels of the expression. In a formal definition od lambda calculus, only one and one only argument can be passed to the function. In practice it is more compact to write same thing as multiary function:



In [54]:

    
(𝜆 x y · (x y))









    Out[54]:





'(𝜆 x · (𝜆 y · (x y)))'

Small comparison below demonstrated they both produce same output:



In [55]:

    
(, (𝜆 x · (𝜆 y · (x y)) 1 2)
   (𝜆 x y · (x y) 1 2)
   (= (𝜆 x · (𝜆 y · (x y)) 1 2)
      (𝜆 x y · (x y) 1 2)))









    Out[55]:





('(1 2)', '(1 2)', True)

Originally even not as a part of the lambda calculus, it is possible to declare functions without arguments in calchylus module:



In [56]:

    
(𝜆 · x)









    Out[56]:





'x'



In [57]:

    
;(macro-print '(APP x))

This will lead us to the discussion about the basic forms and provided macros in calchylus.

Predefined Lambda forms

These are the usual Lambda forms from textbooks provided as Hy macros. Macros are created for shorthands. They are used to make Lambda terms shorter and more comprehensible:

CONST IDENT LET LET* TRUE FALSE REPLACE
PAIR HEAD TAIL FIRST SECOND NIL NIL?
ZERO ZERO? NUM
ONE TWO THREE FOUR FIVE SIX SEVEN EIGHT NINE TEN
COND AND OR NOT XOR
EQ? LEQ?
ADD PRED SUCC EXP SUM PROD SUB
SELF YCOMB
SUMMATION FACTORIAL FIBONACCI

Constant

Definition:

``(defmacro CONST [&rest args] `(L , ~@args))``

Constant form doesn't take any arguments, but it will return given body as a "static" value. In calchylus unnamed constant is a lambda form without any arguments, that is for example: (𝜆 · x). It will be evaluated directly because there are no bound variables in it. Macro for this form is CONST and it will take the body of the lambda expression as an argument:

Also, if lambda abstraction is declared as a constant body, it will be returned as it is:



In [58]:

    
(CONST t (𝜆 x · x) 1 2)









    Out[58]:





2

However, if function application is given, then function will be evaluated and result of it returned as a value of the constant:



In [59]:

    
(CONST t (𝜆 x · x))









    Out[59]:





'(𝜆 t · (𝜆 x · x))'



In [60]:

    
(CONST t (𝜆 x · x 1))









    Out[60]:





'(𝜆 t · 1)'

If more arguments are passed to the lambda function, than it is requires, also free arguments will be returned on the final output. In this case y is a free argument and returned as a left over. This happens not only in constants but on other function forms too:



In [61]:

    
(𝜆 · x y)









    Out[61]:





'(x y)'

Identity

Definition:

``(defmacro IDENT [&rest args] `(L a , a ~@args))``

The next basic form is the identity function. This function will return the given argument as it is. The formal definition of the identity function is: (L x , x). The custom macro provided by calchhylus module is IDENT and it is used following way:



In [62]:

    
(IDENT x)









    Out[62]:





'x'

Given extra argument, will return both the mandatory argument and latter ones in a parentheses:



In [63]:

    
(IDENT x y z)









    Out[63]:





'(x y z)'

If no arguments are provided, then abstraction is returned:



In [64]:

    
(IDENT)









    Out[64]:





'(𝜆 a · a)'

Booleans

Definition:

``(defmacro TRUE [&rest args] `(L a b , a ~@args))``

``(defmacro FALSE [&rest args] `(L a b , b ~@args))``

These two forms are also very fundamental for lambda calculus. Boolean forms takes two arguments, but return only the other.

True returns the first and omits the second argument. False returns the second and omits the first argument. So they are opposites as one would expect. This switch functionality will give the logical background for the whole calculus. Upon these two primitive form, most of the other forms are based.

In calchylus module, macros are provided accordingly: TRUE and FALSE. But let us first take a closer look to both forms. In true form, if arguments are passed to the function, the first argument will be returned as it is:



In [65]:

    
(𝜆 a b · a 1 2)









    Out[65]:





1

In false form, the second argument is returned as it is:



In [66]:

    
(𝜆 a b · b 1 2)









    Out[66]:





2

In both cases the other argument is left out as a useless option.

Logic

Definition:

`` ; logic (defmacro COND [&rest args] `(L p a b , (p a b) ~@args)) (defmacro AND [&rest args] `(L a b , (a b FALSE) ~@args)) ;(defmacro AND2 [&rest args] `(L a b , (a b a) ~@args)) (defmacro OR [&rest args] `(L a b , (a TRUE b) ~@args)) ;(defmacro OR2 [&rest args] `(L a b , (a a b) ~@args)) (defmacro NOT [&rest args] `(L p , (p FALSE TRUE) ~@args)) ;(defmacro NOT2 [&rest args] `(L p a b , (p b a) ~@args))? (defmacro XOR [&rest args] `(L a b , (a (NOT b) b) ~@args)) ``

Lists

Definition:

`` ; lists (defmacro NIL [&rest args] `(FALSE ~@args)) (defmacro PAIR [&rest args] `(L a b s , (s a b) ~@args)) (defmacro FIRST [&rest args] `(TRUE ~@args)) (defmacro SECOND [&rest args] `(FALSE ~@args)) (defmacro HEAD [&rest args] `(L s , (s TRUE) ~@args)) (defmacro TAIL [&rest args] `(L s , (s FALSE) ~@args)) (defmacro NIL? [&rest args] `(L s , (s FALSE TRUE) ~@args)) ``

This form takes one argument, but does nothing with it. One can think it like an omitter, but also replacer because the next possible argument will be returned instead of the first. This is also very close to the idea of the boolean false form:



In [67]:

    
(FALSE 1 2)









    Out[67]:





2



In [68]:

    
(TRUE 2 d)









    Out[68]:





2



In [69]:

    
(𝜆 aa · aa (𝜆 ab · (aa ab)) ac)









    Out[69]:





'(aa ac)'

Numbers

Arithmetics



In [70]:

    
(with-alpha-conversion-and-macros L ,)
(DO (LET a TRUE b FALSE)
    (LET selector 
         (DO (LET* a selector b a) b))
    (selector a b))









    Out[70]:





'(selector (L a b , a) (L a b , b))'

Sandbox test area

$F$ $f$



In [71]:

    
#Ÿ(n (n (L x , x 1)))









    Out[71]:





'(n (n 1))'



In [72]:

    
(SUMMATION THREE SUCC THREE a b)









    Out[72]:





'(a (a (a (a (a (a (a (a (a b)))))))))'



In [73]:

    
(SUCC TWO TWO a )









    Out[73]:





'(L y , (L x y , (x (x y)) (L x y , (x (x y))) a (L x y , (x (x y)) (L x y , (x (x y))) a y)))'



In [74]:

    
(FACTORIAL FIVE)









    Out[74]:





'(L x , (L y , (L x , (L f n , (L n , (L s , (s (L a , (L a b , b)) (L a b , a)) n) n (L x y , (x y)) (L m n x y , (m (n x) y) (f (L n x y , (n (L g h , (h (g x))) (L x , y) (L a , a)) n)) n)) (x x)) (L x , (L f n , (L n , (L s , (s (L a , (L a b , b)) (L a b , a)) n) n (L x y , (x y)) (L m n x y , (m (n x) y) (f (L n x y , (n (L g h , (h (g x))) (L x , y) (L a , a)) n)) n)) (x x))) (L n x y , (n (L g h , (h (g x))) (L x , y) (L a , a)) (L x y , (x (x (x (x (x y))))))) (L x y , (x (x (x (x (x y))))) x) y)))'



In [75]:

    
(FIBONACCI FIVE)









    Out[75]:





'(L x , (L y , (L x , (L f n , (L m n , (L n , (L s , (s (L a , (L a b , b)) (L a b , a)) n) (n (L n x y , (n (L g h , (h (g x))) (L x , y) (L a , a))) m)) n (L x y , (x (x y))) (L x y , (x y)) (L m n x y , (m x (n x y)) (f (L n x y , (n (L g h , (h (g x))) (L x , y) (L a , a)) n)) (f (L n x y , (n (L g h , (h (g x))) (L x , y) (L a , a)) (L n x y , (n (L g h , (h (g x))) (L x , y) (L a , a)) n))))) (x x)) (L x , (L f n , (L m n , (L n , (L s , (s (L a , (L a b , b)) (L a b , a)) n) (n (L n x y , (n (L g h , (h (g x))) (L x , y) (L a , a))) m)) n (L x y , (x (x y))) (L x y , (x y)) (L m n x y , (m x (n x y)) (f (L n x y , (n (L g h , (h (g x))) (L x , y) (L a , a)) n)) (f (L n x y , (n (L g h , (h (g x))) (L x , y) (L a , a)) (L n x y , (n (L g h , (h (g x))) (L x , y) (L a , a)) n))))) (x x))) (L n x y , (n (L g h , (h (g x))) (L x , y) (L a , a)) (L x y , (x (x (x (x (x y))))))) x (L x , (L f n , (L m n , (L n , (L s , (s (L a , (L a b , b)) (L a b , a)) n) (n (L n x y , (n (L g h , (h (g x))) (L x , y) (L a , a))) m)) n (L x y , (x (x y))) (L x y , (x y)) (L m n x y , (m x (n x y)) (f (L n x y , (n (L g h , (h (g x))) (L x , y) (L a , a)) n)) (f (L n x y , (n (L g h , (h (g x))) (L x , y) (L a , a)) (L n x y , (n (L g h , (h (g x))) (L x , y) (L a , a)) n))))) (x x)) (L x , (L f n , (L m n , (L n , (L s , (s (L a , (L a b , b)) (L a b , a)) n) (n (L n x y , (n (L g h , (h (g x))) (L x , y) (L a , a))) m)) n (L x y , (x (x y))) (L x y , (x y)) (L m n x y , (m x (n x y)) (f (L n x y , (n (L g h , (h (g x))) (L x , y) (L a , a)) n)) (f (L n x y , (n (L g h , (h (g x))) (L x , y) (L a , a)) (L n x y , (n (L g h , (h (g x))) (L x , y) (L a , a)) n))))) (x x))) (L n x y , (n (L g h , (h (g x))) (L x , y) (L a , a)) (L n x y , (n (L g h , (h (g x))) (L x , y) (L a , a)) (L x y , (x (x (x (x (x y)))))))) x y))))'



In [76]:

    
(FIBONACCI)









    Out[76]:





'(L x , ((x (L g , (L h , (h (g (L g , (L h , (h (g (L a , (L a , (L b , b))))))))))) (L x , (L x , (L a , (L b , a)))) (L a , a)) (L a , a) (L x , (L y , (x y))) (L x , (L y , (L x , (L f n , (L m n , (L n , (L s , (s (L a , (L a b , b)) (L a b , a)) n) (n (L n x y , (n (L g h , (h (g x))) (L x , y) (L a , a))) m)) n (L x y , (x (x y))) (L x y , (x y)) (L m n x y , (m x (n x y)) (f (L n x y , (n (L g h , (h (g x))) (L x , y) (L a , a)) n)) (f (L n x y , (n (L g h , (h (g x))) (L x , y) (L a , a)) (L n x y , (n (L g h , (h (g x))) (L x , y) (L a , a)) n))))) (x x)) (L x , (L f n , (L m n , (L n , (L s , (s (L a , (L a b , b)) (L a b , a)) n) (n (L n x y , (n (L g h , (h (g x))) (L x , y) (L a , a))) m)) n (L x y , (x (x y))) (L x y , (x y)) (L m n x y , (m x (n x y)) (f (L n x y , (n (L g h , (h (g x))) (L x , y) (L a , a)) n)) (f (L n x y , (n (L g h , (h (g x))) (L x , y) (L a , a)) (L n x y , (n (L g h , (h (g x))) (L x , y) (L a , a)) n))))) (x x))) (L n x y , (n (L g h , (h (g x))) (L x , y) (L a , a)) x) x (L x , (L f n , (L m n , (L n , (L s , (s (L a , (L a b , b)) (L a b , a)) n) (n (L n x y , (n (L g h , (h (g x))) (L x , y) (L a , a))) m)) n (L x y , (x (x y))) (L x y , (x y)) (L m n x y , (m x (n x y)) (f (L n x y , (n (L g h , (h (g x))) (L x , y) (L a , a)) n)) (f (L n x y , (n (L g h , (h (g x))) (L x , y) (L a , a)) (L n x y , (n (L g h , (h (g x))) (L x , y) (L a , a)) n))))) (x x)) (L x , (L f n , (L m n , (L n , (L s , (s (L a , (L a b , b)) (L a b , a)) n) (n (L n x y , (n (L g h , (h (g x))) (L x , y) (L a , a))) m)) n (L x y , (x (x y))) (L x y , (x y)) (L m n x y , (m x (n x y)) (f (L n x y , (n (L g h , (h (g x))) (L x , y) (L a , a)) n)) (f (L n x y , (n (L g h , (h (g x))) (L x , y) (L a , a)) (L n x y , (n (L g h , (h (g x))) (L x , y) (L a , a)) n))))) (x x))) (L n x y , (n (L g h , (h (g x))) (L x , y) (L a , a)) (L n x y , (n (L g h , (h (g x))) (L x , y) (L a , a)) x)) x y))))))'

Self application



In [77]:

    
(with-alpha-conversion-and-macros L ,)









    Out[77]:





<function <lambda> at 0x00000279ABA181E0>



In [78]:

    
(SELF (L f n , (COND (ZERO? n) ONE (PROD (f f (PRED n)) n))) THREE x y) ; 1*2*3 = 6









    Out[78]:





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



In [79]:

    
; SELF
(L f n , (f f n)
  ; function
  (L f n , 
    ; if n is ZERO?
    (L f , (f (L a , (L a b , b)) (L a b , a)) n
    ; then ONE
    (L x y , (x y))
    ; else PROD 
    (L m n x y , (m (n x) y)
      ; function PRED n
      (f f (L n x y , (n (L g h , (h (g x))) (L x , y) (L a , a)) n))
      ; times n
      n)))
  ; THREE
  (L x y , (x (x (x y)))) x y) ; 1*2*3=6









    Out[79]:





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



In [80]:

    
(SELF (L f n , (ZERO? n ZERO (SUM n (f f (PRED n))))) THREE x y) ; 1*2*3 = 6









    Out[80]:





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



In [81]:

    
; SELF
(L f n , (f f n)
  ; function
  (L f n , 
    ; COND
    (L p a b , (p a b) 
      ; if n is ZERO?
      (L f , (f (L a , (L a b , b)) (L a b , a)) n)
      ; then ZERO
      (L x y , y)
      ; else SUM 
      (L m n x y , (m x (n x y))
        ; function PRED n
        (f f (L n x y , (n (L g h , (h (g x))) (L x , y) (L a , a)) n))
        ; times n
        n)))
  ; THREE
  (L x y , (x (x (x y)))) x y) ; 1*2*3=6









    Out[81]:





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



In [82]:

    
(YCOMB a)









    



Recursion error occured for lambda expression:  (L x , (f (x x)) (L x , (f (x x))))



In [83]:

    
(YCOMB (L f n , (ZERO? n ZERO (SUM n (f (PRED n))))) THREE x y) ; 1*2*3 = 6









    Out[83]:





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



In [84]:

    
(YCOMB
  (L f n , 
    ; COND
    (L p a b , (p a b) 
      ; if ZERO? n
      (L f , (f (L a , (L a b , b)) (L a b , a)) n) 
      ; then ZERO
      (L x y , y) 
      ; else SUM 
      (L m n x y , (m x (n x y))
         ; function PRED n
         (f (L n x y , (n (L g h , (h (g x))) (L u , y) (L u , u)) n))
         ; times n
         n)))
  (L x y , (x (x (x y)))) x y)









    Out[84]:





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

Product function



In [85]:

    
(with-alpha-conversion-and-macros L ,)
(YCOMB (L f , (L n , (COND (ZERO? n) ONE (PROD (f (PRED n)) n)))) THREE x y) ; 1*2*3 = 6









    Out[85]:





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



In [86]:

    
(L f , (L x , (f (x x)) (L x , (f (x x))))
  (L f , (L n ,
     (L p , (L a , (L b , (p a b)))
       (L n , (L s , (s (L a , (L a , (L b , b))) (L a , (L b , a))) n) n)
     (L x , (L y , (x y)))
     (L m , (L n x y , (m (n x) y))
        (f (L n , (L x , (L y , (n (L g , (L h , (h (g x)))) (L x , y) (L a , a)))) n))
      n))))
   (L x , (L y , (x (x (x y))))))









    Out[86]:





'(L x , (L y , (L x , (L f , (L n , (L p , (L a , (L b , (p a b))) (L n , (L s , (s (L a , (L a , (L b , b))) (L a , (L b , a))) n) n) (L x , (L y , (x y))) (L m , (L n x y , (m (n x) y)) (f (L n , (L x , (L y , (n (L g , (L h , (h (g x)))) (L x , y) (L a , a)))) n)) n))) (x x)) (L x , (L f , (L n , (L p , (L a , (L b , (p a b))) (L n , (L s , (s (L a , (L a , (L b , b))) (L a , (L b , a))) n) n) (L x , (L y , (x y))) (L m , (L n x y , (m (n x) y)) (f (L n , (L x , (L y , (n (L g , (L h , (h (g x)))) (L x , y) (L a , a)))) n)) n))) (x x))) (L n , (L x , (L y , (n (L g , (L h , (h (g x)))) (L x , y) (L a , a)))) (L x , (L y , (x (x (x y)))))) (L x , (L y , (x (x (x y)))) x) y)))'



In [87]:

    
(with-alpha-conversion-and-macros L ,)









    Out[87]:





<function <lambda> at 0x00000279ABA180D0>



In [88]:

    
; apply YCOMBinator to function f and number n
(L f , (L n , (f (n n)) (L n , (f (n n))))
  ; for function f and number n
  (L f , (L n ,
    ; if n is ZERO?
    (L f , (f (L a , (L a , (L b , b))) (L a , (L b , a))) n
    ; then return number ONE
    (L x , (L y , (x y)))
    ; else calculate PRODuct of a. and b.
    (L m , (L n , (L x , (L y , (m (n x) y))) 
      ; a. apply recursive function f to PREDecessor of n
      (f (L n , (L x , (L y , (n (L g , (L h , (h (g x)))) (L u , y) (L u , u)))) n)))
      ; b. n
      n))))
  ; number THREE
  (L x , (L y , (x (x (x y))))) x y)









    Out[88]:





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



In [89]:

    
#¤(SUM)









    Out[89]:





$$\\\large L\ m\ n\ x\ y\ ,\ (m\ x\ (n\ x\ y))\\\large=_{\beta} \\\large L\ m\ ,\ (L\ n\ ,\ (L\ x\ ,\ (L\ y\ ,\ (m\ x\ (n\ x\ y)))))\\$$



In [90]:

    
#¤(SUM)









    Out[90]:





$$\\\large L\ m\ n\ x\ y\ ,\ (m\ x\ (n\ x\ y))\\\large=_{\beta} \\\large L\ m\ ,\ (L\ n\ ,\ (L\ x\ ,\ (L\ y\ ,\ (m\ x\ (n\ x\ y)))))\\$$



In [91]:

    
; https://stackoverflow.com/questions/36511989/lambda-calculus-reduction-evaluating-expr
#¤(L f x , (f (f x)) (L y , (y ^ 2)) 5)









    Out[91]:





$$\\\large L\ f\ x\ ,\ (f\ (f\ x))\ (L\ y\ ,\ (y^ 2))\ 5\\\large=_{\beta} \\\large (5^ 2)^ 2\\$$



In [92]:

    
#¤
(L f , (L n , (f (n n)) (L n , (f (n n))))
  (L f n ,
    (L f , (f (L a , (L a b , b)) (L a b , a)) n
    (L x y , (x y))
    (L m n x y , (m (n x) y)
      (f (L n x y , (n (L g , (L h , (h (g x)))) (L u , y) (L u , u)) n))
      n)))
  (L x y , (x (x (x y)))) x y)









    Out[92]:





$$\\\large L\ f\ ,\ (L\ n\ ,\ (f\ (n\ n))\ (L\ n\ ,\ (f\ (n\ n))))\ (L\ f\ n\ ,\ (L\ f\ ,\ (f\ (L\ a\ ,\ (L\ a\ b\ ,\ b))\ (L\ a\ b\ ,\ a))\ n\ (L\ x\ y\ ,\ (x\ y))\ (L\ m\ n\ x\ y\ ,\ (m\ (n\ x)\ y)\ (f\ (L\ n\ x\ y\ ,\ (n\ (L\ g\ ,\ (L\ h\ ,\ (h\ (g\ x))))\ (L\ u\ ,\ y)\ (L\ u\ ,\ u))\ n))\ n)))\ (L\ x\ y\ ,\ (x\ (x\ (x\ y))))\ x\ y\\\large=_{\beta} \\\large x\ (x\ (x\ (x\ (x\ (x\ y)))))\\$$



In [93]:

    
#¤
(L f , (L n , (f (n n)) (L n , (f (n n))))
  (L f n ,
    (L f , (f (L a , (L a b , b)) (L a b , a)) n
    (L x y , (x y))
    (L m n x y , (m (n x) y)
      (f (L n , (L x , (L y , (n (L g , (L h , (h (g x)))) (L u , y) (L u , u)))) n))
      n)))
  (L x y , (x (x (x (x y))))) x y)









    Out[93]:





$$\\\large L\ f\ ,\ (L\ n\ ,\ (f\ (n\ n))\ (L\ n\ ,\ (f\ (n\ n))))\ (L\ f\ n\ ,\ (L\ f\ ,\ (f\ (L\ a\ ,\ (L\ a\ b\ ,\ b))\ (L\ a\ b\ ,\ a))\ n\ (L\ x\ y\ ,\ (x\ y))\ (L\ m\ n\ x\ y\ ,\ (m\ (n\ x)\ y)\ (f\ (L\ n\ ,\ (L\ x\ ,\ (L\ y\ ,\ (n\ (L\ g\ ,\ (L\ h\ ,\ (h\ (g\ x))))\ (L\ u\ ,\ y)\ (L\ u\ ,\ u))))\ n))\ n)))\ (L\ x\ y\ ,\ (x\ (x\ (x\ (x\ y)))))\ x\ y\\\large=_{\beta} \\\large x\ (x\ (x\ (x\ (x\ (x\ (x\ (x\ (x\ (x\ (x\ (x\ (x\ (x\ (x\ (x\ (x\ (x\ (x\ (x\ (x\ (x\ (x\ (x\ y)))))))))))))))))))))))\\$$

Calchylus module examples

System configuration

Download Calchylus

Import main evaluator

Pretty print

Three components

Identity function

Passing parameters

Mathematical notation

Evaluation

Shorthands

Higher-order functions

Constant function

LET and LET*

Multiple arguments

Scopes

Collision detection

Name resolution

More variables

DO imperative

Boolean values

DOs

Lambda macros

Initialize

Construct abstration

Arguments

Predefined Lambda forms

Constant

Identity

Booleans

Logic

Lists

Numbers

Arithmetics

Sandbox test area

Self application

Product function

Tests

Function and application constructors

Alpha conversion

Basic shorthand forms

List shorthand forms

Church numerals shorthands

Logic operator shorthands

Math function shorthands

Infinite loop

The MIT License

`LET` and `LET*`