Niech wyrażenie - Let expression

W informatyce wyrażenie „let” wiąże definicję funkcji z ograniczonym zakresem .

Wyrażenie „let” może być również zdefiniowane w matematyce, gdzie wiąże warunek logiczny z ograniczonym zakresem.

Wyrażenie „let” może być traktowane jako abstrakcja lambda zastosowana do wartości. W matematyce wyrażenie let może być również traktowane jako koniunkcja wyrażeń w egzystencjalnym kwantyfikatorze, który ogranicza zakres zmiennej.

Wyrażenie let jest obecne w wielu językach funkcjonalnych, aby umożliwić lokalną definicję wyrażenia do użycia przy definiowaniu innego wyrażenia. Wyrażenie let występuje w niektórych językach funkcjonalnych w dwóch formach; let lub „niech rec”. Let rec jest rozszerzeniem prostego wyrażenia let , które używa kombinatora stałoprzecinkowego do implementacji rekursji .

Historia

Dana Scott „s język LCF był etap w ewolucji rachunku lambda do współczesnych języków funkcjonalnych. Język ten wprowadził wyrażenie let, które od tego czasu pojawiało się w większości języków funkcjonalnych.

Języki Scheme , ML , a ostatnio Haskell odziedziczyły wyrażenia let z LCF.

Języki imperatywne stanowe, takie jak ALGOL i Pascal, zasadniczo implementują wyrażenie let, aby zaimplementować ograniczony zakres funkcji, w strukturach blokowych.

Ściśle związane z „ gdzie ” klauzula, wraz z rekurencyjnego wariant „ gdzie rec ”, pojawiła się już w Peter Landin „s Mechaniczne oceny wyrażeń .

Opis

Wyrażenie „let” definiuje funkcję lub wartość do użycia w innym wyrażeniu. Oprócz tego, że jest konstrukcją używaną w wielu funkcjonalnych językach programowania, jest to konstrukcja języka naturalnego często używana w tekstach matematycznych. Jest to alternatywna konstrukcja składniowa dla klauzuli where.

Niech wyrażenie	Gdzie klauzula
Pozwolić ${\displaystyle a=3}$ oraz ${\displaystyle b=4}$ w ${\ Displaystyle {\ sqrt {a ^ {2} + b ^ {2}}}}$	${\ Displaystyle {\ sqrt {a ^ {2} + b ^ {2}}}}$ gdzie ${\displaystyle a=3}$ oraz ${\displaystyle b=4}$

W obu przypadkach cała konstrukcja jest wyrażeniem o wartości 5. Podobnie jak w przypadku if-then-else typ zwracany przez wyrażenie niekoniecznie musi być typu Boolean.

Wyrażenie let występuje w 4 głównych formach,

Formularz	I	Rekurencyjne	Definicja / Ograniczenie	Opis
Prosty	Nie	Nie	Definicja	Prosta definicja funkcji nierekurencyjnej.
Rekurencyjne	Nie	tak	Definicja	Definicja funkcji rekurencyjnej (implementowana za pomocą kombinatora Y ).
Wzajemne	tak	tak	Definicja	Wzajemnie rekurencyjna definicja funkcji.
Matematyczny	tak	tak	Ograniczenie	Matematyczna definicja wspierająca ogólny warunek boolowski.

W językach funkcyjnych wyrażenie let definiuje funkcje, które mogą być wywołane w wyrażeniu. Zakres nazwy funkcji jest ograniczony do struktury wyrażenia let.

W matematyce wyrażenie let definiuje warunek, który jest ograniczeniem wyrażenia. Składnia może również wspierać deklarację egzystencjalnie skwantyfikowanych zmiennych lokalnych względem wyrażenia let.

Terminologia, składnia i semantyka różnią się w zależności od języka. W Scheme , let jest używany dla formy prostej, a let rec dla formy rekurencyjnej. W ML let zaznacza tylko początek bloku deklaracji z zabawą oznaczającą początek definicji funkcji. W Haskell, niech będą wzajemnie rekurencyjne, z kompilatorem domyślającym się, co jest potrzebne.

Definicja

N poboru reprezentuje funkcję bez nazwy. To jest źródłem niespójności definicji abstrakcji lambda. Jednak abstrakcje lambda mogą być tworzone w celu reprezentowania funkcji o nazwie. W tej formie niezgodność jest usuwana. Termin lambda,

${\ Displaystyle (\ lambda fz) \ (\ lambda xy)}$

jest równoznaczne z określeniem funkcji przez w wyrażeniu , które można zapisać jako wyrażenie let ; ${\displaystyle f}$${\displaystyle f\x=y}$${\displaystyle z}$

${\ Displaystyle \ operatorname {niech} f \ x = y \ operatorname {w} z}$

Wyrażenie let jest zrozumiałe jako wyrażenie w języku naturalnym. Wyrażenie let reprezentuje zastąpienie zmiennej wartością. Reguła substytucji opisuje implikacje równości jako substytucji.

Niech definicja w matematyce

W matematyce let ekspresja jest opisany jako koniunkcji wyrażeń. W językach funkcjonalnych wyrażenie let służy również do ograniczania zakresu. W matematyce zakres jest opisywany przez kwantyfikatory. Wyrażenie let jest koniunkcją w egzystencjalnym kwantyfikatorze.

${\displaystyle (\istnieje xE\land F)\iff \operator {niech} x:e\operator {w} F}$

gdzie E i F są typu Boolean.

Let ekspresja pozwala na zmianę do zastosowania innemu wyrażeniu. To podstawienie można zastosować w ograniczonym zakresie do wyrażenia podrzędnego. Naturalnym zastosowaniem wyrażenia let jest zastosowanie do ograniczonego zakresu (tzw. lambda dropping ). Zasady te określają, w jaki sposób można ograniczyć zakres;

${\ Displaystyle {\ zacząć {przypadki} x \ nie \ w \ operatorname {FV} (E) \ land x \ w \ operatorname {FV} (F) \ implikuje \ operatorname {niech} x: G \ operatorname {in} E\ F=E\ (\nazwa operatora {niech} x:G\nazwa operatora {w} F)\\x\in \nazwa operatora {FV} (E)\land x\not \in \nazwa operatora {FV} (F) \implies \operatorname {let} x:G\operatorname {in} E\ F=(\operatorname {let} x:G\operatorname {in} E)\ F\\x\not \in \operatorname {FV} ( E)\land x\not \in \operatorname {FV} (F)\implikuje \operatorname {let} x:G\operatorname {in} E\ F=E\ F\end{cases}}}$

