Kyrkans kodning

I matematik betyder kyrklig kodning representationen (eller representationsproceduren) av data och operatorer i en lambda-kalkylprocedur. Nödvändigheten av proceduren beror på det faktum att i ren lambdakalkyl bland termerna finns det bara variabler och det finns inga konstanter. För att få fram föremål som beter sig på samma sätt som siffror tillämpas Kyrkokodning. Själva proceduren är uppkallad efter Alonzo Church , som utvecklade lambdakalkylen och banade väg för denna datakodningsmetod. I likhet med siffror kan kyrkans kodning också användas för att representera andra typer av objekt som beter sig som konstanter.

Termer som vanligtvis är primitiva i andra notationer (som heltal, booleaner, par, listor och taggade fackföreningar) representeras i kyrkans kod med funktioner av högre ordning . I en av dess formuleringar säger Turing-Church-avhandlingen att vilken beräkningsbar operator som helst (och dess operander) kan representeras i kyrkans kodning. I den otypade lambdakalkylen är funktioner den enda primitiva datatypen, och alla andra enheter är konstruerade med hjälp av kyrkans kodning.

Kyrkokodning används i allmänhet inte för den praktiska implementeringen av primitiva datatyper. Den används i syfte att på ett avgörande sätt visa att andra primitiva datatyper inte krävs för att utföra beräkningar.

Kyrkans siffror

Kyrkans siffror är representationer av naturliga tal i kyrkans kodning. En högre ordningsfunktion , som representerar ett naturligt tal n, är en funktion som mappar vilken funktion som helst till dess n-faldiga sammansättning . Enkelt uttryckt är "värdet" för en siffra ekvivalent med antalet gånger funktionen kapslar in sitt argument. $f$

f^{\circ n}=\underbrace {f\circ f\circ \cdots \circ f} _{n{\text{ gånger))}.\,

Alla kyrkans siffror är funktioner med två parametrar. Kyrkans siffror '0' , '1' , '2' , …, definieras i lambdakalkylen enligt följande:

$0\ f\ x$ betyder "tillämpa inte funktionen på alls", betyder "tillämpa funktionen 1 gång", etc.: $f$ $x$ $1\ f\ x$

siffra	Sifferdefinition	lambda uttryck
0	$0\ f\ x=x$	$0=\lambda f.\lambda xx$
ett	$1\ f\ x=f\ x$	$1=\lambda f.\lambda xf\ x$
2	$2\ f\ x=f\ (f\ x)$	$2=\lambda f.\lambda xf\ (f\ x)$
3	$3\ f\ x=f\ (f\ (f\ x))$	$3=\lambda f.\lambda xf\ (f\ (f\ x))$
⋮	⋮	⋮
$n$	$n\ f\ x=f^{n}\ x$	$n=\lambda f.\lambda xf^{\circ n}\ x$

Kyrkans siffra 3 representerar processen att tillämpa vilken funktion f som helst tre gånger. Denna funktion tillämpas sekventiellt först på parametern som skickas till den och sedan på resultatet som erhålls som ett resultat av dess tidigare tillämpning.

Beräkningar med kyrkans siffror

Aritmetiska operationer på siffror kan representeras av funktioner på kyrkans siffror. Dessa funktioner kan definieras i lambda-kalkylen eller implementeras i de flesta funktionella programmeringsspråk (se Konvertera lambda-uttryck till funktioner ).

Kodning Booleans

Kyrkans booleaner är resultatet av kyrkans kodning som tillämpas på representationen av de booleska värdena sant och falskt. Vissa programmeringsspråk använder dem som en implementeringsmodell för boolesk aritmetik. Exempel på sådana språk är Smalltalk och Pico .

Boolesk logik kan ses som ett val. Kyrkokodning för booleaner är en funktion av två parametrar:

true väljer den första parametern.
false väljer den andra parametern.

Dessa två definitioner är kända som Church Booleans:

{\begin{aligned}\operatörsnamn {true} &\equiv \lambda a.\lambda ba\\\operatörsnamn {false} &\equiv \lambda a.\lambda bb\end{aligned))

