Aboco de la Lambdokalkulo

Esperanto • English

Laste ĝisdatigita: la 16-an de marto 2022

Oni ne vere komprenas ion krom se oni povas klarigi ĝin al sia avino.
—Alberto EJNŜTEJNO

joel-filipe-Wc8k-KryEPM-unsplash

Enhavotabelo

Enkonduko
Etaj paŝoj
Ni nombru
Vereco, malvereco, kaj amikoj
- Buleaj valoroj
- Logikaj funkciadoj
Ni nombru malantaŭen
- Antaŭanto
- Subtraho
Finrimarkoj
Fontindikoj

Ĉi tiu estas mia provo por fari ja tion, tamen la avino ĉi tie estas mi mem. Mi firme kredas, ke mi ne vere povas kompreni ion, krom se mi povas klarigi ĝin. Ĉi tiu afiŝo estas malstreĉa aliro por fari tion, kaj evitas tre teĥnikajn temojn, krom se ili estas ege bezonitaj.

Kio ĝi estas?

La lambdokalkulo estas minimuma sistemo por esprimi komputadon kiu konformas al la universalaj modeloj de komputado, igi ĝin mem universala modelo de komputado. Alidire ĝi povas esti nomita kiel unu el la plej simplaj programlingvoj, tamen ĝi aspektas kaj alie kondutas el la unuj, kiuj ni kutime konas. La lambdokalkulo ankaŭ formiĝas kiel la bazo por la popolaj funkciaj programlingvoj kiuj nune uziĝas.

Ĉu oni devas lerni ĝin?

Jes kaj ne. Se oni volas kompreni la profundan meĥanismon kiel programaro funkcias, aŭ se oni volas konstrui la sekvan bonegan programlingvon, aŭ se oni simple volas aprezi la elegantecon de ĝia arto, do jes. Tamen, se oni simple volas flugi aviadilon sen scii kiel ĝi funkcias, do ne.

Kion oni devas fari?

Diskutante novajn konceptojn, tre gravas aranĝi la aksiomojn aŭ la komencajn regularojn. Pensu ĝin kiel difini novajn terminojn en ludo, kaj doni al ili sencojn. La koncepto, en kiu, ĉi tiuj sencoj vivas, estas gravaj. Ekzemple, laŭ la ĝardenisto, la akvokondukilo estas uzata por akvi la plantojn, dum laŭ la fajrobrigadisto, la akvokondukilo estas uzata por mortigi la fajron. Kiam la ĝardenisto aŭ la fajrobrigadisto tenas la akvokondukilon, ili ne dubas kion ili tenas aŭ kio estas la celumo. Oni simple kredas en sia intuo, por precizigi la signifon de la akvokondukilo en la tempo, ke ili tenis ĝin.

La vorto alta havas plurajn signifojn. Tamen, en ĉiom da difinitaj signifoj de la vorto, ne ekzistas apriora scio de la valoro de la vorto. Ni akceptas la difinon samkiel ĝi estas. Ni devas konsenti al la uzado de la vorto en la limigita kunteksto de la uzantoj de la vorto. Se ni provas devii el la establiĝita signifo de la vorto, ekzemple, se ni hazarde kreas novan difinon de la vorto pro kaprico, plej verŝajne ĝi ne estos akceptita. Ni bezonas kredi la difinitajn kaj montritajn signifojn de la vorto, por ke ĝi havu sencon al ni. La sama veras pri la lambdokalkulo—ni aŭ akcepti ĉi tiujn aksiomojn kaj operaciu en ĝia domajno, aŭ ni vivu en Neverlando.

Etaj paŝoj

Funkcioj

Kerna ludanto en la lambdokalkulo estas la nocio de funkcio. Plejmulto da ni konas funkciojn en altnivelaj programlingvoj, tamen funkcioj en la lambdokalkulo iomete malsimilas—ili devas havi plej minimume unu parametron. En plejparto de produktadaj programlingvoj nune uzataj, oni povas alvoki funkcion kiu ne prenas argumenton. Tio okazas kutime por kromefikoj. Tamen, lamdokalkule, apenaŭa minimumo de unu argumento estas devigita. Jen kiel minimuna funkcio en la lambdokalkulo aspektas. La jena

λx.x

estas ekvivalenta al

(λz.z)
(λc.c)