gdzie F nie jest typu Boolean . Z tej definicji można wyprowadzić następującą standardową definicję wyrażenia let, używaną w języku funkcjonalnym.

${\ Displaystyle x \ nie \ w \ operatorname {FV} (y) \ implikuje (\ operatorname {niech} x: x = y \ operatorname {w} z) = z [x: = y] = (\ lambda xz) \ y}$

Dla uproszczenia znacznik określający zmienną egzystencjalną , zostanie pominięty w wyrażeniu, jeśli jest on jasny z kontekstu. ${\displaystyle x:}$

${\ Displaystyle x \ nie \ w \ nazwa operatora {FV} (y) \ implikuje (\ nazwa operatora {niech} x = r \ nazwa operatora {w} z) = z [x: = y] = (\ lambda xz) \ r }$

Pochodzenie

Aby uzyskać ten wynik, najpierw załóżmy,

${\ Displaystyle x \ nie \ w \ operatorname {FV} (L)}$

następnie

${\ Displaystyle {\ zacząć {wyrównany} L \ (\ nazwa operatora {niech} x: x = y \ nazwa operatora {w} z) i \ iff (\ nazwa operatora {niech} x: x = y \ nazwa operatora {w} L \ z)\\&\iff x=y\land L\ z\end{wyrównany}}}$

Stosując zasadę substytucji,

${\ Displaystyle {\ zacząć {wyrównany} i \ iff x = y \ ziemia (l \ z) [x: = y] \ \ i \ iff x = y \ ziemia (l [x: = y] \ z [x :=y])\\&\iff x=y\land L\ z[x:=y]\\&\implikuje L\ z[x:=y]\end{wyrównany}}}$

więc dla wszystkich L ,

${\ Displaystyle L \ operatorname {niech} x: x = y \ operatorname {w} z \ implikuje L \ z [x: = y]}$

Niech gdzie K jest nową zmienną. następnie, ${\ Displaystyle L\ X = (X = K)}$

${\ Displaystyle (\ nazwa operatora {niech} x: x = y \ nazwa operatora {w} z) = K \ implikuje z [x: = y] = K}$

Więc,

${\displaystyle \operatorname {niech} x:x=y\operatorname {w} z=z[x:=y]}$

Ale z matematycznej interpretacji redukcji beta,

${\ Displaystyle (\ lambda xz) \ y = z [x: = y]}$

Tutaj, jeśli y jest funkcją zmiennej x, to nie jest to samo x jak w z. Można zastosować zmianę nazwy alfa. Więc musimy mieć,

${\ Displaystyle x \ nie \ w \ operatorname {FV} (y)}$

więc,

${\ Displaystyle x \ nie \ w \ operatorname {FV} (y) \ implikuje \ operatorname {niech} x: x = y \ operatorname {in} z = (\ lambda xz) \ y}$

Wynik ten jest reprezentowany w języku funkcjonalnym w formie skróconej, gdzie znaczenie jest jednoznaczne;

${\ Displaystyle x \ nie \ w \ nazwa operatora {FV} (y) \ implikuje (\ nazwa operatora {niech} x = r \ nazwa operatora {w} z) = z [x: = y] = (\ lambda xz) \ r }$

Tutaj zmienna x jest domyślnie uznawana zarówno za część równania definiującego x, jak i zmienną w kwantyfikatorze egzystencjalnym.

Brak podnoszenia z Boolean

Sprzeczność powstaje, jeśli E jest zdefiniowane przez . W tym przypadku, ${\displaystyle E=\neg}$

${\ Displaystyle x \ nie \ w \ operatorname {FV} (E) \ land x \ w \ operatorname {FV} (F) \ implikuje \ operatorname {niech} x: G \ operatorname {in} E \ F = E \ (\nazwa operatora {niech} x:G\nazwa operatora {w} F)}$

staje się,

${\ Displaystyle \ nazwa operatora {niech} x: G \ nazwa operatora {w} \ neg F = \ neg \ (\ nazwa operatora {niech} x: G \ nazwa operatora {w} F)}$

i za pomocą,

${\displaystyle (\istnieje xE\land F)\iff \operator {niech} x:e\operator {w} F}$

${\ Displaystyle (\ istnieje xG \ ziemia \ neg F) = \ neg \ (\ istnieje xG \ ziemia F)}$

${\ Displaystyle = (\ istnieje x \ neg G \ lor \ neg F)}$

To jest fałszywe, jeśli G jest fałszywe. Aby uniknąć tej sprzeczności, F nie może być typu Boolean. Dla Boolean F poprawne stwierdzenie reguły odrzucania używa implikacji zamiast równości,

${\ Displaystyle x \ nie \ w \ operatorname {FV} (E) \ land x \ w \ operatorname {FV} (F) \ implikuje (\ operatorname {niech} x: G \ operatorname {in} E \ F \ to E\ (\nazwa operatora {niech} x:G\nazwa operatora {w} F))}$

Może wydawać się dziwne, że dla Boolean obowiązuje inna reguła niż dla innych typów. Powodem tego jest to, że zasada

${\displaystyle (\istnieje xE\land F)\iff \operator {niech} x:e\operator {w} F}$

ma zastosowanie tylko wtedy, gdy F jest wartością logiczną. Połączenie tych dwóch zasad tworzy sprzeczność, więc tam, gdzie jedna zasada obowiązuje, druga nie.

Łączenie wyrażeń let

Wyrażenia niech mogą być definiowane z wieloma zmiennymi,

${\ Displaystyle (\istnieje v\cdots \istnieje w\istnieje xE \land F) \iff \nazwa operatora {niech} v \ldots, w, x: E \ nazwa operatora {w} F}$

wtedy można go wyprowadzić,

${\ Displaystyle x \ nie \ w FV (E) \ implikuje (\ istnieje v \ cdots \ istnieje w \ istnieje xE \ F ziemia) \ iff (\ istnieje v \ cdots \ istnieje w (E \ ziemia \ istnieje XF)) }$

więc,

${\ Displaystyle x \ nie \ w FV (E) \ implikuje (\ nazwa operatora {niech} v \ ldots, w, x: E \ ziemia F \ nazwa operatora {w} L \ równoważny \ nazwa operatora {niech} v \ ldots ,w:E\nazwa operatora {w} \nazwa operatora {niech} x:F\nazwa operatora {w} L)}$

