|
|
| (198 intermediate revisions by more than 100 users not shown) |
| Line 1: |
Line 1: |
| {{Orphan|date=July 2012}}
| | This is a preview for the new '''MathML rendering mode''' (with SVG fallback), which is availble in production for registered users. |
|
| |
|
| '''Computable topology''' studies the topological and algebraic structure of computation. Computable topology includes algorithmic topology and therefore encompasses computer science. [[Computational topology]] is equivalent to the topology of [[lambda calculus|λ-calculus]]. Within [[computer science]] computational forms can be reduced to λ-calculus's functional based mathematics. As shown by [[Allan Turing]] and [[Alonzo Church]], the λ-calculus is strong enough to describe all mechanically computable functions (see [[Church-Turing thesis]]).<ref>Church 1934:90 footnote in Davis 1952</ref><ref>Turing 1936–7 in Davis 1952:149</ref><ref>Barendregt, H.P., The Lambda Calculus Syntax and Semantics. North-Holland Publishing Company. 1981</ref> Lambda-calculus is then a foundational mathematics easily made into a principle programming language from which other languages can be built. 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|Scott topology]], and when restricted to continuous functions the type free λ-Calculus amounts to a [[topological space]] reliant on the [[tree topology]]. 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 [[congruence relation|congruency]]. The algebraic structure of computation may also be considered as equivalent to the algebraic structure of λ-calculus, meaning the λ-algebra. The λ-algebra is found to be an extension of the combinatory algebra, with an element introduced to accommodate abstraction. | | If you would like use the '''MathML''' rendering mode, you need a wikipedia user account that can be registered here [[https://en.wikipedia.org/wiki/Special:UserLogin/signup]] |
| | * Only registered users will be able to execute this rendering mode. |
| | * Note: you need not enter a email address (nor any other private information). Please do not use a password that you use elsewhere. |
|
| |
|
| A primary concern of algorithmic topology, as its name suggests, is to develop efficient [[algorithm]]s for solving topological problems, or using topological methods to solve algorithmic problems from other fields.
| | Registered users will be able to choose between the following three rendering modes: |
|
| |
|
| ==Computational topology from λ-calculus topology==
| | '''MathML''' |
| Type free λ-calculus treats functions as rules and does not differentiate functions and the objects which they are applied to, meaning λ-calculus is [[data type|type]] free. A by-product of type free λ-Calculus is an [[effective method|effective computability]] equivalent to [[recursion|general recursion]] and [[Turing machine]]s.<ref name="Barendregt">Barendregt, H.P., The Lambda Calculus Syntax and Semantics. North-Holland Publishing Company. 1981.</ref> The set of λ -terms can be considered a functional topology in which a function space can be [[embedding|embedded]], meaning λ mappings within the space X are such that λ:X → X.<ref name="Barendregt" /><ref name="ScottModels">D. S. Scott. Models for the λ-calculus. Informally distributed, 1969. Notes, December 1969, Oxford Univ.</ref> 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.<ref name="Barendregt" /><ref name="ScottModels" /> 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.<ref>Gordon, M.J.C., The Denotational Description of Programming Languages. Springer Verlag, Berlin. 1979.</ref><ref>Scott, D. S. and Strachey, C. Toward a Mathematical Semantics for Computer Languages, Proc. Symp. on Computers and Automata, Polytechnic Institute of Brooklyn, 21, pp. 19-46. 1971.</ref> By 1971, λ-calculus was equipped to define any sequential computation and could be easily adapted to parallel computations.<ref>G. Berry, Sequential algorithms on concrete data structures, Theoretical Computer Science 20, 265-321 (1982).</ref> The reducibility of all computations to λ-calculus allows these λ-topological properties to become adopted by all programming languages.<ref name="Barendregt" />
| | :<math forcemathmode="mathml">E=mc^2</math> |
|
| |
|
| ==Computational Algebra from λ-calculus algebra==
| | <!--'''PNG''' (currently default in production) |
| 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. Application is defined as an operation between [[lambda term]]s 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 lambda term with value ''t(a)'' via the operation ((λ x.t(x))a = t(a)). Lastly, an [[equivalence relation]] emerges which identifies λ-terms modulo convertible terms, an example being [[beta normal form]].
| | :<math forcemathmode="png">E=mc^2</math> |
|
| |
|
| ==Scott Topology==
| | '''source''' |
| The Scott Topology is essential in understanding the topological structure of computation as expressed through the λ-calculus. Scott found that after constructing a function space using λ-calculus one obtains a [[Kolmogorov space]], a <math>T_o</math> topological space which is [[homeomorphic]] to itself and exhibits [[pointwise convergence]], in short the [[product topology]].<ref>D. S. Scott. “Continuous Lattices.” Oxford University Computing Laboratory August, 1971.</ref> 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 order]]s. 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.
| | :<math forcemathmode="source">E=mc^2</math> --> |
|
| |
| 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.:
| | <span style="color: red">Follow this [https://en.wikipedia.org/wiki/Special:Preferences#mw-prefsection-rendering link] to change your Math rendering settings.</span> You can also add a [https://en.wikipedia.org/wiki/Special:Preferences#mw-prefsection-rendering-skin Custom CSS] to force the MathML/SVG rendering or select different font families. See [https://www.mediawiki.org/wiki/Extension:Math#CSS_for_the_MathML_with_SVG_fallback_mode these examples]. |
| ::if ''X'' ≠ <math>\empty</math> and
| |
| ::<math>\forall</math> ''x,y'' ∈ ''X'' <math>\exists</math> ''z'' ∈ ''X'' where ''x''≤ ''z'' & ''y'' ≤ ''z'' | |
|
| |
|
|
| | ==Demos== |
| ''D'' is a [[complete partial order]] (cpo) if:
| |
|
| |
| ::<math>\exists</math> ''bottom'' element <math>\perp</math> such that <math>\perp</math> ∈ ''D'' & <math>\forall</math> ''x'' ∈ ''D'' <math>\perp</math> ≤ ''x''
| |
|
| |
| ::<math>\cdot</math> Every directed X <math>\subseteq</math>D there exists a [[supremum]].
| |
|
| |
|
| We are now able to define the '''Scott Topology''' over a cpo (D, ≤ ).
| | Here are some [https://commons.wikimedia.org/w/index.php?title=Special:ListFiles/Frederic.wang demos]: |
|
| |
| ''O'' <math>\subseteq</math> ''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 <math>\subseteq</math> D, and [[supremum]](X) ∈ O, then X <math>\cap</math> O <math>\neq</math> <math>\empty </math>. | |
|
| |
|
| |
|
| Using the Scott topological definition of open it is apparent that all topological properties are met.
| |
|
| |
| ::<math>\cdot</math><math>\empty</math> and D, i.e. the empty set and whole space, are open.
| |
|
| |
|
| ::<math>\cdot</math>Open sets are open under arbitrary unions and under intersection: | | * accessibility: |
| :::: ''Proof'': Assume <math>U_i</math> is open where i ∈ I, I being the index set. We define U = <math>\cup</math>{ <math>U_i</math> ; 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'' ∈ <math>U_i</math> for some i, likewise ''b'' ∈ upset(<math>U_i</math>). U must therefore be upper as well since <math>U_i</math> ∈ U. | | ** Safari + VoiceOver: [https://commons.wikimedia.org/wiki/File:VoiceOver-Mac-Safari.ogv video only], [[File:Voiceover-mathml-example-1.wav|thumb|Voiceover-mathml-example-1]], [[File:Voiceover-mathml-example-2.wav|thumb|Voiceover-mathml-example-2]], [[File:Voiceover-mathml-example-3.wav|thumb|Voiceover-mathml-example-3]], [[File:Voiceover-mathml-example-4.wav|thumb|Voiceover-mathml-example-4]], [[File:Voiceover-mathml-example-5.wav|thumb|Voiceover-mathml-example-5]], [[File:Voiceover-mathml-example-6.wav|thumb|Voiceover-mathml-example-6]], [[File:Voiceover-mathml-example-7.wav|thumb|Voiceover-mathml-example-7]] |
| | ** [https://commons.wikimedia.org/wiki/File:MathPlayer-Audio-Windows7-InternetExplorer.ogg Internet Explorer + MathPlayer (audio)] |
| | ** [https://commons.wikimedia.org/wiki/File:MathPlayer-SynchronizedHighlighting-WIndows7-InternetExplorer.png Internet Explorer + MathPlayer (synchronized highlighting)] |
| | ** [https://commons.wikimedia.org/wiki/File:MathPlayer-Braille-Windows7-InternetExplorer.png Internet Explorer + MathPlayer (braille)] |
| | ** NVDA+MathPlayer: [[File:Nvda-mathml-example-1.wav|thumb|Nvda-mathml-example-1]], [[File:Nvda-mathml-example-2.wav|thumb|Nvda-mathml-example-2]], [[File:Nvda-mathml-example-3.wav|thumb|Nvda-mathml-example-3]], [[File:Nvda-mathml-example-4.wav|thumb|Nvda-mathml-example-4]], [[File:Nvda-mathml-example-5.wav|thumb|Nvda-mathml-example-5]], [[File:Nvda-mathml-example-6.wav|thumb|Nvda-mathml-example-6]], [[File:Nvda-mathml-example-7.wav|thumb|Nvda-mathml-example-7]]. |
| | ** Orca: There is ongoing work, but no support at all at the moment [[File:Orca-mathml-example-1.wav|thumb|Orca-mathml-example-1]], [[File:Orca-mathml-example-2.wav|thumb|Orca-mathml-example-2]], [[File:Orca-mathml-example-3.wav|thumb|Orca-mathml-example-3]], [[File:Orca-mathml-example-4.wav|thumb|Orca-mathml-example-4]], [[File:Orca-mathml-example-5.wav|thumb|Orca-mathml-example-5]], [[File:Orca-mathml-example-6.wav|thumb|Orca-mathml-example-6]], [[File:Orca-mathml-example-7.wav|thumb|Orca-mathml-example-7]]. |
| | ** From our testing, ChromeVox and JAWS are not able to read the formulas generated by the MathML mode. |
|
| |
|
| ::::Lastly, if D is a directed set with a supremum in U, then by assumption sup(D) ∈ <math>U_i </math>where <math>U_i </math>is open. There is necessarily a ''b'' ∈ D where upper(b) <math>\cap</math> D <math>\subseteq U_{i} \subseteq</math> U. The union of open sets <math> U_i </math>is therefore open.
| | ==Test pages == |
|
| |
| ::<math>\cdot</math>Open sets under intersection are open:
| |
| ::::''Proof'': Given two open sets, U and V, we define W = U<math>\cap</math>V. If W=<math>\empty</math> 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 <math>\cap</math>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 <math>f: D \rightarrow D^{'}</math> is continuous iff f(sup(X)) = sup(f(X)) for all directed X<math>\subseteq</math> D, where f(X) = {f(x) | x ∈ X} and the second supremum in <math>D^{'}</math>.<ref name="Barendregt" />
| |
|
| |
| 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 <math>{f_{i}}_{i}</math> <math>\subseteq [D \rightarrow D^{'}]</math> be a directed family of maps, then <math>f(x) = \cup_{i}f_{i}(x)</math> if well defined and continuous.
| |
|
| |
| :(2) If F <math>\subseteq [D \rightarrow D^{'}]</math> is directed and cpo and <math> [D \rightarrow D^{'}]</math> a cpo where sup({f(x) | f ∈ F).
| |
|
| |
|
| |
|
| |
| We now show the continuity of ''application''. Using the definition of application as follows:
| |
|
| |
| :::Ap: <math>[D\rightarrow D^{'}] \times D \rightarrow D^{'}</math> where Ap(f,x) = f(x).
| |
|
| |
| Ap is continuous with respect to the Scott topology on the product (<math> [D \rightarrow D^{'}] \times D \rightarrow D^{'}</math>) :
| |
|
| |
| ::''Proof'': λx.f(x) = f is continuous. Let h = λ f.f(x). For directed F<math>\subseteq [D \rightarrow D^{'}]</math>
| |
|
| |
| ::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 has been shown continuous. All that is now required to prove is that ''application'' is continuous when it's separate arguments are continuous, i.e. <math>[D \rightarrow D^{'}] </math>and <math>D \rightarrow D^{'} </math>are continuous, in our case ''f'' and ''h''.
| |
|
| |
| ::Now abstracting our argument to show <math>f:D \times D^{'} \rightarrow D^{''} </math> with ''g'' = λ x.f(x,<math>x_{0}</math>) and ''d'' = λ<math> x^'.f(x_0,x^')</math> as the arguments for D and <math>D^'</math> respectively, then for a directed X <math>\subseteq</math> D
| |
|
| |
| ::g(sup(X)) = f( sup(X),<math>x_{0}^{'})</math> )
| |
|
| |
| :::: = f( sup( (x,<math>x_{0}^{'}</math>) | x ∈ X} ))
| |
|
| |
| :::: (since ''f'' is continuous and {(x,<math>x_{0}^{'}</math>) | x ∈ X}) is directed):
| |
|
| |
| :::: = sup( {f(x,<math>x_{0}^{'}</math>) | 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.
| |
|
| |
|
|
| | To test the '''MathML''', '''PNG''', and '''source''' rendering modes, please go to one of the following test pages: |
| 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 a well defined and suitable candidate functional paradigm for the Scott topology.
| | *[[Displaystyle]] |
|
| | *[[MathAxisAlignment]] |
| | *[[Styling]] |
| | *[[Linebreaking]] |
| | *[[Unique Ids]] |
| | *[[Help:Formula]] |
|
| |
|
| With f ∈ [D <math>\times D^{'} \rightarrow D^{''}</math>] we define <math>\check{f}</math> (x) =λ y ∈ <math>D^{'}</math>f(x,y)We will show:
| | *[[Inputtypes|Inputtypes (private Wikis only)]] |
|
| | *[[Url2Image|Url2Image (private Wikis only)]] |
| :(i) <math>\check{f} </math> is continuous, meaning <math>\check{f}</math> ∈ <math>[D \rightarrow [D^{'} \rightarrow D^{''}] </math>
| | ==Bug reporting== |
|
| | If you find any bugs, please report them at [https://bugzilla.wikimedia.org/enter_bug.cgi?product=MediaWiki%20extensions&component=Math&version=master&short_desc=Math-preview%20rendering%20problem Bugzilla], or write an email to math_bugs (at) ckurs (dot) de . |
| :(ii) λ <math> f.\check{f}: [D \times D^{'} \rightarrow D^{''}]\rightarrow [D\rightarrow [D^{'}\rightarrow D^{''}]</math> is continuous.
| |
|
| |
| ::''Proof'' (i): Let X <math>\subseteq</math> D be directed, then
| |
| | |
| ::<math>\check{f}</math>(sup(X)) = λ y.f( sup(X),y )
| |
|
| |
| :::: = λ y.<math>sup_{x \isin X}</math>( f(x,y) )
| |
|
| |
| :::: = <math>sup_{x \isin X}</math>( λy.f(x,y) )
| |
|
| |
| :::: = sup(<math>\check{f}</math>(X))
| |
|
| |
| ::''Proof'' (ii): Defining L = λ <math> f.\check{f} </math> then for F <math> \subseteq [D \times D^{'} \rightarrow D^{''}]</math> directed
| |
|
| |
| ::L(sup(F)) = λ x λ y. (sup(F))(x,y))
| |
|
| |
| :::: = λ x λ y. <math>sup_{y \isin F}</math>f(x,y)
| |
|
| |
| :::: = <math>sup_{y \isin F} </math>λx λy.f(x,y)
| |
|
| |
| :::: = sup(L(F))
| |
| It has not been demonstrated how and why the λ-calculus defines the Scott topology.
| |
| | |
| ==Böhm trees and Computational 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.<ref name="Barendregt" /> Böhm trees can be seen somewhat analogous to <math>\mathbb{R}</math> 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 <math>\psi</math>.
| |
|
| |
| Informally Böhm trees may be conceptualized as follows:
| |
| | |
| :Given: <math>\Sigma</math> = <math>\perp \cup </math> { λ x_{1} <math>\cdots </math>x_{n} . y | n ∈ <math> \mathbb{N}, x_{1} ... x_{n}</math>y are variables and denoting BT(M) as the Böhm tree for a lambda term M we then have:
| |
|
| |
| :BT(M) = <math>\perp</math> if M is unsolvable (therefore a single node)
| |
| <poem>
| |
| BT(M) = λ<math>\vec{x}</math>.y
| |
| / \
| |
| BT(<math> M_{1} )</math> BT(<math> M_{m}</math> ) ; if M is solvable
| |
| </poem>
| |
| More Formally:
| |
|
| |
| <math>\Sigma</math> is defined as a set of symbols. The Böhm tree of a λ term M, denoted BT(M), is the <math>\Sigma</math> labelled tree defined as follows:
| |
|
| |
| ::If M is unsolvable:
| |
|
| |
| ::BT(M)(< >) = <math>\perp</math>,
| |
|
| |
| ::BT(M)(<math><k> * \alpha</math>) is unsolvable <math>\forall k, \alpha</math>
| |
| | |
| If M is solvable, where M = λ x_{1}<math> \cdots x_{n}.y M_{0} \cdots M_{m-1}</math>: | |
|
| |
| ::BT(M)(< >) = λ x_{1} <math>\cdots x_{n}.y</math>
| |
|
| |
| ::BT(M)(<math><k> * \alpha</math>) = BT(M_k)(<math>\alpha</math>) <math>\forall \alpha</math> and k < m
| |
|
| |
| :::::= undefined <math>\forall \alpha</math> and k <math>\ge</math> 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,<math>\subseteq</math>) on the Scott topology, with ordering of Böhm tree's denoted M<math>\subseteq</math> N, meaning M, N are trees and M results from N. The [[tree topology]] on the set <math>\Gamma</math> is the smallest set allowing for a continuous map
| |
| | |
| ::BT:<math>\Gamma \rightarrow </math>''B''.
| |
| | |
| An equivalent definition would be to say the open sets of <math>\Gamma</math> are the image of the inverse Böhm tree <math> BT^{-1}</math> (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 allow new modes of thought concerning the behaviors of computer science. The binary operator within the λ-algebra A is application. Application is denoted <math>\cdot</math> and is said to give structure <math>A=(X, \cdot)</math>. 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. The λ algebra becomes a combinatory algebra M combined with a syntactic operator λ* that transforms a term ''B(x,y)'', with constants in ''M'', into C(<math>\hat{y}</math>)<math>\equiv</math> λ* x.B(x,<math>\hat{y}</math>). It is also possible to define an [[extension]] model to circumvent the need of the λ* operator by allowing <math>\forall</math>x (fx =gx) <math>\rightarrow</math> 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. Relevant attributes of the combinatory algebra are:
| |
| | |
| Within combinatory algebra there exists ''applicative structures''. An applicative structure W is a combinatory algebra provided:
| |
| ::<math>\cdot</math>W is non-trival, meaning W has [[cardinality]] > 1
| |
| ::<math>\cdot</math>W exibits combinatory completeness (see [[combinatory logic|completeness of the S-K basis]]). More specifically: for every term A ∈ the set of terms of W, and <math> x_1, ... , x_n </math> with the free variables of A within <math>{x_1, ... ,x_n}</math> then:
| |
| ::: <math> \exists f \forall x_1 \cdot \cdot \cdot x_n</math> where <math> fx_1 \cdot \cdot \cdot x_n = A </math>
| |
| | |
| The combiniatory algebra is:
| |
| | |
| :<math>\cdot</math>Never commutative
| |
| | |
| :<math>\cdot</math>Not associative.
| |
| | |
| :<math>\cdot</math>Never finite.
| |
| | |
| :<math>\cdot</math>Never recursive.
| |
| | |
| Combinatory algebras remain unable to act as the algebraic structure for λ-calculus, the lack of recursion being a major disadvantage. However the existence of an applicative term <math>A(x, \vec{y}</math>) provides a good starting point to build a λ-calculus algebra. What is needed is the introduction of a [[lambda term]], i.e. include λx.A(x, <math>\vec{y}</math>).
| |
| | |
| We begin by exploiting the fact that within a combinatory algebra M, with A(x, <math>\vec{y}</math>) within the set of terms, then:
| |
| ::<math>\forall \vec{y}</math> <math>\exists b</math> s.t. bx = A(x, <math>\vec{y}</math>).
| |
| We then require b have a dependence on <math> \vec{y}</math> resulting in:
| |
| :::<math>\forall x</math> B(<math>\vec{y}</math>)x = A(x, <math>\vec{y}</math>).
| |
| B(<math>\vec{y}</math>) becomes equivalent to a λ term, and is therefore suitably defined as follows: B(<math>\vec{y}) \equiv</math> λ*.
| |
| | |
| A ''pre-λ-algebra'' (pλA) can now be defined.
| |
| ::pλA is an applicative structure W = (X,<math>\cdot</math>) 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) <math>\equiv</math> 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:
| |
| ::<math>(\beta)</math> (λ*x.A)x = A
| |
| ::<math>\alpha_{1}</math>λ*x.A<math>\equiv</math> λ*x.A[x:=y] provided y is not a free variable of A
| |
| ::<math>\alpha_{2}</math>(λ*x.A)[y:=z]<math>\equiv</math>λ*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 <math>\Gamma(W) </math> with the following requirements:
| |
| ::a ∈ W <math>\Rightarrow c_{a} \isin \Gamma(W) </math>
| |
| ::x ∈ <math> \Gamma(W) </math> for x ∈ (<math> v_0, v_1, ... </math>)
| |
| ::M,N ∈ <math>\Gamma(W) \Rightarrow </math> (MN) ∈ <math> \Gamma(W) </math>
| |
| ::M ∈ <math>\Gamma(W) \Rightarrow</math> (λx.M) ∈ <math>\Gamma(W)</math>
| |
| | |
| A mapping from the terms within <math>\Gamma(W)</math> to all λ terms within W, denoted '''*''' : <math>\Gamma(W)\rightarrow \Tau(W) </math>, can then be designed as follows:
| |
| ::<math>v_{i}^{*} = w_i, c_{a}^{*} = c_a </math>
| |
| ::(MN)* = M* N*
| |
| ::(λx.M)* = λ* x*.M*
| |
| | |
| We now define '''λ'''(M) to denote the extension after evaluating the terms within <math>\Gamma(W)</math>.
| |
| ::λx.(λy.yx)<math>c_a</math> = λx.<math>c_a</math>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 ∈ <math>\Gamma</math>(W):
| |
| :::'''λ'''(W) [[turnstile (symbol)|<math>\vdash</math>]] M = N <math>\Rightarrow</math> W <math> \vDash </math> 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 theory|group theoretic]] manner.
| |
| | |
| ==References==
| |
| | |
| {{reflist}}
| |
| | |
| [[Category:Computational topology]]
| |
| [[Category:Computational complexity theory]]
| |
| [[Category:Computational science|Topology]]
| |
