Lambda calculus

From apm
Jump to: navigation, search 
Lambda calculus – it's basic rules are unbelievably simple and it can compute anything and everything =

Lambda diagrams are a way to visualize lambda calculus.
Lambda calculus is an extremely simple formalism that is equally expressive to the (much more widely known) Turing machine.
That is: Lambda calculus is "Turing complete".
Any program that is in principle logically possible can be written in Lambda calculus.
A maximally universal computer. At least that is what is the current (2021) consensus on the topic.

The special thing about lambda calculus is that:
Lambda calculus is used very much unchanged as the core of a number of practical programming languages.
Perhaps more so than the Truing machine is.
("practical programming languages" meaning programming languages that are in use in practical applications to a quite notable degree.)

Graphical visualizations for lambda calculus

There are a number of graphical visualizations for Lambda calculus.
The most straightforward one is just to plot out the syntax tree.
There are only three types of elements in the syntax tree of lambda calculus:

  • abstractions
  • applications
  • variables

It's as simple as that.
Well, adding evaluation strategies and a type system makes it a bit more complicated.
But that is the basic gist.

Plain lambda diagrams (PLDs)

An especially nice visualization for lambda calculus are (unannotated) "lambda diagrams".
These are presented by John Tromp on his homepage here: https://tromp.github.io/cl/diagrams.html

Annotated lambda diagrams (ALDs)

Adding some annotations to lambda diagrams may make these into an amazing programming interface with some awesome properties.
Smack in the middle of between textual and visual programming.
See main page: Annotated lambda diagrams

On the fundamentality of lambda calculus

Lambda calculus is without a doubt a very fundamental calculus.
There is no such things as the most fundamental calculus though.

  • Unfortunately because we like to seek "perfect" solutions.
  • Fortunately because we'll never run out of new "miracles".

Turing machine seems less fundamental

The equally expressive truing machine model with

  • unboundedly long memory tape and
  • finite table of rules

certainly seems less fundamental than the lambda calculus.
In that a concrete implementation of the model is less elegant and less amenable to mathematical handling.

"Overloading" lambda calculus

Lambda calculus can be abstracted over by an category theory based interpretation.
See: Compiling to categories (Conal Elliott)
It's kinda like overloading the meaning of function application and ...

Equivalent calculi

There are other calculi equivalent in expressiveness like e.g. the SKI calculus.
Maybe less intuitive though. While identical programs (same fixed points) can be represented, they differ in run-times.
(Interestingly conversion between calculi in general is a hard problem)

Similar but different calculi

There are other calculi that are similarly sparse in rules like e.g. the pi-calculus.
(wiki-TODO: Look into this again – is the property of mathematical substitutability given?)

Functional vs Relational

Lambda calculus is modelling functional relationships not relational relationsships.
There is a directionality in functional relationships while there is none in relational relationships.
Evaluation needs a direction to proceed so this kinda makes sense maybe?

Variable names / indices

When using names for bound variables then terms that are syntactically different (that is: not written out the same)
are not necessarily semantically different (that is: they may still mean the same).
This is because the exact same structure can use different names for the variables.
Also when there are reused variable names(shadowing) then evaluation by substitution-of-variables-by-their-definition (aka β-reduction)
can lead to name collisions that must be resolved by renaming (aka α-conversion).
This is all additional bookkeeping only leading to additional computational load.

One thus desires to represent the terms of lambda calculus without naming the bound variables.
A natural way to do so is by using so called de Brujin indices.

A de Brujin index is a whole positve number at the location of a variable that represents
how many nested surrounding binders one needs to jump over to reach the binder for the variable
In a way a de Brujin index specifies The disrete degree of non-locality.

De Brujin indices are hard to manually operate by human mind though as ...

  • they can change during β-reductions and
  • binders do not carry visually matchable value names

Note that there is yet another quite interesting approach in naming/indexing variables. See:

For this to work deferred/lazy evaluation is a necessary prerequisite.
Also when (unlike untyped lambda calculus) types are involved it's possible to run into occurs check issues.

It gives higher order abstract syntax (HOAS) for constructing terms, while retaining a simple first-order representation.

Related

External links

Retrieved from "http://apm.bplaced.net/w/index.php?title=Lambda_calculus&oldid=13741"