Ĉi tiu ekvivalenteco nomiĝas la alfakonverto. La nomoj ne gravas, tiel longe kiel ili estas uzitaj konsekvence. Rondkrampoj povas esti uzataj por forigi plursensecon aplikante funkciojn. La funkcio ĉi-supre ekvivalentas al:

(λx.x)

La Greka litero λ montras, ke la ĉirkaŭa kunteksto estas funkcio—aŭ iu, kiu povas esti aplikata. The simbol λ estas uzata anstataŭ alia simbolo pro la kompostada atentindaĵo kiu estas diskutita ĉi tie. Do, ne maltrankviliĝu. Oni simple povas uzi ĝin.

Kio sekvas post la simbolo λ, antaŭ la signo ., estas la parametro. Teĥnike, ĝi povas esti ia simbolo. Tio simple signifas la nomon, kiu povas esti uzita aplikante tiun funkcion, por referenci al ĝia argumento.

La simbolo ., ĉi tie, estas la apartigilo inter la parametra listo kaj la funkciokorpo. En la funkcio (λx.x), la korpo simple estas la simbolo x.

Variabloj

En la lambdokalkulo, la simboloj kiuj estas uzataj ene funkcio nomiĝas variabloj. Reiri al la difinita funkcio supre:

(λx.x)

La parametro x estas variablo, kiu ligiĝas tial, ke ĝi estas sandviĉiĝita inter λ kaj .. Tamen, en la funkcio:

(λx.xy)

La parametro y estas variablo kiu liberas tial, ke ĝi ne vivas inter λ kaj ..

Funkciapliko

Por uzi funkcion, oni devas apliki ĝin al io. La ligitaj variabloj estas anstataŭigitaj per tiuj, kiuj ili estas aplikitaj—procedo nomiĝas betaredukto.

Ekzemple:

(λx.x)y
y

Ni disapartigu ĝin:

Apliki (λx.x) al y:
Konsumi la argumentojn, tiam anstataŭigi ĉiujn instancojn de x en la korpo, per y.

«Atendu, ĝi nur revenas la argumenton y.» oni eble diras. Tio pravas. La funkcio (λx.x) estas la identeca funkcio—unuopa-parametra funkcio kiu revenas kion ajn ĝi estas aplikita al.

Funkcioj ne estas limigitaj, por esti aplikataj al simboloj. Ili ankaŭ povas esti aplikataj al aliaj funkcioj.

(λx.x)(λy.y)
(λy.y)

En la ekzemplo ĉi-supre, la identeca funkcio estas aplikata al identeca funkcio, revenonte identecan funkcion.

Jen alia apliko kun liberaj variabloj:

(λa.ab)(λy.y)
(λy.y)b
b

La ligita variablo a estis anstataŭigita per (λy.y), kiu estas do aplikata al la libera variablo b, rezultante al b.

Memoru, ke la jena funkciapliko:

(λx.(λy.y))ab
(λy.y)b
b

ekvivalentas al:

(λxy.y)ab
b

Havi plurajn parametrajn nomojn estas steno de pluraj lambdoj, igante al la malplilongigita versio la efekton, ke ĝi konsumas plurajn argumentojn samtempe.

Ene la korpo da funkcio, kiam du simboloj tuŝas al si reciproke, la unua simbolo estas supozita por esti funkcio aplikata al la dua simbolo, sen la rondkrampoj. Ekzemple, la jena kodaĵo:

(λxy.xy)

ekvivalentas al:

(λxy.x(y))

Ni nombru

Komenco

Pro tio ke preskaŭ ĉio en la lambdokalkulo esprimiĝas kiel funkcioj, ĝia opinio pri nombroj unikas. Aserteble, la plej grava nombro en la lambdokalkulo estas la nulo—0. Jen la difino de 0:

(λsz.z)

Por oportunecaj celoj, ni etikedu tiun esprimon kiel 0, kun la simbolo = legita kiel «ekvivalentas al.»

0 ≡ (λsz.z)

Konstrui el 0, ni nombru la unuajn tri nombradaj nombroj:

1 ≡ (λsz.s(z))
2 ≡ (λsz.s(s(z)))
3 ≡ (λsz.s(s(s(z))))

Postanto

La postanto de entjero estas difinita kiel la sekva entjero, kalkulante supren. Do, la postanto de 0 estas 1. Jen la difino de la postanta funkcio:

S ≡ (λxyz.y(xyz))

Ni provu tiun per 0. En la ekzemploj malsupre, la = simbolo estas legita kiel «malpligrandiĝas al»:

S0
≡ (λxyz.y(xyz))(λsz.z)
= (λyz.y((λsz.z)yz))
= (λyz.y((λz.z)z))
= (λyz.y(z))
≡ 1

Ni disapartigu ĝin:

Precizigi la postanton (S) de nulo (0);
Precizigi la ekvivalentan funkcian notadon;
Apliki (λsz.z) al y anstataŭigi la ligitan variablon s al y;
Apliki (λz.z) al z anstataŭigi la ligitan variablon z al z; kaj
La taksado ĉesas kaj liveriĝas (λyz.y(z)) , kiu estas la nombro 1.

Adicio

Kio se oni volas efektivigi 2+3? Bonŝance, la postanta funkcio povas fari tion. Oni esprimu tion kiel 2S3, en kiu, oni uzos + kiel la intermeta operatoro. Jen la difino de la adicia funkcio:

Nomo: A
Profilo: S ≡ (λxyz.y(xyz))
Enigoj: x, y
Eligoj: c
Uzado: xAy

Ni elprovu tion:

2+3 ≡ 2A3
≡ (λsz.s(sz))(λxyz.y(xyz))(λuv.u(u(uv)))
= SS3
≡ (λxyz.y(xyz))((λxyz.y(xyz))(λuv.u(u(uv))))
= (λxyz.y(xyz))(λyz.y((λuv.u(u(uv)))yz))
= (λxyz.y(xyz))(λyz.y(y(y(yz))))
≡ S4
= (λyz.y((λyz.y(y(y(yz))))yz))
= (λyz.y(y(y(y(yz)))))
≡ 5

Ni disapartigu ĝin:

Eldiri la problemon;
Precizigi la ekvivalentan funkcian notadon de 2, S, kaj 3;
Malpligrandigi ĝin donas SS3
La plena versio de SS3, kiu kongruas al 2S3 aŭ du S kaj 3;
Malpligrandigi plu;
Eĉ malpligrandigi plu;
Nun malpligrandiĝitas al S4;
Apliki S al 4; kaj
Oni alvenas ĉe 5.

Multipliko

La multiplika funkcio difinitas kiel:

Nomo: M
Profilo: (λxyz.x(yz))
Enigoj: a, b
Eligoj: c
Uzado: Mab

Male al adicio, kiu uzas intermetan sintakson, multipliki du nombrojn sekvas antaŭmetan operaciskribon. Do, por multipliki 2 kaj 3, oni diras M23.

Ni elprovu tion:

2*3 ≡ M23
≡ (λabc.a(bc))(λsz.s(sz))(λxy.x(x(xy)))
= (λc.(λsz.s(sz))((λxy.x(x(xy)))c)
= (λcz.((λxy.x(x(xy)))c)(((λxy.x(x(xy)))c)z))
= (λcz.(λy.c(c(cy))))(c(c(cz)))
= (λcz.c(c(c(c(c(cz))))))
≡ 6

Multipliki du nombrojn en la lambdokalkulo estas tiom facila kaj simpla. Tamen, antaŭ ol daŭri al pli aritmetikaj funkcioj, ni unue traktu verecajn valorojn kaj kondiĉaĵojn, kiuj estas antaŭkondiĉoj en lerni la aliajn funkciojn.

Vereco, malvereco, kaj amikoj

Buleaj valoroj

La prezentoj de vereco kaj malvereco en la lambdokalkulo mallongas kaj elegantas:

T ≡ (λxy.x)
F ≡ (λxy.y)

En agado:

Tab ≡ (λxy.x)ab = a
Fab ≡ (λxy.y)ab = b

Logikaj funkciadoj

La tri abocaj operatoroj: KAJ, AŬ, kaj NE:

∧ ≡ λxy.xy(λuv.v) ≡ λxy.xyF
∨ ≡ λxy.x(λuv.u)y ≡ λxy.xTy
¬ ≡ λx.x(λuv.v)(λab.a) ≡ λx.xFT

Ni kontrolu se ¬T estas jam F:

¬T
≡ λx.x(λuv.v)(λab.a)(λcd.c)
≡ TFT
≡ (λcd.c)(λuv.v)(λab.a)
= (λuv.v)
≡ F

Ni nombru malantŭen

Antaŭanto

La antaŭanto de nombro estas difinita kiel la antaŭa nombro precizigita kiam kalkuli malantaŭen. La motivo kial la diskuto pri la antaŭanta funkcio estas farita aparte estas, ke ne estas intue por lerni ĝin komence, kaj la scio pri la aliaj funckioj gravas lerni ĝin.

Ni supozu, ke oni havas duon, io kiel (y, x), en kiu, la unua ero estas unu paŝo supre, aŭ la postanto de la dua ero. Pro tio ke la unua ero estas la postanto, tio signifas ke la dua ero estas la antaŭanto. Vide:

(z+1, z) = (z, z-1)

Pro tio:

x = Py iff y = Sx

Tio signifas, ke x estas la antaŭanto de y, se kaj nur se, y estas la postanto de x. Do, por precizigi la antaŭanton de nombro x, oni kreu duon kiel supre, tiam elektu la duan eron:

Ni difinu iujn bazajn unuojn. Duo aspektas kiel:

(λz.zab)

Kaj la plej mallonga unuo de duo estas:

(λz.z00) ≡ (λz.z(λsz.z)(λsz.z))

Por elekti la unuan kaj duan erojn de duo, oni uzas T kaj F:

(λz.zab)(λxy.x) ≡ (λz.zab)T = Tab = a
(λz.zab)(λxy.y) ≡ (λz.zab)F = Fab = b

Oni bezonas funkcion kiu ricevas duon kaj kreas novan duon, en kiu, la unua ero estas la postanto de la unua ero de la enigo kaj la dua ero estas la unua ero de la enigo:

Nomo: Q
Profilo: (λpz.z(S(pT))(pT))
Enigoj: (a, b)
Eligoj: (S(a), a)
Uzado: Q(a,b)

Ni elprovu tion:

Q(λz.z00)
≡ (λpz.z(S(pT))(pT))(λz.z00)
= (λpz.z(S(pT))(pT))(λz.z(λsz.z)(λsz.z))
= (λz.z(λsz.s(z)(λsz.z)))
≡ (λz.z10)

Aspektas prave. Oni nun povas konstrui la antaŭantan funkcion:

Nomo: P
Profilo: (λn.nQ(λz.z00))F
Enigoj: N, en kiu, estas naturnombro
Eligoj: N-1
Uzado: PN

Ni elprovu tion:

P1
≡ ((λn.nQ(λz.z00))F)1
≡ ((λn.nQ(λz.z00))F)(λsz.s(z))
= (1Q(λz.z00))F
= ((λsz.s(z)((λpz.z((S(pT))(pT)))(λz.z(λsz.z)(λsz.z)))))(λxy.y)
= (λz.((λpz.z((S(pT))(pT)))(λz.z(λsz.z)(λsz.z)))z)(λxy.y)
≡ (λu.((λpz.z((S(pT))(pT)))(λz.z(λsz.z)(λsz.z)))u)(λxy.y)
= ((λpz.z((S(pT))(pT)))(λz.z(λsz.z)(λsz.z)))(λxy.y)
= (λz.z((S((λz.z(λsz.z)(λsz.z))T)((λz.z(λsz.z)(λsz.z))T))))(λxy.y)
= (λz.z((S(λsz.z)(λsz.z))))(λxy.y)
= (λz.z((λsz.s(z)(λsz.z))))(λxy.y)
= (λxy.y)((λsz.s(z)(λsz.z)))
= (λsz.z)
≡ 0

Subtraho

Nu, nun ke oni havas la antaŭantan funkcion, oni nun povas konstrui la subtrahan funkcion.

B ≡ (λxy.yPx)

Ni elprovu tion:

B11
≡ (λxy.yPx) (λsz.s(z)) (λsz.s(z))
= (λsz.s(z)) (P(λsz.s(z)))
= (λsz.s(z)) (λsz.z)
= (λz.(λsz.z)z)
= (λz.(λz.z))
≡ (λsz.z)
≡ 0

Finrimarkoj

Oni simple ungogratis la tegon de la lambdokalkulo, tamen oni ĵus spektis ĝian vastegan espriman potencon, konsidere al kiel minimune la sistemo estas difinita.

Dank’ al Lucas LUGAO pro la korektoj.