| slovo | definícia |
lambda-calculus
(foldoc) | lambda-calculus
(Normally written with a Greek letter lambda).
A branch of mathematical logic developed by Alonzo Church in
the late 1930s and early 1940s, dealing with the application
of functions to their arguments. The pure lambda-calculus
contains no constants - neither numbers nor mathematical
functions such as plus - and is untyped. It consists only of
lambda abstractions (functions), variables and applications
of one function to another. All entities must therefore be
represented as functions. For example, the natural number N
can be represented as the function which applies its first
argument to its second N times (Church integer N).
Church invented lambda-calculus in order to set up a
foundational project restricting mathematics to quantities
with "effective procedures". Unfortunately, the resulting
system admits Russell's paradox in a particularly nasty way;
Church couldn't see any way to get rid of it, and gave the
project up.
Most functional programming languages are equivalent to
lambda-calculus extended with constants and types. Lisp
uses a variant of lambda notation for defining functions but
only its purely functional subset is really equivalent to
lambda-calculus.
See reduction.
(1995-04-13)
|
| | podobné slovo | definícia |
knights of the lambda-calculus
(foldoc) | Knights of the Lambda-Calculus
A semi-mythical organisation of wizardly LISP and Scheme
hackers. The name refers to a mathematical formalism invented
by Alonzo Church, with which LISP is intimately connected.
There is no enrollment list and the criteria for induction are
unclear, but one well-known LISPer has been known to give out
buttons and, in general, the *members* know who they are.
[Jargon File]
|
polymorphic lambda-calculus
(foldoc) | polymorphic lambda-calculus
System F
(Or "second order typed lambda-calculus",
"System F", "Lambda-2"). An extension of {typed
lambda-calculus} allowing functions which take types as
parameters. E.g. the polymorphic function "twice" may be
written:
twice = /\ t . \ (f :: t -> t) . \ (x :: t) . f (f x)
(where "/\" is an upper case Greek lambda and "(v :: T)" is
usually written as v with subscript T). The parameter t will
be bound to the type to which twice is applied, e.g.:
twice Int
takes and returns a function of type Int -> Int. (Actual type
arguments are often written in square brackets [ ]). Function
twice itself has a higher type:
twice :: Delta t . (t -> t) -> (t -> t)
(where Delta is an upper case Greek delta). Thus /\
introduces an object which is a function of a type and Delta
introduces a type which is a function of a type.
Polymorphic lambda-calculus was invented by Jean-Yves Girard
in 1971 and independently by John C. Reynolds in 1974.
["Proofs and Types", J-Y. Girard, Cambridge U Press 1989].
(2005-03-07)
|
pure lambda-calculus
(foldoc) | pure lambda-calculus
Lambda-calculus with no constants, only functions expressed
as lambda abstractions.
(1994-10-27)
|
second-order lambda-calculus
(foldoc) | Second-Order Lambda-calculus
(SOL) A typed lambda-calculus.
["Abstract Types have Existential Type", J. Mitchell et al,
12th POPL, ACM 1985, pp. 37-51].
(1995-07-29)
|
typed lambda-calculus
(foldoc) | typed lambda-calculus
(TLC) A variety of lambda-calculus in which every
term is labelled with a type.
A function application (A B) is only synctactically valid if
A has type s --> t, where the type of B is s (or an instance
or s in a polymorphic language) and t is any type.
If the types allowed for terms are restricted, e.g. to
Hindley-Milner types then no term may be applied to itself,
thus avoiding one kind of non-terminating evaluation.
Most functional programming languages, e.g. Haskell, ML,
are closely based on variants of the typed lambda-calculus.
(1995-03-25)
|
|