Prawa dotyczące rachunku lambda i wyrażeń let

Redukcja Eta daje regułę opisującą abstrakcje lambda. Reguła ta wraz z dwoma wyprowadzonymi powyżej prawami określa związek między rachunkiem lambda a wyrażeniami let.

Nazwa	Prawo
Równoważność redukcji eta	${\displaystyle f\ x=y\equiv f=\lambda xy}$
Równoważność let-lambda	${\ Displaystyle f \ notin FV (E) \ implikuje (\ nazwa operatora {niech} f: f = E \ nazwa operatora {w} L \ równoważny (\ lambda fL) \ e)}$(gdzie jest nazwą zmiennej.) ${\displaystyle f}$
Niech kombinacja	${\ Displaystyle x \ notin FV (E) \ implikuje (\ nazwa operatora {niech} v, \ kropki, w, x: E \ ziemia F \ nazwa operatora {w} L \ równoważne \ nazwa operatora {niech} v, \ kropki, w :E\nazwa operatora {w} \nazwa operatora {niech} x:F\nazwa operatora {w} L)}$

Niech definicja zdefiniowana z rachunku lambda

Aby uniknąć potencjalnych problemów związanych z definicją matematyczną , Dana Scott pierwotnie zdefiniowała wyrażenie let z rachunku lambda. Można to uznać za oddolną lub konstruktywną definicję wyrażenia let , w przeciwieństwie do odgórnej lub aksjomatycznej definicji matematycznej.

Proste, nierekurencyjne wyrażenie let zostało zdefiniowane jako cukier składniowy dla abstrakcji lambda zastosowanej do terminu. W tej definicji

${\ Displaystyle (\ nazwa operatora {niech} _ {s} x = r \ nazwa operatora {w} z) \ równoważnik (\ lambda xz) \ r}$

Definicja prostego wyrażenia let została następnie rozszerzona, aby umożliwić rekursję przy użyciu kombinatora stałoprzecinkowego .

Kombinator stałopunktowy

Operator paradoksalny może być reprezentowany przez wyrażenie

${\ Displaystyle \ lambda f. \ nazwa operatora {niech} x = f \ x \ nazwa operatora {w} x}$

Ta reprezentacja może zostać przekształcona w termin lambda. Abstrakcja lambda nie obsługuje odwołań do nazwy zmiennej w zastosowanym wyrażeniu, więc x musi być przekazany jako parametr do x .

${\ Displaystyle \ lambda f. \ operator {niech} x \ x = f \ (x \ x) \ operatorname {w} x \ x}$

Stosując zasadę redukcji eta,

${\displaystyle f\ x=y\equiv f=\lambda xy}$

daje,

${\ Displaystyle \ Lambda f. \ Operator {niech} x = \ Lambda xf \ (x \ x) \ Operator {w} x \ x}$

Wyrażenie let może być wyrażone jako abstrakcja lambda przy użyciu,

${\ Displaystyle n \ nie \ w FV (E) \ do (\ Operator {niech} n = E \ Operator {w} L \ równoważny (\ Lambda nL) \ E)}$

daje,

${\ Displaystyle \ lambda f. (\ lambda xx \ x) \ (\ lambda xf \ (x\ x))}$

Jest to prawdopodobnie najprostsza implementacja kombinatora stałoprzecinkowego w rachunku lambda. Jednak jedna redukcja beta daje bardziej symetryczną formę kombinatora Y Curry'ego.

${\ Displaystyle \ lambda f. (\ lambda xf \ (x\ x))\ (\ lambda xf \ (x\ x))}$

Rekurencyjne wyrażenie niech

Rekurencyjne wyrażenie let o nazwie „let rec” jest definiowane za pomocą kombinatora Y dla rekurencyjnych wyrażeń let.

${\ Displaystyle (\ nazwa operatora {niech\ rec} x = r \ nazwa operatora {w} z) \ równoważny (\ lambda xz) \ (y \ (\ lambda xy))}$

Wzajemnie rekurencyjne wyrażenie niech

To podejście jest następnie uogólniane w celu wspierania wzajemnej rekurencji. Wzajemnie rekurencyjne wyrażenie let może być skomponowane przez przeorganizowanie wyrażenia w celu usunięcia dowolnych warunków i . Osiąga się to poprzez zastąpienie wielu definicji funkcji jedną definicją funkcji, która ustawia listę zmiennych równą liście wyrażeń. Wersja kombinatora Y, zwana wielowariantowym kombinatorem stałopunktowym Y*, jest następnie używana do obliczania punktu stałego wszystkich funkcji w tym samym czasie. Rezultatem jest wzajemnie rekurencyjna implementacja wyrażenia let .

Wiele wartości

Wyrażenie let może służyć do reprezentowania wartości, która jest członkiem zbioru,

${\ Displaystyle \ nazwa operatora {niech} x \ w X \ nazwa operatora {w} x}$

W ramach zastosowania funkcji, jednego wyrażenia do drugiego,

${\ Displaystyle {\ zacząć {wyrównany} i (\ nazwa operatora {niech} x \ w X \ nazwa operatora {w} x) \ (\ nazwa operatora {niech} r \ w Y \ nazwa operatora {w} r) \ \ & = \ operator {let} x\in X\land y\in Y\operator {in} x\ y\\&=\operator {let} (x,y)\in X\times Y\operator {in} x\ y \end{wyrównany}}}$

Ale inna zasada dotyczy zastosowania wyrażenia let do samego siebie.

${\ Displaystyle {\ zacząć {wyrównany} i (\ nazwa operatora {niech} x \ w X \ nazwa operatora {w} x) \ (\ nazwa operatora {niech} x \ w X \ nazwa operatora {w} x) \ \ & = \ operatorname {let} x\in X\operatorname {in} x\ x\end{aligned}}}$

Nie ma prostej zasady łączenia wartości. Wymagana jest ogólna forma wyrażenia reprezentująca zmienną, której wartość należy do zbioru wartości. Wyrażenie powinno być oparte na zmiennej i zestawie.

Aplikacja funkcji zastosowana do tej formy powinna dawać inne wyrażenie w tej samej formie. W ten sposób każde wyrażenie dotyczące funkcji wielu wartości może być traktowane tak, jakby miało jedną wartość.

