The Coq mailing list

[Helmut Brandl <helmut.brandl AT gmx.net>]

Lambda calculus is the theoretical basis for functional programming languages like Ocaml, Haskell, etc. Therefore as a coq user it is an interesting topic for me.

Since Church's lambda calculus, Gödel's recursive functions and Turing's automatic machines are equivalent, I was curious to find the analogue of a *universal turing machine* expressed in lambda calculus. I have found a quite simple *universal lambda term* which does the job.

I have documented the construction of a *universal lambda term* in this  paper

https://hbr.github.io/Lambda-Calculus/lam-simu/index.html

It gives a short introduction to lambda calculus. Then it introduces a programming notation for lambda calculus similar to Haskell/Ocaml in order to make lambda calculus more readable for functional programmers.

In this notation some basic functions for booleans, pairs, numbers and optional values are introduced.

In order to encode lambda terms the usual Gödel numbering has been avoided. Instead of Gödel numbers the basic idea of algebraic data types has been used.

Based on the structure of an encoded lambda term, a lambda term is constructed which reduces an encoded lambda term to normal form or loops infinitely in case no normal form exists.