Calculo lambda, creato principto per Alonzo Church, es lingua de programmatura computatro maximo parvo. Quamquam non habe numero, serie de charactere vel ullo typo de data non functionale, id pote repraesenta omne machina de Turing.
Tres elemento compone calculo lambda: quantitate variabile (q.v.), functione et applicatione.
Elemento | Syntaxe | Exemplo |
---|---|---|
Quantitate variabile | <nomine> |
x |
Functione | λ<parametro>.<corpore> |
λx.x |
Applicatione | <functione><q.v. aut functione> |
(λx.x)a |
Functione fundamentale es identitate: λx.x
cum argumento primo x
et cum
corpore secundo x
. In mathematica, nos scribe id: x↦x
.
x
es q.v. ligato nam id es et in copore et
argumento.λx.y
, y
es q.v. libero nam non es declarato ante.Valutatione es facto per reductione beta (reductione β) que es essentialiter substitutione lexicale.
Dum valutatione de formula (λx.x)a
, nos substitue omne evento de x
in
corpore de functione pro a
.
(λx.x)a
vale a
(λx.y)a
vale y
Pote etiam crea functione de ordine supero: (λx.(λy.x))a
vale λy.a
.
Etsi calculo lambda solo tracta functione de uno parametro, nos pote crea
functione cum plure argumento utente methodo de Curry: λx.(λy.(λz.xyz))
es scriptura informatica de formula mathematico f: x, y, z ↦ x(y(z)))
.
Ergo, interdum, nos ute λxy.<corpore>
pro λx.λy.<corpore>
.
Es nec numero nec booleano in calculo lambda.
v = λx.λy.x
f = λx.λy.y
Primo, nos pote defini functione «si t tunc a alio b» per si = λtab.tab
.
Si t
es vero, valutatione da (λxy.x) a b
id es a
. Similiter si t
es
falso, nos obtine b
.
Secundo, nos pote defini operatore de logica:
et = λa.λb.si a b f
vel = λa.λb.si a t b
non = λa.si a f t
Nos pone:
0 = λf.λx.x
(0: f↦id
)1 = λf.λx.f x
(1: f↦f
)2 = λf.λx.f(f x)
(2: f↦f⚬f
)Cum mente generale, successore de numero n
es S n = λf.λx.f((n f) x)
(n+1: f↦f⚬fⁿ
). Id es n
est functione que da fⁿ
ex functione f
.
Postremo additione es λab.(a S)b
Got a suggestion? A correction, perhaps? Open an Issue on the Github Repo, or make a pull request yourself!
Originally contributed by Max Sun, and updated by 0 contributor(s).