Nie wystarczy, aby formularz reprezentował tylko zbiór wartości. Każda wartość musi mieć warunek określający, kiedy wyrażenie przyjmuje wartość. Powstała konstrukcja to zestaw par warunków i wartości, zwany „zestawem wartości”. Zobacz zawężanie algebraicznych zbiorów wartości .

Zasady konwersji między rachunkiem lambda a wyrażeniami let

Zostaną podane meta-funkcje opisujące konwersję między wyrażeniami lambda i let . Meta-funkcja to funkcja, która przyjmuje program jako parametr. Program to dane dla meta-programu. Program i metaprogram znajdują się na różnych metapoziomach.

Następujące konwencje będą używane do odróżnienia programu od metaprogramu,

• Nawiasy kwadratowe [] będą używane do reprezentowania aplikacji funkcji w programie meta.
• W metaprogramie dla zmiennych będą używane wielkie litery. Małe litery reprezentują zmienne w programie.
• ${\displaystyle \equiv}$ będzie używany dla równych w programie meta.

Dla uproszczenia zastosowana zostanie pierwsza reguła podana, że ​​dopasowania. Reguły zakładają również, że wyrażenia lambda zostały wstępnie przetworzone, tak aby każda abstrakcja lambda miała unikatową nazwę.

Używany jest również operator substytucji. Wyrażenie oznacza zastąpienie każdego wystąpienia G w L przez S i zwrócenie wyrażenia. Użyta definicja została rozszerzona, aby objąć podstawienie wyrażeń, z definicji podanej na stronie rachunku Lambda . Dopasowywanie wyrażeń powinno porównywać wyrażenia pod kątem równoważności alfa (zmiany nazw zmiennych). ${\ Displaystyle L [G: = S]}$

Konwersja z wyrażenia lambda do wyrażenia let

Poniższe reguły opisują sposób konwersji z wyrażenia lambda na wyrażenie let bez zmiany struktury.

1. ${\ Displaystyle \ Operatorname {de-lambda} [V] \ Equiv V}$
2. ${\ Displaystyle \ operatorname {de-lambda} [M\ N] \ równoważne \ operatorname {de-lambda} [M] \ \ operatorname {de-lambda} [N]}$
3. ${\ Displaystyle \ Operatorname {de-lambda} [F = \ Lambda PE] \ Equiv \ Operatorname {De-lambda} [F \ P = E]}$
4. ${\ Displaystyle \ operatorname {de-lambda} [E = F] \ równoważne \ operatorname {de-lambda} [E] = \ operatorname {de-lambda} [F]}$
5. ${\displaystyle \operator {de-lambda} [(\lambda FE)L]\equiv \operator {niech łączyć} [\operator {niech} F:\operator {de-lambda} [F=L]\operator { w} E]}$
6. ${\ Displaystyle V \ nie \ w \ operatorname {FV} [\ lambda FE] \ do \ operatorname {de-lambda} [\ lambda FE] \ equiv \ operatorname {niech łączyć} [\ operator {niech} V: \ nazwa operatora {de-lambda} [V\ F=E]\nazwa operatora {w} V]}$
7. ${\ Displaystyle V \ neq W \ do \ nazwa operatora {niech łączyć} [\ nazwa operatora {niech} V: E \ nazwa operatora {w} \ nazwa operatora {niech} W: F \ nazwa operatora {w} G] \ równoważnik \ nazwa operatora { let} V,W:E\land F\nazwa operatora {in} G}$
8. ${\displaystyle \operator {niech łączyć} [\operator {niech} V:E\operator {w} F] \equiv \operator {niech} V:E\operator {w} F}$

Reguła 6 tworzy unikalną zmienną V jako nazwę funkcji.

Przykład

Na przykład kombinator Y ,

${\ Displaystyle \ lambda f. (\ lambda xf \ (x\ x))\ (\ lambda xf \ (x\ x))}$

jest konwertowany na,

${\displaystyle \operatorname {niech} p:p\f=\operator {niech} x:x\q=f\ (q\q)\operator {w} f\ (x\ x)\operator {w} p }$

