User:Samuel lev/sandbox

Computational Topology

Computation in computer science can be reduced to a specific functional based mathematics, lambda calculus. As shown by Allan Turing and Alonzo Church, the λ-calculus is strong enough to describe all mechanically computable functions (see Church-Turing thesis). Lambda-calculus is then a principle programming language from which others can be built. One interpretation is due to the fact bound variables in λ-calculus correspond to formal parameters in a procedure, and the type free principle related to the fact that within a machine, both program and data are the same, namely bits. For this reason when considering the topology of computation it is suitable to focus on the topology of λ-calculus. Functional programming, e.g. type free lambda Calculus, originated as a theoretical foundation of mathematics. The premise relies on functional computability, where objects and functions are of the same type. The topology of λ-calculus is the Scott topology, and when restricted to continuous functions the type free λ-Calculus amounts to a topological space reliant on the tree topology. Both topological spaces 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 congruence relation. Openness within the Scott topology is defined such that if a set O is an open subset of the complete partial order D with relation ≤, then for x ∈ O and x le; y then y ∈ O. Secondly, if the supremum of X is in O with X ≤ D a directed set, then X ∩ O ≠ Ø.

Computational topology is λ calculus topology

Type free λ-calculus treats functions as rules and does not differentiate functions and the objects to which they are applied by type, i.e.data type free. A by-product of type free λ-Calculus is an effective computability equivalent to recursion . The set of λ -terms is then a functional topology in which a function space can be embedded, X → X . Introduced November 1969 Scott's untyped set theoretic model constructed a proper topology for any λ-calculus model whose function space is limited to continuous functions . The result of a Scott continuous λ-calculus topology implies a programming semantic allowing fixed point combinatorics, such as the Y Combinator, and data types . By 1971 λ-calculus was equipped to define any sequential computation and could be easily adapted to parallel computations . The reducibility of all computations to λ-calculus allows topological properties within itself to be applicable to all programming languages .

Based on the operators within lambda calculus, application and abstraction, it is possible to develop a algebra with group structure using application and abstraction as binary operators, as well as use the continuity such operators provide to produce the Scott topology . Application is defined as an operation between lambda terms producing a λ-term, e.g. the application of λ onto the lambda term a produces the lambda term λa. abstraction incorporates undefined variables by denoting λx.t(x) as the function assigning the variable a to the a lambda term with value t(a) via the operation ((λ x.t(x))a = t(a)). Lastly, an equivalence relation emerges identifying λ-terms modulo convertible terms, an example being beta normal form. The resulting topology consists of recursive functions that are definable when restricted to numerals with an infinite or singleton range when acting on a lambda term . The applicable topology for λ-calculus is the tree topology.

Scott Topology

The Scott Topology is essential in understanding the topological structure of computation as expressed using λ-calculus. Scott found that after constructing a function space using using λ-calculus one obtains a Kolmogorov space, T_o topological space which is homeomorphic to itself and exhibits pointwise convergence, in short the product topology . 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. Scott approaches his derivation using a complete lattice, resulting in a topology dependent on the lattice structure. 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.

Complete partial orders are defined as follows:

First, given the partially ordered set D=(D,≤) where a subset X of D, X ≤ D is directed, i.e.:

if X &neq; $\emptyset$ and

$\forall$ x,y ∈ X $\exists$ z &issin; X where x≤ z & y ≤ z

D is a complete partial order (cpo) if:

$\exists$ bottom element $\perp$ such that $\perp$ ∈ D & $\forall$ x ∈ D $\perp$ ≤ x

$\cdot$ Every directed X $\subseteq$D there exists a supremum.

We are now able to define the Scott Topology over a cpo (D, ≤ ).

O $\subseteq$ D is open if:

(1) for x ∈ O, and x ≤ y, then y ∈ O, i.e. O is an upper set.

(2) for a directed set X $\subseteq$ D, and supremum(X) ∈ O, then X $\cap$ O $\neq$ $\emptyset$.

Using the Scott topological definition of open it is apparent that all topological properties are met.

$\cdot$$\emptyset$ and D, i.e. the empty set and whole space, are open.

$\cdot$Open sets are open under arbitrary unions and under intersection:

