|
A typed lambda calculus is a typed formalism that uses the lambda-symbol (\lambda) to denote anonymous function abstraction. In this context, types are usually objects of a syntactic nature that are assigned to lambda terms; the exact nature of a type depends on the calculus considered (see kinds below). From a certain point of view, typed lambda calculi can be seen as refinements of the untyped lambda calculus but from another point of view, they can also be considered the more fundamental theory and untyped lambda calculus a special case with only one type. Typed lambda calculi are foundational programming languages and are the base of typed functional programming languages such as ML and Haskell and, more indirectly, typed imperative programming languages. Typed lambda calculi play an important role in the design of type systems for programming languages; here typability usually captures desirable properties of the program, e.g. the program will not cause a memory access violation. Typed lambda calculi are closely related to mathematical logic and proof theory via the Curry–Howard isomorphism and they can be considered as the internal language of classes of categories, e.g. the simply typed lambda calculus is the language of Cartesian closed categories (CCCs). Computable functions and lambda calculus A function F: N → N of natural numbers is a computable function if and only if there exists a lambda expression f such that for every pair of x, y in N, F(x)=y if and only if f x =β y, where x and y are the Church numerals corresponding to x and y, respectively and =β meaning equivalence with beta reduction. This is one of the many ways to define computability; see the Church-Turing thesis for a discussion of other approaches and their equivalence. Undecidability of equivalence There is no algorithm that takes as input two lambda expressions and outputs TRUE or FALSE depending on whether or not the two expressions are equivalent. This was historically the first problem for which undecidability could be proven. As is common for a proof of undecidability, the proof shows that no computable function can decide the equivalence. Church's thesis is then invoked to show that no algorithm can do so. Church's proof first reduces the problem to determining whether a given lambda expression has a normal form. A normal form is an equivalent expression that cannot be reduced any further under the rules imposed by the form. Then he assumes that this predicate is computable, and can hence be expressed in lambda calculus. Building on earlier work by Kleene and constructing a Gödel numbering for lambda expressions, he constructs a lambda expression e that closely follows the proof of Gödel's first incompleteness theorem. If e is applied to its own Gödel number, a contradiction results. Lambda calculus and programming languages As pointed out by Peter Landin's 1965 paper A Correspondence between ALGOL 60 and Church's Lambda-notation, sequential procedural programming languages can be understood in terms of the lambda calculus, which provides the basic mechanisms for procedural abstraction and procedure (subprogram) application. Lambda calculus reifies "functions" and makes them first-class objects, which raises implementation complexity when it is implemented. Anonymous functions Main article: Anonymous function For example in Lisp the 'square' function can be expressed as a lambda expression as follows: (lambda (x) (* x x)) The above example is an expression that evaluates to a first-class function. The symbol lambda creates an anonymous function, given a list of parameter names, (x) — just a single argument in this case, and an expression that is evaluated as the body of the function, (* x x). The Haskell example is identical. Anonymous functions are sometimes called lambda expressions. For example Pascal and many other imperative languages have long supported passing subprograms as arguments to other subprograms through the mechanism of function pointers. However, function pointers are not a sufficient condition for functions to be first class datatypes, because a function is a first class datatype if and only if new instances of the function can be created at run-time. And this run-time creation of functions is supported in Smalltalk, Javascript, and more recently in Scala, Eiffel ("agents"), C# ("delegates") and C++11, among others. Reduction strategies For more details on this topic, see Evaluation strategy. Whether a term is normalising or not, and how much work needs to be done in normalising it if it is, depends to a large extent on the reduction strategy used. The distinction between reduction strategies relates to the distinction in functional programming languages between eager evaluation and lazy evaluation. Full beta reductions Any redex can be reduced at any time. This means essentially the lack of any particular reduction strategy—with regard to reducibility, "all bets are off". Applicative order The leftmost, innermost redex is always reduced first. Intuitively this means a function's arguments are always reduced before the function itself. Applicative order always attempts to apply functions to normal forms, even when this is not possible. Most programming languages (including Lisp, ML and imperative languages like C and Java) are described as "strict", meaning that functions applied to non-normalising arguments are non-normalising. This is done essentially using applicative order, call by value reduction (see below), but usually called "eager evaluation". Normal order The leftmost, outermost redex is always reduced first. That is, whenever possible the arguments are substituted into the body of an abstraction before the arguments are reduced. Call by name As normal order, but no reductions are performed inside abstractions. For example λx.(λx.x)x is in normal form according to this strategy, although it contains the redex (λx.x)x. Call by value Only the outermost redexes are reduced: a redex is reduced only when its right hand side has reduced to a value (variable or lambda abstraction). Call by need As normal order, but function applications that would duplicate terms instead name the argument, which is then reduced only "when it is needed". Called in practical contexts "lazy evaluation". In implementations this "name" takes the form of a pointer, with the redex represented by a thunk. Applicative order is not a normalising strategy. The usual counterexample is as follows: define Ω = ωω where ω = λx.xx. This entire expression contains only one redex, namely the whole expression; its reduct is again Ω. Since this is the only available reduction, Ω has no normal form (under any evaluation strategy). Using applicative order, the expression KIΩ = (λx.λy.x) (λx.x)Ω is reduced by first reducing Ω to normal form (since it is the rightmost redex), but since Ω has no normal form, applicative order fails to find a normal form for KIΩ. In contrast, normal order is so called because it always finds a normalising reduction, if one exists. In the above example, KIΩ reduces under normal order to I, a normal form. A drawback is that redexes in the arguments may be copied, resulting in duplicated computation (for example, (λx.xx) ((λx.x)y) reduces to ((λx.x)y) ((λx.x)y) using this strategy; now there are two redexes, so full evaluation needs two more steps, but if the argument had been reduced first, there would now be none). The positive tradeoff of using applicative order is that it does not cause unnecessary computation, if all arguments are used, because it never substitutes arguments containing redexes and hence never needs to copy them (which would duplicate work). In the above example, in applicative order (λx.xx) ((λx.x)y) reduces first to (λx.xx)y and then to the normal order yy, taking two steps instead of three. Most purely functional programming languages (notably Miranda and its descendents, including Haskell), and the proof languages of theorem provers, use lazy evaluation, which is essentially the same as call by need. This is like normal order reduction, but call by need manages to avoid the duplication of work inherent in normal order reduction using sharing. In the example given above, (λx.xx) ((λx.x)y) reduces to ((λx.x)y) ((λx.x)y), which has two redexes, but in call by need they are represented using the same object rather than copied, so when one is reduced the other is too. A note about complexity While the idea of beta reduction seems simple enough, it is not an atomic step, in that it must have a non-trivial cost when estimating computational complexity.[18] To be precise, one must somehow find the location of all of the occurrences of the bound variable V in the expression E, implying a time cost, or one must keep track of these locations in some way, implying a space cost. A naïve search for the locations of V in E is O(n) in the length n of E. This has led to the study of systems that use explicit substitution. Sinot's director strings[19] offer a way of tracking the locations of free variables in expressions. Parallelism and concurrency The Church–Rosser property of the lambda calculus means that evaluation (β-reduction) can be carried out in any order, even in parallel. This means that various nondeterministic evaluation strategies are relevant. However, the lambda calculus does not offer any explicit constructs for parallelism. One can add constructs such as Futures to the lambda calculus. Other process calculi have been developed for describing communication and concurrency. Semantics The fact that lambda calculus terms act as functions on other lambda calculus terms, and even on themselves, led to questions about the semantics of the lambda calculus. Could a sensible meaning be assigned to lambda calculus terms? The natural semantics was to find a set D isomorphic to the function space D → D, of functions on itself. However, no nontrivial such D can exist, by cardinality constraints because the set of all functions from D into D has greater cardinality than D. In the 1970s, Dana Scott showed that, if only continuous functions were considered, a set or domain D with the required property could be found, thus providing a model for the lambda calculus. This work also formed the basis for the denotational semantics of programming languages. See also Applicative computing systems – Treatment of objects in the style of the lambda calculus Binary lambda calculus – A version of lambda calculus with binary I/O, a binary encoding of terms, and a designated universal machine. Calculus of constructions – A typed lambda calculus with types as first-class values Cartesian closed category – A setting for lambda calculus in category theory Categorical abstract machine – A model of computation applicable to lambda calculus Combinatory logic – A notation for mathematical logic without variables Curry–Howard isomorphism – The formal correspondence between programs and proofs Domain theory – Study of certain posets giving denotational semantics for lambda calculus Evaluation strategy – Rules for the evaluation of expressions in programming languages Explicit substitution – The theory of substitution, as used in β-reduction Harrop formula – A kind of constructive logical formula such that proofs are lambda terms Kappa calculus – A first-order analogue of lambda calculus Kleene–Rosser paradox – A demonstration that some form of lambda calculus is inconsistent Knights of the Lambda Calculus – A semi-fictional organization of LISP and Scheme hackers Lambda cube – A framework for some extensions of typed lambda calculus Lambda-mu calculus – An extension of the lambda calculus for treating classical logic Rewriting – Transformation of formulæ in formal systems SECD machine – A virtual machine designed for the lambda calculus Simply typed lambda calculus - Version(s) with a single type constructor SKI combinator calculus – A computational system based on the S, K and I combinators System F – A typed lambda calculus with type-variables Typed lambda calculus – Lambda calculus with typed variables (and functions) Universal Turing machine – A formal computing machine that is equivalent to lambda calculus Unlambda – An esoteric functional programming language based on combinatory logic Let expression – An expression close related to a lambda abstraction. Deductive lambda calculus – The consideration of the problems associated with considering lambda calculus as a Deductive system. Curry's paradox – A paradox arising from the consideration of lambda calculus as a deductive system. |
About us|Jobs|Help|Disclaimer|Advertising services|Contact us|Sign in|Website map|Search|
GMT+8, 2015-9-11 20:51 , Processed in 0.346734 second(s), 16 queries .