Reguła	Wyrażenie lambda
6	${\ Displaystyle \ Operatorname {de-lambda} [\ lambda f. (\ lambda xf \ (x\ x)) \ (\ lambda xf \ (x\ x))]}$ ${\ Displaystyle V \ nie \ w \ operatorname {FV} [\ lambda FE] \ do \ operatorname {de-lambda} [\ lambda FE]}$ ${\ Displaystyle V = p, F = f, E = (\ lambda xf\ (x\ x))\ (\ lambda xf\ (x\ x))}$ ${\displaystyle \operator {niech łączyć} [\operator {niech} V:\operator {de-lambda} [V\ F=E]\operator {w} V]}$
4	${\ Displaystyle \ operatorname {niech łączyć} [\ operatorname {niech} p: \ operatorname {de-lambda} [p\ f = (\ lambda xf\ (x\ x))\ (\ lambda xf\ (x\ x))]\nazwa operatora {in} p]}$ ${\ Displaystyle \ Operatorname {de-lambda} [p\ f = (\ lambda xf\ (x\ x))\ (\ lambda xf\ (x\ x))]}$ ${\ Displaystyle \ Operatorname {de-lambda} [E = F]}$ ${\ Displaystyle E = p\ f, F = (\ lambda xf\ (x\ x))\ (\ lambda xf\ (x\ x))}$ ${\ Displaystyle \ operatorname {de-lambda} [E] = \ operatorname {de-lambda} [F]}$ ${\ Displaystyle \ operatorname {de-lambda} [p\ f] = \ operatorname {de-lambda} [(\ lambda xf \ (x\ x)) \ (\ lambda xf \ (x\ x))]}$ ${\displaystyle \operator {niech łączyć} [\operator {niech} p:\operator {de-lambda} [p\ f] = \ operatorname {de-lambda} [(\ lambda xf\ (x\ x)) \ (\lambda xf\ (x\ x))]\nazwa operatora {w} p]}$
5	${\displaystyle \operator {niech łączyć} [\operator {niech} p:\operator {de-lambda} [p\ f] = \ operatorname {de-lambda} [(\ lambda xf\ (x\ x)) \ (\lambda xf\ (x\ x))]\nazwa operatora {w} p]}$ ${\ Displaystyle \ Operatorname {de-lambda} [(\ lambda xf \ (x\ x)) \ (\ lambda xf \ (x\ x))]}$ ${\ Displaystyle \ Operatorname {de-lambda} [(\ Lambda FE) L]}$ ${\ Displaystyle F = x, E = f\ (x\ x), L = (\ lambda xf\ (x\ x))}$ ${\displaystyle \operator {niech łączyć} [\operator {niech} F:\operator {de-lambda} [F=L]\operator {w} E]}$ ${\ Displaystyle \ nazwa operatora {niech łączyć} [\ nazwa operatora {niech} x: \ nazwa operatora {de-lambda} [x = \ lambda xf \ (x \ x)] \ operator {w} f \ (x\ x) ]}$
3	${\displaystyle \operator {niech łączyć} [\operator {niech łączyć} p:\operator {de-lambda} [p\f]=\operator {niech łączyć} [\operator {niech} x:\operator {de -lambda} [x=\lambda xf\ (x\ x)]\nazwa operatora {w} f\ (x\ x)]\nazwa operatora {w} p]}$ ${\ Displaystyle \ operatorname {de-lambda} [x = \ lambda xf \ (x \ x)]}$ ${\ Displaystyle \ Operatorname {de-lambda} [F = \ Lambda PE]}$ ${\ Displaystyle F = x, P = x, E = f \ (x\ x)}$ ${\ Displaystyle \ Operatorname {de-lambda} [F \ P = E]}$ ${\ Displaystyle \ operatorname {de-lambda} [x\ x=f\ (x\ x)]}$
8	${\displaystyle \operator {niech łączyć} [\operator {niech łączyć} p:\operator {de-lambda} [p\f]=\operator {niech łączyć} [\operator {niech} x:\operator {de -lambda} [x\ x=f\ (x\ x)]\nazwa operatora {w} f\ (x\ x)]\nazwa operatora {w} p]}$ ${\displaystyle \operator {niech łączyć} [\operator {niech} x:\operator {de-lambda} [x\ x=f\ (x\ x)]\operator {w} f\ (x\ x) ]}$ ${\displaystyle \operatorname {niech łączyć} [Y]}$ ${\ Displaystyle Y = \ nazwa operatora {niech} x: \ nazwa operatora {de-lambda} [x\ x = f\ (x\ x)] \ nazwa operatora {w} f \ (x\ x)}$ ${\ Displaystyle Y}$ ${\displaystyle \operatorname {niech} x:\operator {de-lambda} [x\ x=f\ (x\ x)]\operator {w} f\ (x\ x)}$
8	${\displaystyle \operator {niech łączyć} [\operator {niech} p:\operator {de-lambda} [p\ f]=\operator {niech} x:\operator {de-lambda} [x\ x= f\ (x\ x)]\nazwa operatora {w} f\ (x\ x)\nazwa operatora {w} p]}$ ${\displaystyle \operatorname {niech łączyć} [Y]}$ ${\ Displaystyle Y = \ nazwa operatora {niech} p: \ nazwa operatora {de-lambda} [p\ f = \ nazwa operatora {niech} x: \ nazwa operatora {de-lambda} [x\ x=f\ (x\ x) ]\nazwa operatora {w} f\ (x\ x)]\nazwa operatora {w} p}$ ${\ Displaystyle Y}$ ${\ Displaystyle \ nazwa operatora {niech} p: p \ f = \ nazwa operatora {niech} x: \ nazwa operatora {de-lambda} [x\ x = f\ (x\ x)] \ nazwa operatora {w} f \ (x \ x)\nazwa operatora {w} p}$
4	${\displaystyle \operator {niech} p:\operator {de-lambda} [p\f]=\operator {niech} x:\operator {de-lambda} [x\ x=f\ (x\ x)] \nazwa operatora {w} f\ (x\ x)\nazwa operatora {w} p}$ ${\ Displaystyle \ operatorname {de-lambda} [x\ x=f\ (x\ x)]}$ ${\ Displaystyle \ Operatorname {de-lambda} [E = F]}$ ${\ Displaystyle E = x \ x, F = f \ (x\ x)}$ ${\ Displaystyle \ operatorname {de-lambda} [E] = \ operatorname {de-lambda} [F]}$ ${\ Displaystyle \ operatorname {de-lambda} [x\ x] = \ operatorname {de-lambda} [f\ (x\ x)]}$
2	${\displaystyle \operator {niech} p:\operator {de-lambda} [p\f]=\operator {niech} x:\operator {de-lambda} [x\ x]=\operator {de-lambda} [f\ (x\ x)]\nazwa operatora {w} f\ (x\ x)\nazwa operatora {w} p}$ ${\ Displaystyle \ operatorname {de-lambda} [x\ x], \ operatorname {de-lambda} [f\ (x\ x)]}$ ${\displaystyle \operator {de-lambda} [p\f],\operator {de-lambda} [M_{1}\ N_{1}],\operator {de-lambda} [M_{2}\ N_{ 2}],}$ ${\displaystyle M_{1}=pN_{1}=fM_{2}=xN_{2}=xM_{3}=fN_{3}=x\x}$ ${\displaystyle \operator {de-lambda} [M_{1}]\ \operatorname {de-lambda} [N_{1}],\operator {de-lambda} [M_{2}]\ \operatorname {de- lambda} [N_{2}],\nazwa operatora {lambda} [M_{3}]\ \nazwa operatora {lambda} [N_{3}]}$ ${\displaystyle \operator {de-lambda} [p]\ \operator {de-lambda} [f],\operator {de-lambda} [x]\ \operator {de-lambda} [x],\operator { de-lambda} [f]\ \operator {de-lambda} [x]\ \operatorname {de-lambda} [x]}$
1	${\displaystyle \operator {niech} p:\operator {de-lambda} [p]\ \operator {de-lambda} [f]=\operator {niech} x:\operator {de-lambda} [x]\ \operatorname {lambda} [x]=\operatorname {lambda} [f]\ (\operatorname {lambda} [x]\ \operatorname {lambda} [x])\operatorname {in} f\ (x\ x)]\nazwa operatora {w} p}$ ${\ Displaystyle \ Operatorname {de-lambda} [V]}$ ${\ Displaystyle V}$
	${\displaystyle \operatorname {niech} p:p\f=\operator {niech} x:x\ x=f\ (x\ x)\operator {w} f\ (x\ x)]\operator {w} P}$

Konwersja z wyrażeń let do lambda

