Running Church’s Programs

I seek a small programming language. I explore here approaching even closer to the historic λ calculus from which so much has already been borrowed by designers of computer languages. The language is scarcely more than Church’s original calculus. It might be called a bald language — no hair. It takes from LISP the notion of executing or evaluating functions whereas Church only showed how to argue the equivalence of functions. I describe here what I mean by evaluating a λ expression which is essentially what Scheme does. In Church’s time computers were merely a theoretical construct and what they could compute was of theoretical interest.

Part of this exercise is to understand the low level execution of a functional language. It might be well to learn the lessons of the Turing tar-pit. See these notes for more perspective on why I am doing this. I report some early coding experience here.

I add bounded numbers simply because neither LISP nor Scheme suggests how to print functions, which are the only values known to the strict lambda calculus. Integers give λ programs something to think and talk about. Church makes it clear, how to informally include integers and arithmetic operators, as primitives but also shows how to implement them formally as pure functions. I have added integers in conformance with his informal description. Familiar arithmetic operations are still missing however and cannot be efficiently built upon the provided primordial functions.

This is the smallest language that I can imagine which may plausibly be useful. I want to try faking the sorts of integers that Church builds from functions, but with the performance of primitive integers.

The source syntax is initially limited to Church’s but allowing numerals. More comfortable syntax later if other ideas pan out. A function call is evaluated by evaluating the function and its argument and then evaluating the function body in light of the new argument value bound to the function’s parameter. More detail here.

Arithmetic, so far, is limited to the increment operator, bound to ‘i’, decrement to ‘d’ and zero predicate to ‘z’. ‘(z n)’ returns K = (λx(λyx)) if n is zero, and otherwise H = (λx(λyy)). K and H are also bound to these two values in the primal name space. P is now available in all versions.

I compile the source input to Mcode defined here. I propose to design a dumb machine merely adequate to express a program to obey Mcode. The idea is a half page of C code that interprets the Mcode. Later a half page of C code to emulate the machine that interprets the Mcode.

The normal mode of executing Scheme, and LISP, is to read a program and after it is all read begin executing a compiled static version of the code. Functions are ‘calculated’ by pairing the current environ with extant compiled sub expressions that were in place just after reading the whole program. The environ supplies a value to each free variable of the expression.

Here is the C code in the form of a Read-Eval-Print-Loop.
Here is about the same thing in OCaml that I found in this presentation.

Here we provide Scheme code to transform λ expressions into combinator expressions which have no free or bound variables.

Here are features that are easy to add but omitted for the sake of having and keeping a truly bald language and system. More controversial features:
Efficient invisible optimizations of Church numbers
I am not sure that this is feasible.
Explore syntax extensions towards writing useful programs.
No ideas here yet but obvious places to look.
Early development within the bald language proceeds by merely implementing those constructs already invented by Church and his students which yields recursion, if-then-else, car-cdr-cons. One way to do this is to provide an editable file which defines these with a place to insert your new code that uses them. Here is such a file into which you can insert your code that refers to the functions defined by Church at the end of section 4. This code illustrates Church’s development of arithmetic in a similar fashion. This yields S-expressions from pure functions.

This code, (and this) which achieves recursive functions via the Y combinator, implements these Scheme functions.

A useful standalone program would translate a λ expression into a Scheme expression. This is a cheaty way of debugging.

Here are fragmentary ideas on machine architecture. It should be easy to implement the unlambda language. This relates Scheme to the λ calculus.

To Do: Clarify arithmetic limits. Harden code. Describe semantics better. Relate semantics to Church’s algorithms. Find suitable solution to null? in pure calculus.