Den här definitionen tillåter predikat (det vill säga funktioner som returnerar en boolean ) att fungera direkt som om villkor:

En funktion som returnerar ett booleskt värde, som sedan appliceras på två parametrar, returnerar antingen den första eller andra parametern:

\operatörsnamn {predikat} \ x\ \operatörsnamn {då-sats} \ \operatörsnamn {annan-sats}

löser sig som en then-sats om x evalueras till sant, och else-sats om x evalueras till falskt.

Eftersom sant och falskt motsvarar valet av den första eller andra parametern för denna funktion, kan denna formalism användas för att implementera logiska standardoperatorer. Observera att det finns två versioner av implementeringen av not-operatorn, beroende på den valda uttrycksupplösningsstrategin .

{\begin{aligned}\operatörsnamn {and} &=\lambda p.\lambda qp\ q\ p\\\operatörsnamn {eller} &=\lambda p.\lambda qp\ p\ q\\\ operatörsnamn {not} _{1}&=\lambda p.\lambda a.\lambda bp\ b\ a\ {\scriptstyle {\text{(Detta är den korrekta implementeringsversionen för applicerande utvärderingsordning.)))}\ \ \operatörsnamn {inte} _{2}&=\lambda pp\ (\lambda a.\lambda bb)\ (\lambda a.\lambda ba)=\lambda pp\operatörsnamn {false} \operatörsnamn {true} \ { \scriptstyle {\text{(Detta är den korrekta implementeringsversionen för den normala utvärderingsordningen.)}}}\\\operatörsnamn {xor} &=\lambda a.\lambda ba\ (\operatörsnamn {inte} \ b )\ b\ \\operatörsnamn {if} &=\lambda p.\lambda a.\lambda bp\ a\ b\end{aligned}}

Några exempel:

{\begin{aligned}\operatörsnamn {and} \operatörsnamn {true} \operatörsnamn {false} &=(\lambda p.\lambda qp\ q\ p)\ \operatörsnamn {true} \ \operatörsnamn {false } =\operatörsnamn {true} \operatörsnamn {false} \operatörsnamn {true} =(\lambda a.\lambda ba)\operatörsnamn {false} \operatörsnamn {true} =\operatörsnamn {false} \\\operatörsnamn {eller} \operatörsnamn {true} \operatörsnamn {false} &=(\lambda p.\lambda qp\ p\ q)\ (\lambda a.\lambda ba)\ (\lambda a.\lambda bb)=(\lambda a .\lambda ba)\ (\lambda a.\lambda ba)\ (\lambda a.\lambda bb)=(\lambda a.\lambda ba)=\operatörsnamn {true} \\\operatörsnamn {inte} _{ 1}\ \operatörsnamn {true} &=(\lambda p.\lambda a.\lambda bp\ b\ a)(\lambda a.\lambda ba)=\lambda a.\lambda b.(\lambda a. \lambda ba)\ b\ a=\lambda a.\lambda b.(\lambda cb)\ a=\lambda a.\lambda bb=\operatörsnamn {falskt} \\\operatörsnamn {inte} _{2}\ \operatörsnamn {true} &=(\lambda pp\ (\lambda a.\lambda bb)(\lambda a.\lambda ba))(\lambda a.\lambda ba)=(\lambda a.\lambda ba) (\lambda a.\lambda bb)(  \lambda a.\lambda ba)=(\lambda b.(\lambda a.\lambda bb))\ (\lambda a.\lambda ba)=\lambda a.\lambda bb=\operatörsnamn {falskt} \end {Justerat}}

Predikat

Predikat är funktioner som returnerar ett booleskt värde.

Det mest grundläggande predikatet är , som returnerar (sant) om dess argument är ett kyrkotal och (falskt) om dess argument är något annat kyrkotal: $\operatörsnamn {IsZero}$ $\operatorname {true}$ $0$ $\operatörsnamn {false}$

\operatörsnamn {IsZero} =\lambda nn\ (\lambda x.\operatörsnamn {false} )\ \operatörsnamn {true}

Detta predikat kontrollerar om dess första argument är mindre än eller lika med dess andra:

