Církevní kódování

V matematice znamená církevní kódování reprezentaci (nebo proceduru reprezentace) dat a operátorů v proceduře lambda počtu. Nezbytnost postupu je dána tím, že v čistém lambda kalkulu jsou mezi členy pouze proměnné a neexistují žádné konstanty. Aby bylo možné získat objekty, které se chovají stejně jako čísla, používá se církevní kódování. Samotný postup je pojmenován po Alonzovi Churchovi , který vyvinul lambda kalkul a byl průkopníkem této metody kódování dat. Podobně jako čísla lze kódování Church použít také k reprezentaci jiných typů objektů, které se chovají jako konstanty.

Termíny, které jsou obvykle primitivní v jiných zápisech (jako jsou celá čísla, booleovské hodnoty, páry, seznamy a označené svazky), jsou v Churchově kódu reprezentovány pomocí funkcí vyššího řádu . Turing-Churchova teze v jedné ze svých formulací uvádí, že v Churchově kódování může být reprezentován jakýkoli vyčíslitelný operátor (a jeho operandy). V netypovém lambda kalkulu jsou funkce jediným primitivním datovým typem a všechny ostatní entity jsou konstruovány pomocí Church kódování.

Církevní kódování se obecně nepoužívá pro praktickou implementaci primitivních datových typů. Používá se za účelem přesvědčivého prokázání toho, že k provádění výpočtů nejsou vyžadovány jiné primitivní datové typy.

Kostelní čísla

Církevní čísla jsou reprezentace přirozených čísel v církevním kódování. Funkce vyššího řádu , která představuje přirozené číslo n, je funkce, která mapuje jakoukoli funkci na její n-násobné složení . Jednoduše řečeno, „hodnota“ číslice je ekvivalentní tomu, kolikrát funkce zapouzdří svůj argument. $F$

f^{\circ n}=\underbrace {f\circ f\circ \cdots \circ f} _{n{\text{ times))}.\,

Všechna církevní čísla jsou funkce se dvěma parametry. Církevní čísla '0' , '1' , '2' , …, jsou definována v lambda kalkulu takto:

$0\ f\ x$ znamená „nepoužít funkci vůbec “, znamená „použít funkci jednou“ atd.: $F$ $X$ $1\ f\ x$

Číslo	Definice číslic	lambda výraz
0	$0\ f\ x=x$	$0=\lambda f.\lambda xx$
jeden	$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$

Churchova číslice 3 představuje proces aplikace libovolné použité funkce f třikrát. Tato funkce je postupně aplikována nejprve na parametr, který jí byl předán, a poté na výsledek získaný v důsledku předchozí aplikace.

Výpočty s církevními číslicemi

Aritmetické operace s čísly mohou být reprezentovány funkcemi na církevních číslicích. Tyto funkce mohou být definovány v lambda kalkulu nebo implementovány ve většině funkčních programovacích jazyků (viz Převod lambda výrazů na funkce ).

Kódování Booleans

Church booleans jsou výsledkem kódování Church aplikovaného na reprezentaci booleovských hodnot true a false. Některé programovací jazyky je používají jako implementační model pro booleovskou aritmetiku. Příklady takových jazyků jsou Smalltalk a Pico .

Booleovskou logiku lze považovat za volbu. Kódování církve pro booleovské hodnoty je funkcí dvou parametrů:

true vybere první parametr.
false vybere druhý parametr.

Tyto dvě definice jsou známé jako Church Booleans:

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

Tato definice umožňuje predikátům (tj. funkcím, které vracejí boolean ) pracovat přímo jako podmínky:

Funkce, která vrací booleovskou hodnotu, která je poté aplikována na dva parametry, vrací buď první nebo druhý parametr:

\operatorname {predikát} \ x\ \operatorname {pak-klauzule} \ \operatorname {jinak-klauzule}

vyhodnotí se jako klauzule potom, pokud se x vyhodnotí jako pravda, a klauzule else, pokud se x vyhodnotí jako nepravda.

Protože true a false odpovídají volbě prvního nebo druhého parametru této funkce, lze tento formalismus použít k implementaci standardních logických operátorů. Všimněte si, že existují dvě verze implementace operátoru not, v závislosti na zvolené strategii rozlišení výrazu .

