As shown by Alan Turing and Alonzo Church, the λ-calculus is strong enough to describe all mechanically computable functions (see Church–Turing thesis).
Both the Scott and Tree topologies exhibit continuity with respect to the binary operators of application ( f applied to a = fa ) and abstraction ((λx.t(x))a = t(a)) with a modular equivalence relation based on a congruency.
Type free λ-calculus treats functions as rules and does not differentiate functions and the objects which they are applied to, meaning λ-calculus is type free.
A by-product of type free λ-calculus is an effective computability equivalent to general recursion and Turing machines.
[4][5] Introduced November 1969, Dana Scott's untyped set theoretic model constructed a proper topology for any λ-calculus model whose function space is limited to continuous functions.
[4][5] The result of a Scott continuous λ-calculus topology is a function space built upon a programming semantic allowing fixed point combinatorics, such as the Y combinator, and data types.
[8] The reducibility of all computations to λ-calculus allows these λ-topological properties to become adopted by all programming languages.
[4] Based on the operators within lambda calculus, application and abstraction, it is possible to develop an algebra whose group structure uses application and abstraction as binary operators.
Lastly, an equivalence relation emerges which identifies λ-terms modulo convertible terms, an example being beta normal form.
[9] It is the ability of self homeomorphism as well as the ability to embed every space into such a space, denoted Scott continuous, as previously described which allows Scott's topology to be applicable to logic and recursive function theory.
It is possible to generalise Scott's theory with the use of complete partial orders.
For this reason a more general understanding of the computational topology is provided through complete partial orders.
We will re-iterate to familiarize ourselves with the notation to be used during the discussion of Scott topology.
Using the definition of application as follows: Ap is continuous with respect to the Scott topology on the product (
Once completed it will have been shown that the mathematical foundation of λ-calculus is a well defined and suitable candidate functional paradigm for the Scott topology.
f(x,y)We will show: It has not been demonstrated how and why the λ-calculus defines the Scott topology.
Böhm trees, easily represented graphically, express the computational behavior of a lambda term.
It is possible to predict the functionality of a given lambda expression from reference to its correlating Böhm tree.
where the Böhm tree of a given set is similar to the continued fraction of a real number, and what is more, the Böhm tree corresponding to a sequence in normal form is finite, similar to the rational subset of the Reals.
Böhm trees are defined by a mapping of elements within a sequence of numbers with ordering (≤, lh) and a binary operator * to a set of symbols.
The Böhm tree is then a relation among a set of symbols through a partial mapping ψ.
) ; if M is solvable More formally: Σ is defined as a set of symbols.
The applicability of the Bömh trees and the tree topology has many interesting consequences to λ-terms expressed topologically: New methods of interpretation of the λ-calculus are not only interesting in themselves but allow new modes of thought concerning the behaviors of computer science.
A combinatory algebra allows for the application operator and acts as a useful starting point but remains insufficient for the λ-calculus in being unable to express abstraction.
It is also possible to define an extension model to circumvent the need of the λ* operator by allowing ∀x (fx =gx) ⇒ f =g .
The construction of the λ-algebra through the introduction of an abstraction operator proceeds as follows: We must construct an algebra which allows for solutions to equations such as axy = xyy such that a = λ xy.xyy there is need for the combinatory algebra.
) provides a good starting point to build a λ-calculus algebra.
Before defining the full λ-algebra we must introduce the following definition for the set of λ-terms within W denoted
, can then be designed as follows: We now define λ(M) to denote the extension after evaluating the terms within
Finally we obtain the full λ-algebra through the following definition: Though arduous, the foundation has been set for a proper algebraic framework for which the λ-calculus, and therefore computation, may be investigated in a group theoretic manner.