Zasady te odwracają konwersję opisaną powyżej. Konwertują z wyrażenia let na wyrażenie lambda bez zmiany struktury. Nie wszystkie wyrażenia let mogą być konwertowane przy użyciu tych reguł. Reguły zakładają, że wyrażenia są już ułożone tak, jakby zostały wygenerowane przez de-lambda .

1. ${\ Displaystyle \ Operatorname {get-lambda} [F, G \ V = E] = \ Operatorname {get-lambda} [F, G = \ Lambda VE]}$
2. ${\ Displaystyle \ operatorname {get-lambda} [F, F = E] = \ operatorname {de-let} [E]}$
3. ${\ Displaystyle \ Operatorname {de-let} [\ Lambda VE] \ Equiv \ Lambda V. \ Operator {de-let} [E]}$
4. ${\displaystyle \operatorname {de-let} [M\ N] \equiv \operatorname {de-let} [M] \ \operatorname {de-let} [N]}$
5. ${\ Displaystyle \ operatorname {de-let} [V] \ równoważne V}$
6. ${\ Displaystyle V \ nie \ w FV [\ nazwa operatora {get-lambda} [V, E]] \ do \ nazwa operatora {de-let} [\ nazwa operatora {niech} V: E \ \ nazwa operatora {w} V] \ equiv \operatorname {get-lambda} [V,E]}$
7. ${\ Displaystyle V \ nie \ w FV [\ nazwa operatora {get-lambda} [V, E]] \ do \ nazwa operatora {de-let} [\ nazwa operatora {niech} V: E \ \ nazwa operatora {w} L] \ equiv (\lambda V.\operator {de-let} [L])\ \operatorname {get-lambda} [V,E]}$
8. ${\ Displaystyle W \ nie \ w \ operatorname {FV} [\ operatorname {get-lambda} [V, E]] \ do \ operatorname {de-let} [\ operatorname {let} V, W: E \ land F \ \operatorname {w} G]\equiv \operatorname {de-let} [\operatorname {w} V:E\ \operatorname {w} \operatorname {w} W:F\ \operatorname {w} G]}$
9. ${\ Displaystyle V \ w \ nazwa operatora {FV} [\ nazwa operatora {get-lambda} [V, E]] \ do \ nazwa operatora {de-let} [\ nazwa operatora {niech} V: E \ \ nazwa operatora {w} L ]\equiv \operatorname {de-let} [\operatorname {let} V:V\ V=\operatorname {get-lambda} [V,E][V:=V\ V]\ \operatorname {in} L[ V:=V\ V]]}$
10. ${\ Displaystyle W \ w \ operatorname {FV} [\ operatorname {get-lambda} [V, E]] \ do \ operatorname {de-let} [\ operatorname {niech} V, W: E \ land F \ \ operatorname {w} L]\equiv \operatorname {de-let} [\operatorname {let} V:V\ W=\operatorname {get-lambda} [V,E][V:=V\ W]\ \operatorname {w} \operatorname {niech} W:F[V:=V\ W]\ \operatorname {w} L[V:=V\ W]]}$

Nie ma dokładnego odpowiednika strukturalnego w rachunku lambda dla wyrażeń let, które mają wolne zmienne, które są używane rekurencyjnie. W takim przypadku wymagane jest dodanie pewnych parametrów. Reguły 8 i 10 dodają te parametry.

Reguły 8 i 10 są wystarczające dla dwóch wzajemnie rekurencyjnych równań w wyrażeniu let . Jednak nie będą działać dla trzech lub więcej wzajemnie rekurencyjnych równań. Ogólny przypadek wymaga dodatkowego poziomu pętli, co sprawia, że ​​funkcja meta jest nieco trudniejsza. Poniższe zasady zastępują zasady 8 i 10 we wdrażaniu przypadku ogólnego. Reguły 8 i 10 pozostawiono, aby najpierw przestudiować prostszy przypadek.

1. lambda-form — przekonwertuj wyrażenie na połączenie wyrażeń, z których każdy ma postać zmienna = wyrażenie .
   1. ${\ Displaystyle \ nazwa operatora {forma lambda} [G \ V = E] = \ nazwa operatora {forma lambda} [G = \ lambda VE]}$
   2. ${\ Displaystyle \ nazwa operatora {forma lambda} [E \ ziemia F] = \ nazwa operatora {forma lambda} [E] \ ziemia \ nazwa operatora {forma lambda} [F]}$
   3. ${\ Displaystyle \ Operatorname {forma lambda} [V = E] = V = E}$...... gdzie V jest zmienną.
2. lift-vars — pobierz zestaw zmiennych, które wymagają X jako parametru, ponieważ wyrażenie ma X jako zmienną wolną.
   1. ${\ Displaystyle X \ w \ operatorname {FV} [E] \ do \ operatorname {lift-vars} [X, V = E] = \ {V \}}$
   2. ${\ Displaystyle X \ nie \ w \ operatorname {FV} [E] \ do \ operatorname {lift-vars} [X, V = E] = \ {\}}$
   3. ${\displaystyle \operatorname {lift-vars} [X,E\land F]=\operatorname {lift-vars} [X,E]\cup \operatorname {lift-vars} [XF]}$
3. pod- zmienne - Dla każdej zmiennej w zestawie zastąp ją zmienną zastosowaną do X w wyrażeniu. To sprawia, że X jest zmienną przekazywaną jako parametr, zamiast być wolną zmienną po prawej stronie równania.
   1. ${\displaystyle \operatorname {podzmienne} [E,\{V\}\cup S,X]=\operatorname {podzmienne} [E[V:=V\X],S,X]}$
   2. ${\ Displaystyle \ operatorname {podzmienne} [E, \ {\}, X] = E}$
4. de-let - Podnieś każdy warunek w E tak, że X nie jest wolną zmienną po prawej stronie równania.
   1. ${\ Displaystyle {\ zacząć {wyrównany} L & = \ nazwa operatora {forma lambda} [E] \ ziemia S = \ nazwa operatora {lift-vars} [X, L] \ do \ nazwa operatora {de-let} [\ nazwa operatora { let} V\ldots W,X:E\land F\ \nazwa operatora {w} G]\\&\equiv \nazwa operatora {de-let} [\nazwa operatora {let} V\ldots W:\nazwa operatora {podzmienne } [L,S,X]\ \operator {w} \operator {niech} \operator {podzmienne} [\operator {forma lambda} [F],S,X]\ \operator {w} \operator {podzmienne} [G,S,X]]\end{wyrównane}}}$