Proof: Assume $U_{i}$ is open where i ∈ I, I being the index set. We define U = $\cup${ $U_{i}$ ; i ∈ I}. Take b as an element of the upper set of U, therefore a ≤ b for some a ∈ U It must be that a ∈ $U_{i}$ for some i, likewise b ∈ upset($U_{i}$). U must therefore be upper as well since $U_{i}$ ∈ U.

Lastly, if D is a directed set with a supremum in U, then by assumption sup(D) ∈ $U_{i}$where $U_{i}$is open. There is necessarily a b ∈ D where upper(b) $\cap$ D $\subseteq U_{i}\subseteq$ U. The union of open sets $U_{i}$is therefore open.

$\cdot$Open sets under intersection are open:

Proof: Given two open sets, U and V, we define W = U$\cap$V. If W=$\emptyset$ then W is open. If non-empty say b ∈ upset(W) (the upper set of W), then for some a ∈ W, a ≤ b. Since a ∈ U $\cap$V, and b an element of the upper set of both U and V, then b ∈ W. W being open implies the intersection of open sets is open.

Though not shown here, it is the case that the map $f:D\rightarrow D^{'}$ is continuous iff f(sup(X)) = sup(f(X)) for all directed X$\subseteq$ D, where f(X) = {f(x) | x ∈ X} and the second supremum in $D^{'}$.

Before we begin explaining that application as common to λ-calculus is continuous within the Scott topology we require a certain understanding of the behavior of supremums over continuous functions as well as the conditions necessary for the product of spaces to be continuous namely