{\begin{aligned}\operatorname {and} &=\lambda p.\lambda qp\ q\ p\\\operatorname {or} &=\lambda p.\lambda qp\ p\ q\\\ operatorname {not} _{1}&=\lambda p.\lambda a.\lambda bp\ b\ a\ {\scriptstyle {\text{(Toto je správná verze implementace pro aplikační pořadí hodnocení.)))}\ \ \operatorname {ne} _{2}&=\lambda pp\ (\lambda a.\lambda bb)\ (\lambda a.\lambda ba)=\lambda pp\operatorname {false} \operatorname {true} \ { \scriptstyle {\text{(Toto je správná verze implementace pro normální pořadí hodnocení.)}}}\\\jméno operátora {xor} &=\lambda a.\lambda ba\ (\jméno operátora {není} \ b )\ b\ \\název operátora {if} &=\lambda p.\lambda a.\lambda bp\ a\ b\end{zarovnáno}}

Několik příkladů:

{\begin{aligned}\operatorname {and} \operatorname {true} \operatorname {false} &=(\lambda p.\lambda qp\ q\ p)\ \operatorname {true} \ \operatorname {false } =\operatorname {pravda} \operatorname {false} \operatorname {true} =(\lambda a.\lambda ba)\operatorname {false} \operatorname {true} =\operatorname {false} \\\operatorname {nebo} \operatorname {pravda} \operatorname {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)=\jméno operátora {pravda} \\\jméno operátora {ne} _{ 1}\ \operatorname {pravda} &=(\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=\operatorname {false} \\\operatorname {ne} _{2}\ \operatorname {pravda} &=(\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=\jméno operátora {false} \end {zarovnaný}}

Predikáty

Predikáty jsou funkce, které vracejí booleovskou hodnotu.

Nejzákladnějším predikátem je , který vrací (true), pokud je jeho argumentem církevní číslo , a (false), pokud je jeho argumentem jakákoli jiná církevní číslovka: $\operatorname {IsZero}$ $\operatorname {true}$ $0$ $\operatorname {false}$

\operatorname {IsZero} =\lambda nn\ (\lambda x.\operatorname {false} )\ \operatorname {true}

Tento predikát kontroluje, zda je jeho první argument menší nebo roven druhému:

\operatorname {LEQ} =\lambda m.\lambda n.\operatorname {IsZero} \ (\operatorname {minus} \ m\ n)

V souvislosti s identitou

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

Kontrola rovnosti může být provedena následujícím způsobem:

\operatorname {EQ} =\lambda m.\lambda n.\operatorname {and} \ (\operatorname {LEQ} \ m\ n)\ (\operatorname {LEQ} \ n\ m)

Církevní páry

Viz také: nevýhody

Církevní páry jsou církevně kódovanou reprezentací párového typu, tedy n-tice dvou hodnot. Pár je reprezentován jako funkce, která má jinou funkci jako argument. Výsledkem této funkce je použití argumentu na dvě složky dvojice. Definice v lambda kalkulu :

{\begin{aligned}\operatorname {pair} &\equiv \lambda x.\lambda y.\lambda zz\ x\ y\\\operatorname {first} &\equiv \lambda pp\ (\lambda x .\lambda yx)\\\název operátora {druhý} &\equiv \lambda pp\ (\lambda x.\lambda yy)\end{zarovnáno}}

Příklad:

{\begin{aligned}&\operatorname {first} \ (\operatorname {pair} \ 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{zarovnáno}}

Seznam kódování

( neměnný ) seznam se skládá z uzlů. Níže jsou uvedeny základní operace se seznamy:

Funkce	Popis
nula	Vrátí prázdný seznam.
isnil	Zkontroluje, zda je seznam prázdný.
nevýhody	Připojí danou hodnotu na začátek (případně prázdného) seznamu.
hlava	Vrátí první prvek ze seznamu.
ocas	Vrátí celý seznam kromě prvního prvku.

Níže jsou čtyři různá zobrazení seznamu:

Prostřednictvím vytvoření každého uzlu seznamu dvou párů.
Prostřednictvím vytvoření každého uzlu seznamu z jednoho páru.
Reprezentace seznamu pomocí funkce pravého skládání .
Reprezentace seznamu pomocí Scottova kódování.

Reprezentace jako dva páry

Neprázdný seznam může být implementován dvojicí Church;

První obsahuje první prvek seznamu.
Druhý obsahuje zbývající prvky ('konec' seznamu).

Tímto způsobem však není možné vyjádřit prázdný seznam, protože nemáme definovanou reprezentaci prázdné hodnoty (null). Pro reprezentaci a možnost kódování prázdných seznamů lze pár zabalit do jiného páru.

První je null (prázdný seznam).
Second.First obsahuje první prvek seznamu.
Second.Second obsahuje konec seznamu.

Pomocí této myšlenky lze základní operace se seznamy vyjádřit následovně: [1]

výraz	Popis
$\operatorname {nil} \equiv \operatorname {pair} \ \operatorname {true} \ \operatorname {true}$	První prvek z dvojice je true , což znamená, že seznam je prázdný.
$\operatorname {isnil} \equiv \operatorname {first}$	Kontrola, zda je seznam prázdný.
$\operatorname {cons} \equiv \lambda h.\lambda t.\operatorname {pair} \operatorname {false} \ (\operatorname {pair} h\ t)$	vytvořte neprázdný uzel seznamu a předejte mu první prvek (hlavu seznamu) h a konec t .
$\operatorname {head} \equiv \lambda z.\operatorname {first} \ (\operatorname {second} z)$	druhý . první je hlava seznamu.
$\operatorname {tail} \equiv \lambda z.\operatorname {second} \ (\operatorname {second} z)$	druhý.druhý je konec seznamu.

V prázdném seznamu se přístup k druhému prvku ( Second ) nikdy nepoužívá, pokud se koncepty záhlaví a konce seznamu vztahují pouze na neprázdné seznamy.

Reprezentace jako jeden pár

Alternativně lze seznamy definovat následovně: [2]

{\begin{aligned}\operatorname {cons} &\equiv \operatorname {pair} \\\operatorname {head} &\equiv \operatorname {first} \\\operatorname {tail} &\equiv \operatorname { druhý} \\\jméno operátora {nil} &\equiv \název operátora {false} \\\jméno operátora {isnil} &\equiv \lambda ll(\lambda h.\lambda t.\lambda d.\jméno operátora {false} )\ operatorname {true} \end{aligned}}

kde poslední definice je speciální případ obecnější funkce:

\operatorname {process-list} \equiv \lambda ll(\lambda h.\lambda t.\lambda d.\operatorname {head-and-tail-clause} )\operatorname {nul-clause}

Reprezentace seznamu pomocí funkce pravého skládání

Alternativně ke kódování pomocí Church párů lze seznam zakódovat jeho identifikací pomocí funkce pravého asociativního skládání. Například seznam tří prvků x, y a z lze zakódovat funkcí vyššího řádu, která po aplikaci na kombinátor c a hodnotu n vrátí cx(cy(czn)).

{\begin{aligned}\operatorname {nil} &\equiv \lambda c.\lambda nn\\\operatorname {isnil} &\equiv \lambda ll\ (\lambda h.\lambda t.\operatorname { false} )\ \operatorname {true} \\\operatorname {cons} &\equiv \lambda h.\lambda t.\lambda c.\lambda nc\ h\ (t\ c\ n)\\\operatorname {head } &\equiv \lambda ll\ (\lambda h.\lambda th)\ \operatorname {false} \\\operatorname {tail} &\equiv \lambda l.\lambda c.\lambda nl\ (\lambda h. \lambda t.\lambda gg\ h\ (t\ c))\ (\lambda tn)\ (\lambda h.\lambda tt)\end{aligned}}

Reprezentace seznamu pomocí Scottova kódování

Další alternativní reprezentací je Scottova kódová reprezentace seznamů, která využívá myšlenku pokračování a může vést ke zjednodušení kódu [3] . (viz také kódování Mogensen–Scott ). V tomto přístupu využíváme skutečnosti, že seznamy lze zpracovat pomocí vzorového párování .

Literatura

Přímo reflektivní metaprogramování
Církevní číslice a booleovské vysvětlování . Univerzita Roberta
Teoretické základy pro praktické „zcela funkční programování“ (kapitoly 2 a 5). Vše o církevním kódování a dalších podobných metodách kódování.
Některé interaktivní příklady církevních číslic
Živý výukový program Lambda Calculus: Booleovská algebra

Viz také

lambda kalkul
Systém F ohledně použití a implementace církevních číslic v něm pro typizované výpočty
Mogensen-Scott kódování
Definice ordinálních čísel podle von Neumanna je dalším způsobem reprezentace přirozených čísel. V tomto případě jsou definovány jako množiny.

Poznámky

↑ Pierce, Benjamin C. Typy a programovací jazyky . - MIT Press , 2002. - S. 500. - ISBN 978-0-262-16209-8 .
↑ Tromp, John. 14. Binární lambda kalkul a kombinační logika // Náhodnost a složitost, od Leibnize k Chaitinu (anglicky) / Calude, Cristian S.. - World Scientific , 2007. - S. 237-262. — ISBN 978-981-4474-39-9 .
Jako PDF: Tromp, John Binary Lambda Calculus and Combinatory Logic (PDF) (14. května 2014). Získáno 24. listopadu 2017. Archivováno z originálu 1. června 2018. (neurčitý)
↑ Jansen, Jan Martin. Programování v λ-Calculus: From Church to Scott and Back // LNCS : deník. - 2013. - Sv. 8106 . - S. 168-180 . - doi : 10.1007/978-3-642-40355-2_12 .