Przykłady

Na przykład wyrażenie let uzyskane z kombinatora Y ,

${\displaystyle \operatorname {niech} p:p\f=\operator {niech} x:x\q=f\ (q\q)\ \operatorname {w} f\ (x\ x)\ \operatorname {w } P}$

jest konwertowany na,

${\ Displaystyle \ lambda f. (\ lambda xf\ (x\ x))\ (\ lambda qf\ (q\ q))}$

Reguła	Wyrażenie lambda
6	${\displaystyle \operatorname {de-let} [\operatorname {niech} p:p\ f=\operator {niech} x:x\ q=f\ (q\ q)\ \operatorname {w} f\ (x \ x)\ \nazwa operatora {w} p]}$ ${\ Displaystyle \ nazwa operatora {de-let} [\ nazwa operatora {niech} V: E \ \ nazwa operatora {w} V]}$ ${\ Displaystyle V=p, E=p\ f=\operator {niech} x:x\ q=f\ (q\ q)\ \operatorname {w} f\ (x\ x)}$ ${\ Displaystyle \ Operatorname {get-lambda} [V, E]}$
1	${\displaystyle \operatorname {get-lambda} [p,p\f=\operatorname {niech} x:x\q=f\ (q\q)\ \operatorname {w} f\ (x\ x)]}$ ${\ Displaystyle \ Operatorname {get-lambda} [F, G \ V = E]}$ ${\ Displaystyle F = p, G = p, V = f, E = \ nazwa operatora {niech} x: x \ q = f \ (q\ q) \ \ nazwa operatora {w} f \ (x\ x)}$ ${\ Displaystyle \ Operatorname {get-lambda} [F, G = \ Lambda VE]}$
2	${\ Displaystyle \ operatorname {get-lambda} [p, p = \ lambda f. \ operatorname {niech} x: x\ q = f \ (q\ q) \ \ operatorname {w} f \ (x\ x) ]}$ ${\ Displaystyle \ Operatorname {get-lambda} [F, F = E]}$ ${\ Displaystyle F = p, E = \ lambda f. \ nazwa operatora {niech} x: x \ q = f \ (q\ q) \ \ nazwa operatora {w} f \ (x\ x)}$ ${\displaystyle \operatorname {de-let} [E]}$
3	${\displaystyle \operatorname {de-let} [\lambda f.\operatorname {niech} x:x\ q=f\ (q\ q)\ \operatorname {w} f\ (x\ x)]}$ ${\ Displaystyle \ operatorname {de-let} [\ lambda VE]}$ ${\ Displaystyle V = f, E = \ nazwa operatora {niech} x: x\ q = f \ (q\ q) \ \ nazwa operatora {w} f \ (x\ x)}$ ${\ Displaystyle \ lambda V. \ nazwa operatora {de-let} [E]}$
7	${\ Displaystyle \ lambda f. \ operatorname {de-let} [\ operatorname {niech} x: x \ q = f \ (q\ q) \ \ operatorname {w} f \ (x\ x)]}$ ${\displaystyle \operatorname {de-let} [\operatorname {niech} x:x\ q=f\ (q\ q)\ \operatorname {w} f\ (x\ x)]}$ ${\ Displaystyle V \ nie \ w FV [\ nazwa operatora {get-lambda} [V, E]] \ do \ nazwa operatora {de-let} [\ nazwa operatora {niech} V: E \ \ nazwa operatora {w} L]}$ ${\ Displaystyle V=x, E=x\ q=f\ (q\ q), L=f\ (x\ x)}$ ${\ Displaystyle (\ lambda V. \ operatorname {de-let} [L]) \ \ operatorname {get-lambda} [V, E]}$
4	${\ Displaystyle (\ lambda x. \ operatorname {de-let} [f\ (x\ x)]) \ \ operatorname {get-lambda} [x, x\ q=f\ (q\ q)]}$ ${\displaystyle \operatorname {de-let} [f\ (x\ x)]}$ ${\ Displaystyle \ operatorname {de-let} [M \ N]}$ ${\ Displaystyle M = f, N = (x\ x)}$ ${\ Displaystyle \ operatorname {de-let} [M] \ \ operatorname {de-let} [N]}$ ${\displaystyle \operatorname {de-let} [f]\ \operatorname {de-let} [x\ x]}$
4	${\ Displaystyle (\ lambda x. \ operatorname {de-let} [f] \ \ operatorname {de-let} [x\ x]) \ \ operatorname {get-lambda} [x, x\ q = f \ ( q\ q)]}$ ${\displaystyle \operatorname {de-let} [x\ x]}$ ${\ Displaystyle \ operatorname {de-let} [M \ N]}$ ${\ Displaystyle M = x, N = x}$ ${\ Displaystyle \ operatorname {de-let} [M] \ \ operatorname {de-let} [N]}$ ${\displaystyle \operatorname {delet} [x]\ \operatorname {delet} [x]}$
5	${\ Displaystyle (\ lambda x. \ operatorname {de-let} [f] \ (\ operatorname {de-let} [x] \ \ operatorname {de-let} [x])) \ \ operatorname {get-lambda } [x,x\ q=f\ (q\ q)]}$ ${\displaystyle \operatorname {delet} [V]}$ ${\ Displaystyle V}$
1	${\ Displaystyle (\ lambda xf \ (x\ x)) \ \ operatorname {get-lambda} [x, x\ q=f\ (q\ q)]}$ ${\ Displaystyle \ operatorname {get-lambda} [x, x\ q=f\ (q\ q)]}$ ${\ Displaystyle \ Operatorname {get-lambda} [F, G \ V = E]}$ ${\ Displaystyle F=x,G=x,V=q,E=f\ (q\ q)}$ ${\ Displaystyle \ Operatorname {get-lambda} [F, G = \ Lambda VE]}$ ${\ Displaystyle \ operatorname {get-lambda} [x, x = \ lambda qf \ (q\ q)]}$
2	${\ Displaystyle (\ lambda xf \ (x\ x)) \ \ operatorname {get-lambda} [x, x = \ lambda qf \ (q\ q)]}$ ${\ Displaystyle \ operatorname {get-lambda} [x, x = \ lambda qf \ (q\ q)]}$ ${\ Displaystyle \ Operatorname {get-lambda} [F, F = E]}$ ${\ Displaystyle F = x, E = \ lambda qf \ (q\ q)}$ ${\displaystyle \operatorname {de-let} [E]}$ ${\ Displaystyle \ operatorname {de-let} [\ lambda qf \ (q\ q)]}$
3	${\ Displaystyle (\ lambda xf \ (x\ x)) \ \ operatorname {de-let} [\ lambda qf \ (q\ q)]}$ ${\ Displaystyle \ operatorname {de-let} [\ lambda qf \ (q\ q)]}$ ${\ Displaystyle \ operatorname {de-let} [\ lambda VE]}$ ${\ Displaystyle V = q, E = f\ (q\ q)}$ ${\ Displaystyle \ lambda V. \ nazwa operatora {de-let} [E]}$ ${\ Displaystyle \ lambda q. \ operatorname {de-let} [f\ (q\ q)]}$
4	${\ Displaystyle (\ lambda xf\ (x\ x))\ (\ lambda q.\operator {de-let} [f\ (q\ q)])}$ ${\displaystyle \operatorname {de-let} [f\ (q\ q)]}$ ${\displaystyle \operatorname {de-let} [M_{1}\ N_{1}]}$ ${\displaystyle M_{1}=f,N_{1}=q\q}$ ${\displaystyle \operatorname {delet} [M_{1}]\ \operatorname {delet} [N_{1}]}$ ${\displaystyle \operatorname {de-let} [f]\ \operatorname {de-let} [q\ q]}$ ${\displaystyle \operatorname {de-let} [M_{2}\ N_{2}]}$ ${\displaystyle M_{2}=q,N_{2}=q}$ ${\displaystyle \operatorname {delet} [q]\ \operatorname {delet} [q]}$
5	${\ Displaystyle (\ lambda xf \ (x\ x)) \ (\ lambda q. \ operatorname {de-let} [f] \ (\ operatorname {de-let} [q] \ \ operatorname {de-let} [Q]))}$ ${\displaystyle \operatorname {delet} [V]}$ ${\styl wyświetlania}$ ${\ Displaystyle V}$
	${\ Displaystyle (\ lambda xf\ (x\ x))\ (\ lambda qf\ (q\ q))}$