\operatörsnamn {LEQ} =\lambda m.\lambda n.\operatörsnamn {IsZero} \ (\operatörsnamn {minus} \ m\ n)

I samband med identiteten

x=y\equiv (x\leq y\land y\leq x)

Jämställdhetskontrollen kan genomföras på följande sätt:

\operatörsnamn {EQ} =\lambda m.\lambda n.\operatörsnamn {och} \ (\operatörsnamn {LEQ} \ m\ n)\ (\operatörsnamn {LEQ} \ n\ m)

Kyrkopar

Se även: nackdelar

Kyrkapar är en kyrkokodad representation av en partyp, det vill säga en tuppel med två värden. Ett par representeras som en funktion som tar en annan funktion som argument. Resultatet av denna funktion är att tillämpa argumentet på de två komponenterna i paret. Definition i lambdakalkyl :

{\begin{aligned}\operatörsnamn {pair} &\equiv \lambda x.\lambda y.\lambda zz\ x\ y\\\operatörsnamn {first} &\equiv \lambda pp\ (\lambda x .\lambda yx)\\\operatörsnamn {andra} &\equiv \lambda pp\ (\lambda x.\lambda yy)\end{aligned}}

Exempel:

{\begin{aligned}&\operatörsnamn {först} \ (\operatörsnamn {par} \ a\ b)\\=&(\lambda pp\ (\lambda x.\lambda yx))\ ((\ lambda x.\lambda y.\lambda zz\ x\ y)\ a\ b)\\=&(\lambda pp\ (\lambda x.\lambda yx))\ (\lambda zz\ a\ b)\ \=&(\lambda zz\ a\ b)\ (\lambda x.\lambda yx)\\=&(\lambda x.\lambda yx)\ a\ b=a\end{aligned}}

Lista kodningar

Listan ( oföränderlig ) består av noder. Följande är de grundläggande funktionerna för listor:

Fungera	Beskrivning
noll	Returnerar en tom lista.
isnil	Kontrollerar om listan är tom.
nackdelar	Lägger till det givna värdet i början av en (eventuellt tom) lista.
huvud	Returnerar det första elementet från listan.
svans	Returnerar hela listan utom det första elementet.

Nedan finns fyra olika listvyer:

Genom skapandet av varje nod i listan med två par.
Genom att skapa varje nod i listan från ett par.
Representerar en lista via en högerassociativ vikfunktion .
Listrepresentation med Scott-kodning.

Representation som två par

En icke-tom lista kan implementeras av ett kyrkapar;

First innehåller det första elementet i listan.
Andra innehåller de återstående elementen ('svansen' på listan).

Det är dock inte möjligt att uttrycka en tom lista på detta sätt, eftersom vi inte har en representation av det tomma värdet (null) definierat. För att representera det och kunna koda tomma listor kan ett par slås in i ett annat par.

Först är null (en tom lista).
Second.First innehåller det första elementet i listan.
Second.Second innehåller svansen på listan.

Med denna idé kan grundläggande listoperationer uttryckas på följande sätt: [1]

uttryck	Beskrivning
$\operatörsnamn {noll} \equiv \operatörsnamn {par} \ \operatörsnamn {true} \ \operatörsnamn {true}$	Det första elementet i paret är sant , vilket betyder att listan är tom.
$\operatörsnamn {isnil} \equiv \operatörsnamn {först}$	Kontrollerar om listan är tom.
$\operatörsnamn {cons} \equiv \lambda h.\lambda t.\operatörsnamn {par} \operatörsnamn {false} \ (\operatörsnamn {par} h\ t)$	skapa en icke-tom listnod och skicka det första elementet (huvudet på listan) h och svansen t till det .
$\operatörsnamn {huvud} \equiv \lambda z.\operatörsnamn {första} \ (\operatörsnamn {andra} z)$	second.first är huvudet på listan.
$\operatörsnamn {svans} \equiv \lambda z.\operatörsnamn {andra} \ (\operatörsnamn {andra} z)$	second.second är svansen på listan.