(1) With ${f_{i}}_{i}$ $\subseteq [D\rightarrow D^{'}]$ be a directed family of maps, then $f(x)=\cup _{i}f_{i}(x)$ if well defined and continuous.

(2) If F $\subseteq [D\rightarrow D^{'}]$ is directed and cpo and $[D\rightarrow D^{'}]$ a cpo where sup({f(x) | f ∈ F).

We now show the continuity of application. Using the definition of application as follows:

Ap: $[D\rightarrow D^{'}]\times D\rightarrow D^{'}$ where Ap(f,x) = f(x).

Ap is continuous with respect to the Scott topology on the product ($[D\rightarrow D^{'}]\times D\rightarrow D^{'}$) :

Proof: λx.f(x) = f is continuous. Let h = λ f.f(x). For directed F$\subseteq [D\rightarrow D^{'}]$

h(sup(F)) = sup(F)(x)

= sup( {f(x) | f ∈ F} )

= sup( {h(f) | f ∈ F} )

= sup( h(F) )

By definition of Scott continuity h is therefore continuous. All that is now required to prove is that application is continuous when it's separate arguments are continuous, i.e. $[D\rightarrow D^{'}]$and D $\rightarrow D^{'}$are continuous, in our case f and h.

Now abstracting our argument to show $f:D\times D^{'}\rightarrow D^{''}$ with g = λ x.f(x,x_{0}) and d = λ$x^{'}.f(x_{0},x^{'})$ as the arguments for D and $D^{'}$ respectively, then for a directed X $\subseteq$ D

g(sup(X)) = f( sup(X),$x_{0}^{'})$ )

= f( sup( {x,$x_{0}^{'}$) | x ∈ X} ))

(since f is continuous and {(x,$x_{0}^{'}$) | x ∈ X}) is directed):

= sup( {f(x,$x_{0}^{'}$) | x ∈ X} )

= sup(g(X))

g is therefore continuous. The same process can be taken to show d is continuous.

It has now been shown application is continuous under the Scott topology.

In order to demonstrate the Scott topology is a suitable fit for λ-calculus it is necessary to prove abstraction remains continuous over the Scott topology. Once completed it will have been shown that the mathematical foundation of λ-calculus is well defined within a function space that is allotted by the Scott topology.

With f ∈ [D $\times D^{'}\rightarrow D^{''}$] we define ${\check {f}}$ (x) =λ y ∈ $D^{'}$f(x,y)We will show:

(i) ${\check {f}}$ is continuous, meaning ${\check {f}}$ ∈ $[D\rightarrow [D^{'}\rightarrow D^{''}]$

(ii) λ $f.{\check {f}}:[D\times D^{'}\rightarrow D^{''}]\rightarrow [D\rightarrow [D^{'}\rightarrow D^{''}]$ is continuous.

Proof (i): Let X $\subseteq$ D be directed, then

${\check {f}}$(sup(X)) = λ y.f( sup(X),y )

= λ y.$sup_{x\in X}$( f(x,y) )

= $sup_{x\in X}$( λy.f(x,y) )

= sup(${\check {f}}$(X))

Proof (ii): Defining L = λ $f.{\check {f}}$ then for F $\subseteq [D\times D^{'}\rightarrow D^{''}]$ directed

L(sup(F)) = λ x λ y. (sup(F))(x,y))

= λ x λ y. $sup_{y\in F}$f(x,y)

= $sup_{y\in F}$λx λy.f(x,y)

= sup(L(F))

Böhm trees and Computational Topology

Böhm trees, easily represented graphically, express the computational behavior of a lambda term. It is possible, from reference to the correlating Böhm tree, to predict the functionality of a given lambda expression. Böhm trees can be seen somewhat analogous to $\mathbb {R}$. The Böhm tree of a given set is similar to the continued fraction of a real number, and similar to the rational subset of the Reals, the Böhm tree corresponding to a sequence in normal form is finite.

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 $\psi$.

Informally Böhm trees may be conceptualized as follows:

Given: $\Sigma$ = $\perp \cup$ { λ x_{1} $\cdots$x_{n} . y | n ∈ $\mathbb {N} ,x_{1}...x_{n}$y are variables and denoting BT(M) as the Böhm tree for a lambda term M we then have:

BT(M) = $\perp$ if M is unsolvable (therefore a single node)

BT(M) = λ${\vec {x}}$.y

$\wedge$

BT($M_{1})_{}$ BT($M_{m}$ ) ; if M is solvable

More Formally:

$\Sigma$ is defined as a set of symbols. The Böhm tree of a λ term M, denoted BT(M), is the $\Sigma$ labelled tree defined as follows:

If M is unsolvable:

BT(M)(< >) = $\perp$,

BT(M)($<k>*\alpha$) is unsolvable $\forall k,\alpha$

If M is solvable, where M = λ x_{1}$\cdots x_{n}.yM_{0}\cdots M_{m-1}$:

BT(M)(< >) = λ x_{1} $\cdots x_{n}.y$

BT(M)($<k>*\alpha$) = BT(M_k)($\alpha$) $\forall \alpha$ and k < m

= undefined $\forall \alpha$ and k $\geq$ m

We may now move on to show that Böhm trees act as suitable mappings from the tree topology to the scott topology. Allowing one to see computational constructs, be it within the Scott or tree topology, as Böhm tree formations.

Böhm tree and tree topology

It is found that Böhm tree's allow for a continuous mapping from the tree topology to the Scott topology. More specifically:

We begin with the cpo B = (B,$\subseteq$) on the Scott topology, with ordering of Böhm tree's meaning M$\subseteq$ N, where M, N are trees, if M results from N. The tree topology on the set $\Gamma$ is the smallest set allowing for a continuous map

BT:$\Gamma \rightarrow$B.

An equivalent definition would be to say the open sets of $\Gamma$ are the image of the inverse Böhm tree $BT^{-1}$ (O) where O is Scott open in B.

The applicability of the Bömh trees and the tree topology has many interesting consequences to λ-terms expressed topologically:

Normal forms are found to exist as isolated points.

Unsolvable λ-terms are compactification points.

Application and abstraction, similar to the Scott topology, are continuous on the tree topology.

Algebraic structure of Computation

New methods of interpretation of the λ-calculus are not only interesting in themselves, but provide great incite into the behaviors of computer science. A λ-calculus algebra can allow to have provably equal terms as equivalent within the algebra. Group structures then illuminate relations between λ-terms, $\beta$ reductions, and applicative forms. The binary operator within the a λ-algebra A is the application operator $\cdot$ giving structure $A=(X,\cdot )$ In order to allow for abstraction a combinatory algebra results. The λ algebra is then a combinatory algebra M combined with a syntactic operator λ* that transforms a term B(x,y), with constants in M, into C(${\hat {y}}$)$\equiv$ λ* x.B(x,${\hat {y}}$). It is also possible to define an extension model to circumvent the need of the λ* operator by allowing $\forall$x fx =gx) $\rightarrow$ f =g .

To accomplish the necessary assumption that there exist solutions to equations such as axy = xyy | a = λ xy.xyy there is need for the combinatory algebra. Combinatory algebras can be defined as follows:

(I)M = (X,$\cdot$ )is an applicative structure if $\cdot$ is a binary operation on X.

M is extensional if for f,$f^{'}$ ∈ X then ($\forall$ x ∈ X f.x = $f^{'}.x)$ $\Rightarrow$ f = $f^{'}$

(II) If M = (X,$\cdot$), then we write a ∈ M instead of a ∈ X

Within combinatory algebra there exists applicative structures. An applicative structure W is a combinatory algebra provided:

$\cdot$W is non-trival, meaning W has cardinality > 1

$\cdot$W exibits combinatory completeness (see completeness of the S-K basis). More specifically: for every term A ∈ the set of terms of W, and $x_{1},...,x_{n}$ with the free variables of A within ${x_{1},...,x_{n}}$ then:

$\exists f\forall x_{1}\cdot \cdot \cdot x_{n}fx_{1}\cdot \cdot \cdot x_{n}=A$

Important results of the combiniatory algebra show they:

Never commute

Never are associative.

Never are finite.

and never are recursive.

Combinatory algebras remain unable to act as the algebraic structure for λ-calculus. However the existence of an applicative term A(x, ${\vec {y}}$) provides a good starting point to build a λ-calculus algebra. What is needed is the introduction of a lambda terms, i.e. include λx.A(x, ${\vec {y}}$).

We begin by exploiting the fact that within a combinatory algebra M with A(x, ${\vec {y}}$) within the set of terms then:

$\forall {\vec {y}}$ $\exists b$ s.t. bx = A(x, ${\vec {y}}$).

We then require b have a dependence on ${\vec {y}}$ resulting in:

$\forall x$ B(${\vec {y}}$)x = A(x, ${\vec {y}}$).

B(${\vec {y}}$) becomes equivilent to a λ term, and is therefore suitably defined as follows: B(${\vec {y}})\equiv$ λ*.

A pre-λ-algebra (pλA) can now be defined.

pλA is an applicative structure W = (X,$\cdot$) such that for each term A within the set of terms within W and for every x there is a term λ*x.A ∈ T(W) (T(W) $\equiv$ the terms of W) where (the set of free variables of λ*x.A) = (the set of free variables of A) - {x}. W must also demonstrate:

$(\beta )$ (λ*x.A)x = A

$\alpha _{1}$λ*x.A$\equiv$ λ*x.A[x:=y] provided y is not a free variable of A

$\alpha _{2}$(λ*x.A)[y:=z]$\equiv$λ*x.A[x:=y] provided y,z ≠ x and z is not a free variable of A

Before defining the full λ-algebra we must introduce the following definition for the set of λ-terms within W denoted $\Gamma (W)$ with the following requirements:

a ∈ W $\Rightarrow c_{a}\in \Gamma (W)$

x ∈ $\Gamma (W)$ for x ∈ {$v_{0},v_{1},...$)

M,N ∈ $\Gamma (W)\Rightarrow$ (MN) ∈ $\Gamma (W)$

M ∈ $\Gamma (W)\Rightarrow$ (λx.M) ∈ $\Gamma (W)$

A mapping from the terms within $\Gamma (W)$ to all λ terms within W, denoted * : $\Gamma (W)\rightarrow \mathrm {T} (W)$, can then be designed as follows:

$v_{i}^{*}=w_{i},c_{a}^{*}=c_{a}$

(MN)* = M* N*

(λx.M)* = λ* x*.M*

We now define λ(M) to denote the extension after evaluating the terms within $\Gamma (W)$.

λx.(λy.yx)$c_{a}$ = λx.$c_{a}$x in λ(W).

Finally we obtain the full λ-algebra through the following definition:

(1) A λ-algebra is a pλA W such that for M,N ∈ $\Gamma$(W):

λ(W) $\vdash$ M = N $\Rightarrow$ W $\vDash$ M = N.

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.