Jako drugi przykład weź podniesioną wersję kombinatora Y ,

${\ Displaystyle \ operatorname {niech} p, q: p\ f\ x=f\ (x\ x) \ ziemia q\ p\ f= (p\ f) \ (p\ f) \ \ operatorname {w} q\ p}$

jest konwertowany na,

${\ Displaystyle (\ lambda p. (\ lambda qq\ p) \ \ lambda p. \ lambda f. (p \ f) \ (p \ f)) \ \ lambda f. \ lambda xf \ (x\ x) }$

Reguła	Wyrażenie lambda
8	${\displaystyle \operatorname {de-let} [\operatorname {niech} p,q:p\ f\ x=f\ (x\ x)\land q\ p\ f=(p\ f)\ (p\ f)\ \nazwa operatora {w} q\ p]}$
7	${\displaystyle \operatorname {de-let} [\operator {niech} p:p\ f\ x=f\ (x\ x)\ \operatorname {w} \operatorname {niech} q:q\ p\ f= (p\ f)\ (p\ f)\ \nazwa operatora {w} q\ p]}$
1, 2	${\ Displaystyle (\ lambda p. \ operatorname {de-let} [\ operatorname {niech} q: q\ p\ f = (p\ f) \ (p\ f) \ \ operatorname {w} q\ p] )\ \operatorname {get-lambda} [p,p\ f\ x=f\ (x\ x)]}$
7, 4, 5	${\ Displaystyle (\ lambda p. \ operatorname {de-let} [\ operatorname {niech} q: q\ p\ f = (p\ f) \ (p\ f) \ \ operatorname {w} q\ p] )\ \lambda f.\lambda xf\ (x\ x)}$
1, 2	${\ Displaystyle (\ lambda p. (\ lambda qq\ p) \ \ operatorname {get-lambda} [q, q\ p \ f = (p \ f) \ (p \ f)]) \ \ lambda f. \lambda xf\ (x\ x)}$
	${\ Displaystyle (\ lambda p. (\ lambda qq\ p) \ \ lambda p. \ lambda f. (p \ f) \ (p \ f)) \ \ lambda f. \ lambda xf \ (x\ x) }$

Dla trzeciego przykładu tłumaczenie,

${\ Displaystyle \ operatorname {niech} x: x \ f = f \ (x\ f) \ \ operatorname {w} x}$

jest,

${\ Displaystyle (\ lambda xx\ x)\ (\ lambda x. \ lambda ff \ (x\ x\ f))}$

Reguła	Wyrażenie lambda
9	${\ Displaystyle \ operatorname {niech} x: x \ f = f \ (x\ f) \ \ operatorname {w} x}$
1	${\displaystyle \operatorname {niech} x:\operatorname {get-lambda} [x,x\ f=f\ (x\ f)][x:=x\ x]\ \operatorname {w} x[x: =x\ x]}$
2	${\displaystyle \operatorname {niech} x:\operatorname {get-lambda} [x,x=\lambda ff\ (x\ f)][x:=x\ x]\ \operatorname {w} x\ x}$
	${\ Displaystyle \ operatorname {niech} x: (x = \ lambda ff \ (x \ f)) [x: = x \ x] \ \ operatorname {w} x \ x}$
7	${\ Displaystyle \ operatorname {niech} x: (x \ x = \ lambda ff \ (x \ x \ f)) \ \ operatorname {w} x \ x}$
1	${\ Displaystyle (\ lambda xx \ x) \ \ operatorname {get-lambda} [x, x \ x = \ lambda ff \ (x\ x\ f)]}$
2	${\ Displaystyle (\ lambda xx \ x) \ \ operatorname {get-lambda} [x, x = \ lambda x. \ lambda ff \ (x\ x\ f)]}$
	${\ Displaystyle (\ lambda xx\ x)\ (\ lambda x. \ lambda ff \ (x\ x\ f))}$

Kluczowi ludzie

• Dana Scott

Zobacz też

• Zakres (informatyka)
• Podnoszenie lambdy
• Kombinator stałopunktowy
• Rachunek lambda
• Paradoks Curry'ego
• Dedukcyjny rachunek lambda
• Programowanie logiki ograniczeń
• Zawężenie algebraicznych zbiorów wartości

Bibliografia