Deductive lambda calculus: Difference between revisions

Browse history interactively ← Previous editContent deleted Content addedVisual WikitextInline

Revision as of 02:21, 21 February 2014 editThepigdog (talk \| contribs)Extended confirmed users5,174 edits →Example: No solutions -> One solution ← Previous edit		Latest revision as of 00:55, 19 February 2024 edit undoAxelBoldt (talk \| contribs)Administrators44,507 edits no refs support the material here; seems to be original research. Redirecting to lambda calculusTags: New redirect Visual edit: Switched
(182 intermediate revisions by 26 users not shown)
Line 1:		Line 1:
			#REDIRECT ]
	'''Deductive lambda calculus''' considers what happens when ] are regarded as mathematical expressions. ] is defined as a programming language where evaluation proceeds by performing reductions on an expression until it is in normal form. Considered as mathematics, each reduction would not alter the value of the expression. The expression would equal the reduction of the expression.

	== History ==

	Alonzo Church invented the Lambda Calculus in the 1930s, originally to provide a new and simpler basis for mathematics<ref>A. Church, "A set of postulates for the foundation of logic", ''Annals of Mathematics'', Series 2, 33:346–366 (1932).</ref><ref>For a full history, see Cardone and Hindley's "History of Lambda-calculus and Combinatory Logic" (2006).</ref>. However soon after inventing it major logic problems were identified with the definition of the Lambda Abstraction<ref>{{Cite journal \|first=S. C. \|last=Kleene \|lastauthoramp=yes \|first2=J. B. \|last2=Rosser \|title=The inconsistency of certain formal logics \|journal=] \|volume=36 \|issue=3 \|pages=630–636 \|year=1935 \|doi=10.2307/1968646 }}</ref>.

	The ] is an implementation of ] in ]. Combinatory Logic is closely related to Lambda Calculus. ] found that the key step in this paradox could be used to implement the simpler ]. The existence of this paradox meant that the Combinatory Logic, and Lambda Calculus, could not be both consistent and complete as a ]<ref>
	The Inconsistency of Certain Formal Logic
	Haskell B. Curry
	The Journal of Symbolic Logic
	Vol. 7, No. 3 (Sep., 1942), pp. 115-117
	Published by: Association for Symbolic Logic
	Article Stable URL: http://www.jstor.org/stable/2269292
	</ref>.

	Later the Lambda Calculus was resurrected as a definition of a programming language.

	== Interpretation of Lambda calculus as mathematics ==

	In the mathematical interpretation, lambda expressions represent values. ] are deductive steps that do not alter the values of expressions.

	=== Eta reduction as mathematics ===

	An eta-redex is defined by,
	:<math>x \not \in \operatorname{FV}(f) \to \operatorname{eta-redex} = f </math>

	In the mathematical interpretation,
	: <math>\operatorname{eta-redex} = X </math>

	Taking f to be a variable then,
	: <math>\lambda x.(f\ x) = f </math>
	or by letting <math>f\ x = y </math>
	: <math>f\ x = y \iff f = \lambda x.y </math>

	This definition defines <math> \lambda x.y </math> to be the solution for ''f'' in the equation,
	: <math>f\ x = y </math>

	=== Beta reduction as mathematics ===

	A beta redex is,
	: <math>\operatorname{beta-redex} = b </math>
	and as,
	: <math>\operatorname{beta-redex} = X </math>
	then,
	: <math>\lambda x.b z = b </math>

	This rule is implied by the instantiation of quantified variables. If,
	: <math>\forall x: f\ x = y </math>

	then <math>f\ z </math> is the expression y with the quantified variable x instantiated as z.
	: <math>f\ z = y </math>
	so,
	: <math>\lambda x.y\ z = y </math>

	As beta reduction is implied from eta reduction, there is no contradiction between the two definitions.

	== Logical inconsistency ==

	From eta reduction,
	: <math>f\ x = y \iff f = \lambda x.y </math>

	This rule may be interpreted as defining <math>\lambda x.y </math> to be the solution of the equation <math>f\ x = y </math>. In defining the solution to the equation in terms of ''x'' and ''y'' the definition implicitly assumes that there is one and only function ''f'' that satisfies the equation. However, for some equations there may be none or multiple solutions. The definition may be compared with defining <math>\sqrt{}</math> by,

	: <math>y = x^2 \iff x = \sqrt{y} </math>

	This is not a valid definition as the equation <math>y = x^2</math> has two solutions. The proper definition is,

	: <math>(y = x^2 \and x >= 0) \iff x = \sqrt{y} </math>

	An expression in mathematics may represent multiple values if it has ]. The variables may be ]. Existential quantification turns an equation into a ] of equations, with each variable populated with single value in each equation.

	The solution set for <math>f</math> in <math>f\ x = y</math> is,
	: <math>\{f: f\ x = y \} </math>

	For the definition <math>(f\ x = y \iff f = \lambda x.y)</math> to be valid there must be only one solution in this solution set.

	The mathematical (or extensional) definition of function equality is that two functions are equal if they perform the same mapping;
	: <math>f = g \iff (\forall x f\ x = g\ x)</math>

	Using this definition the cardinality condition giving a valid definition of a lambda abstraction is,
	: <math>(\forall x \|\{f\ x: f\ x = y \}\| = 1) \to (f\ x = y \iff f = \lambda x.y)</math>

	The left hand side may often be shown to be false where <math>x = f</math>

	=== No solutions ===

	Starting with the equation,
	: <math> x = \neg x </math>

	defining <math>x = y\ y</math> gives,
	: <math> y\ y = \neg (y\ y) </math>
	or
	: <math> x = \operatorname{let} f\ y = \neg (y\ y) \operatorname{in} f\ f </math>

	The cardinality is,
	: <math>\|\{f\ f: f\ f = \neg (f\ f) \}\| = 0 </math>

	so it is not valid to get,
	: <math> (f\ x = y \iff f = \lambda x.y)</math>

	If we go ahead anyway and ],
	: <math>x = (\lambda f.f\ f) (\lambda x.\neg(x\ x)) </math>

	Then,
	:<math>f\ f = (\lambda x.\neg\ (x\ x))\ (\lambda x.\neg\ (x\ x)) = \neg\ (\lambda.x \neg\ (x\ x))\ (\lambda x.\neg\ (x\ x))</math>

	There is no solution to the equation, and the value does not exist.

	=== Multiple solutions ===

	Also it is possible to construct lambda expressions for which there are multiple values. For example,
	: <math>4 = x^2</math>
	gives,
	: <math>x = 4/x</math>
	Defining <math>x = y\ y</math>
	: <math>y\ y = 4/(y\ y)</math>
	or,
	: <math>x = \operatorname{let} f\ y = \frac{4}{y\ y} \operatorname{in} f\ f</math>

	The cardinality is given by,
	: <math>\|\{f\ f: f\ f = \frac{4}{f\ f} \}\| = 2 </math>

	If we go ahead anyway and ],
	: <math>x = (\lambda f.f\ f) (\lambda x.\frac{4}{x\ x}) </math>

	Then,
	:<math>f\ f = (\lambda x.\frac{4}{x\ x})\ (\lambda x.\frac{4}{x\ x}) = \frac{4}{(\lambda.x \frac{4}{x\ x}\ (\lambda x.\frac{4}{x\ x})}</math>

	so,
	:<math>(f\ f)^2 = 4 </math>

	== Intensional versus extensional equality ==

	Another difficulty for the interpretation of lambda calculus as a deductive system is the representation of values as functions. The untyped lambda calculus is implemented by performing reductions on a lambda term, until the term is in normal form. The ] interpretation<ref>
	{{cite web
	\|last=Selinger
	\|first=Peter
	\|title=Lecture Notes on Lambda Calculus (PDF)
	\|url=http://www.mscs.dal.ca/~selinger/papers/#lambdanotes.pdf
	\|pages=6}}
	</ref>
	<ref>
	{{cite web
	\|url=http://plato.stanford.edu/entries/lambda-calculus/
	\|publisher=Stanford
	\|title=Lambda calculus - intensionality
	\|page=1.2 Intensionality
	}}
	</ref> of equality is that the reduction of a lambda term to normal form is the value of the lambda term.

	This interpretation considers the identify of a lambda expression to be its structure. Two lambda terms are equal if they are alpha convertible.

	One way to describe this is that extensional equality describes equality of functions, where as intensional equality describes equality of function implementations.

	The mathematical (or ]) definition of function equality is that two functions are equal if they perform the same mapping;
	: <math>f = g \iff (\forall x f\ x = g\ x)</math>

	The extensional definition of equality is incompatible with the intensional definition. This can be seen in the example below, where applying a mathematical law changes a function to an equivalent function, yet the intensional interpretation of equality says that the two functions are not equal. This shows the untyped lambda calculus with intensional equality is inconsistent with mathematics as a deductive system.

	This incompatibly is created by considering lambda terms as values. In ] this is not a significant problem, because built-in types may be added to carry values that are in a ] and have both extensional and intensional equality.

	=== Example ===

	In ], the ] implies that <math>2 * (r + s) = 2r + 2s</math>. Using the ] the left and right hand sides may be represented as lambda terms.

	Left hand side;
	:<math>\lambda r.\lambda s.(\operatorname{mult}\ 2\ (\operatorname{plus}\ r\ s)</math>
	:<math>\lambda r.\lambda s.(\lambda m.\lambda n.\lambda f. m\ (n\ f))\ (\lambda f.\lambda x.f\ (f\ x))\ ((\lambda m.\lambda n.\lambda f.\lambda x. m\ f\ (n\ f\ x))\ r\ s)</math>
	:<math>\lambda r.\lambda s.\lambda f.\lambda x.r\ f\ (s\ f\ (r\ f\ (s\ f\ x)))</math>

	Right hand side;
	:<math>\lambda r.\lambda s.\operatorname{plus}\ (\operatorname{mult}\ 2\ r)\ (\operatorname{mult}\ 2\ s)</math>
	:<math>\lambda r.\lambda s.(\lambda m.\lambda n.\lambda f.\lambda x. m\ f\ (n\ f\ x))\ ((\lambda m.\lambda n.\lambda f. m\ (n\ f))\ (\lambda f.\lambda x.f\ (f\ x))\ r)\ ((\lambda m.\lambda n.\lambda f. m\ (n\ f))\ (\lambda f.\lambda x.f\ (f\ x))\ s)</math>
	:<math>\lambda r.\lambda s.\lambda f.\lambda x.r\ f\ (r\ f\ (s\ f\ (s\ f\ x)))</math>

	Comparison;
	:<math>\lambda r.\lambda s.\lambda f.\lambda x.r\ f\ (s\ f\ (r\ f\ (s\ f\ x)))</math>
	:<math>\lambda r.\lambda s.\lambda f.\lambda x.r\ f\ (r\ f\ (s\ f\ (s\ f\ x)))</math>

	The two terms beta reduce to similar expressions. Still they are not alpha convertible, so according to intensional equality, the left hand side and the right hand side are different functions. But according to the distributive law the two functions are the same. If the two functions are applied to the same Church numerals they produce the same result, so in that sense the distributive law holds. But the functions themselves are not equal.

	This a significant problem because all values in the untyped lambda calculus are terms that define functions. So any mathematically correct transformation of a lambda calculus program may change the meaning of the program.

	== Set theoretic domain ==

	Lambda abstractions are functions of functions. A natural step is to define a domain for the lambda abstraction as a set of all functions.

	The set of all functions from a domain D to a range R is defined by,
	: <math>f \in F \iff (\forall x : x \in D \implies f\ x \in R) </math>

	Then the definition of the set of all functions of functions is,

	: <math>f \in F \iff (\forall x : x \in F \implies f\ x \in F) </math>

	This definition is an unsolved equation for F. So is there a solution for F?

	Consider a version of ]. Suppose there is a function ''g'' that is defined on all functions other than itself.
	: <math>g\ g \not \in F</math>
	: <math>x \ne g \implies g\ x \in F</math>

	Firstly assume ''g'' is in ''F''. This will be used to deduce a falsehood.
	: <math>g \in F \iff (\forall x : x \in F \implies g\ x \in F) </math>
	instantiate ''x'' as ''g''.
	: <math> \implies (g \in F \implies g\ g\in F) </math>
	: <math> \implies g\ g \in F</math>

	which is false because.
	: <math>g\ g \not \in F</math>

	Secondly assume ''g'' not in ''F'',
	: <math>g \not \in F</math>

	From the definition of all functions of functions, it can be shown that,
	: <math> (\forall x : x \in F \implies g\ x \in F) \implies g \in F</math>
	: <math> (\forall x : x \in F \implies g \ne x \implies g\ x \in F) \implies g \in F</math>
	: <math> (\forall x : x \in F \implies \operatorname{true}) \implies g \in F</math>
	: <math> \operatorname{true} \implies g \in F</math>
	: <math> g \in F</math>

	which is false because we assumed,
	: <math>g \not \in F</math>

	So ''g'' is an element of ''F'' and not an element of ''F''.

	Therefore, if there exists a function that may not be applied to itself, then there is no set ''F'' satisfying the above definition of "all functions". This result leads us to question the set theoretic approach to lambda calculus. The usual approach to defining sets of functions is to build a ]. However, because the only type in the untyped lambda calculus is the function, it is not clear how to do this.

	== Domain of lambda calculus ==

	The problems with lambda abstraction arose when a domain was imposed on it. If the lambda abstraction is allowed to define the domain, instead of imposing the domain upon the lambda abstraction, these problems no longer appear.

	Lambda calculus is defined by beta reductions and eta reductions. Interpreting reduction as defining equality gives an implicit domain for the lambda calculus. The rules are,
	* Every lambda abstraction has one value.
	* The beta reduction of a lambda term has the same value.
	* The eta reduction of a lambda term has the same value.
	* If two lambda terms can not be shown to be equal, they are not equal.

	=== Example: No solutions -> One solution ===

	For example the equation <math>x = \neg x</math> may be coded with ] and using ] as,
	:<math>\operatorname{not}_1 = \lambda p.\lambda a.\lambda b.p\ b\ a</math>
	:<math>(\lambda f.(\lambda x.f\ (x\ x))\ (\lambda x.f\ (x\ x))) (\lambda p.\lambda a.\lambda b.p\ b\ a) </math>

	And the recursion is,
	:<math>(\lambda x.(\lambda p.\lambda a.\lambda b.p\ b\ a)\ (x\ x))\ (\lambda x.(\lambda p.\lambda a.\lambda b.p\ b\ a)\ (x\ x)) </math>
	:<math>(\lambda p.\lambda a.\lambda b.p\ b\ a)\ ((\lambda x.(\lambda p.\lambda a.\lambda b.p\ b\ a)\ (x\ x))\ (\lambda x.(\lambda p.\lambda a.\lambda b.p\ b\ a)\ (x\ x))) </math>
	:<math>\lambda a.\lambda b.((\lambda x.(\lambda p.\lambda a.\lambda b.p\ b\ a)\ (x\ x))\ (\lambda x.(\lambda p.\lambda a.\lambda b.p\ b\ a)\ (x\ x)))\ b\ a </math>
	: ...
	:<math>\lambda a.\lambda b.(\lambda a.\lambda b.((\lambda x.(\lambda p.\lambda a.\lambda b.p\ b\ a)\ (x\ x))\ (\lambda x.(\lambda p.\lambda a.\lambda b.p\ b\ a)\ (x\ x)))\ b\ a)\ b\ a </math>
	: ... (beta and then eta reduction)
	:<math>(\lambda x.(\lambda p.\lambda a.\lambda b.p\ b\ a)\ (x\ x))\ (\lambda x.(\lambda p.\lambda a.\lambda b.p\ b\ a)\ (x\ x)) </math>

	Which is the first line and will recurse indefinitely. The expression never reduces to normal form. However every lambda term in the reduction represents the same value. This value is distinct from the encodings for ''true'' or ''false''. It is not part of the Boolean domain but it exists in the lambda calculus domain.

	=== Example: Multiple solutions -> One solution ===

	If ] and division can be encoded using Church encoding, then the lambda calculus term called the Y combinator may be used to define a square root. The ] asserts that any computable operator (and its operands) can be represented under Church encoding. It is an achievable technical task to define such an encoding.

	Using such an encoding,
	: <math> x^2 = n \Rightarrow x = \frac{n}{x} \Rightarrow f\ x = \frac{n}{x} \and Y\ f = x</math>

	If there was an implementation of ''division'' then,
	: <math> Y (\operatorname{division} n) </math>

	represents two values in the domain of the signed numbers. However it is a lambda expression so has only one value in the lambda calculus domain. Beta reduction of this lambda term never reaches normal form. However it represents a value, so a single value in the lambda calculus domains represents two values in the signed number domain.

	==References==
	{{reflist}}

	{{math-stub}}

	]

Latest revision as of 00:55, 19 February 2024

Redirect to:

Lambda calculus