I en tom lista används aldrig åtkomst till det andra elementet ( Second ), i den mån begreppen huvud och svans på en lista endast gäller icke-tomma listor.

Representation som ett enda par

Alternativt kan listor definieras enligt följande: [2]

{\begin{aligned}\operatörsnamn {cons} &\equiv \operatornamn {par} \\\operatörsnamn {huvud} &\equiv \operatörsnamn {första} \\\operatörsnamn {svans} &\equiv \operatörsnamn { andra} \\\operatörsnamn {noll} &\equiv \operatörsnamn {falskt} \\\operatörsnamn {isnil} &\equiv \lambda ll(\lambda h.\lambda t.\lambda d.\operatörsnamn {false} )\ operatornamn {true} \end{aligned}}

där den sista definitionen är ett specialfall av en mer allmän funktion:

\operatörsnamn {process-list} \equiv \lambda ll(\lambda h.\lambda t.\lambda d.\operatörsnamn {huvud-och-svans-klausul} )\operatörsnamn {noll-klausul}

Att representera en lista via en högerassociativ vikfunktion

Som ett alternativ till kodning med Church-par kan en lista kodas genom att identifiera den med en högerassociativ vikfunktion. Till exempel kan en lista med tre element x, y och z kodas med en högre ordningsfunktion som, när den tillämpas på kombinatorn c och värdet n, returnerar cx(cy(czn)).

{\begin{aligned}\operatörsnamn {noll} &\equiv \lambda c.\lambda nn\\\operatörsnamn {isnil} &\equiv \lambda ll\ (\lambda h.\lambda t.\operatörsnamn { false} )\ \operatörsnamn {true} \\\operatörsnamn {nackdelar} &\equiv \lambda h.\lambda t.\lambda c.\lambda nc\ h\ (t\ c\ n)\\\operatörsnamn {huvud } &\equiv \lambda ll\ (\lambda h.\lambda th)\ \operatörsnamn {falskt} \\\operatörsnamn {svans} &\equiv \lambda l.\lambda c.\lambda nl\ (\lambda h. \lambda t.\lambda gg\ h\ (t\ c))\ (\lambda tn)\ (\lambda h.\lambda tt)\end{aligned}}

Listrepresentation med Scott-kodning

En annan alternativ representation är Scott-kodningsrepresentationen av listor, som använder idén om fortsättning och kan leda till kodförenkling [3] . (se även Mogensen–Scott-kodning ). I detta tillvägagångssätt använder vi det faktum att listor kan bearbetas genom mönstermatchning .

Litteratur

Direktreflekterande metaprogrammering
Kyrkans siffror och booleaner förklaras . Robert University
Teoretiska grunder för praktisk 'Helt funktionell programmering' (kapitel 2 och 5). Allt om kyrklig kodning och andra liknande kodningsmetoder.
Några interaktiva exempel på kyrkans siffror
Lambda Calculus Live Tutorial: Boolean algebra

Se även

lambda kalkyl
System F angående användning och implementering av kyrkans siffror i det för maskinskrivna beräkningar
Mogensen-Scott kodning
Definitionen av ordningstal enligt von Neumann är ett annat sätt att representera naturliga tal. I det här fallet definieras de i termer av set.

Anteckningar

↑ Pierce, Benjamin C. Typer och programmeringsspråk . - MIT Press , 2002. - P. 500. - ISBN 978-0-262-16209-8 .
↑ Tromp, John. 14. Binär Lambda-kalkyl och kombinatorisk logik // Slumpmässighet och komplexitet, från Leibniz till Chaitin (engelska) / Calude, Cristian S.. - World Scientific , 2007. - P. 237-262. — ISBN 978-981-4474-39-9 .
Som PDF: Tromp, John Binary Lambda Calculus and Combinatory Logic (PDF) (14 maj 2014). Hämtad 24 november 2017. Arkiverad från originalet 1 juni 2018. (obestämd)
↑ Jansen, Jan Martin. Programmering i λ-Calculus: Från kyrka till Scott och tillbaka // LNCS : journal. - 2013. - Vol. 8106 . - S. 168-180 . - doi : 10.1007/978-3-642-40355-2_12 .