Systém F
Systém F je logický formalismus , který umožňuje vyjádřit funkcí ve velmi bohaté a velmi přísné způsobem a formálně prokázat obtížné vlastnosti. Konkrétně systém F (známý také pod názvem polymorfní lambda kalkul nebo lambda kalkul druhého řádu ) je rozšířením lambda kalkulu jednoduše napsaného, který zavedl nezávisle logik Jean-Yves Girard a počítačový vědec John C. Reynolds . Tento systém se odlišuje od lambda-kalkulu jednoduše napsaného existencí univerzální kvantifikace typů, které umožňují vyjádřit polymorfismus.
Systém F má dvě zásadní vlastnosti:
- redukce termínů se silně normalizuje (více řečeno: všechny výpočty končí);
- to odpovídá podle korespondence Curry-Howard na minimální logiky Výroková druhého řádu . To znamená: výrokový počet bez negace, ale s kvantifikátory .
Úvodní poznámka : Čtení tohoto článku předpokládá předběžné čtení článku „ lambda-kalkul “ a jeho asimilaci.
Úvod
Jak dokazuje jeho dvojí původ, systém F lze studovat ve dvou velmi odlišných kontextech:
- V oblasti funkčního programování, kde se jeví jako velmi expresivní rozšíření jádra jazyka ML. Jeho expresivitu ilustruje skutečnost, že běžné datové typy (boolean, celá čísla, seznamy atd.) Jsou v systému F definovatelné ze základních konstrukcí;
- V oblasti logiky a konkrétněji v teorii důkazu. Prostřednictvím Curry-Howardovy korespondence je systém F skutečně izomorfní s minimální logikou druhého řádu. Tento systém navíc velmi přesně zachycuje třídu numerických funkcí, jejichž existence je prokazatelná v intuitivní aritmetice druhého řádu (někdy se jí říká intuitivní analýza ). Je to navíc tato pozoruhodná vlastnost systému F, která historicky motivovala jeho zavedení Jean-Yvesem Girardem, pokud tato vlastnost umožňuje vyřešit problém eliminace škrtů v aritmetice druhého řádu, předpokládaných Takeuti (in) .
Historicky hrál systém F zásadní roli v základech výpočetní techniky tím, že od začátku sedmdesátých let navrhoval bohatý, jednoduchý a velmi expresivní formalizmus velmi obecných vypočítatelných funkcí. Vydláždilo cestu moderním typizovaným programovacím jazykům a asistentům jako COQ .
Stejně jako lambda kalkul jednoduše zadaného systému, systém F připouští dvě ekvivalentní prezentace:
- Prezentace pro církev , ve které každý semestr obsahuje všechny typové anotace potřebné k rekonstrukci jejího typu (jednoznačně);
- Prezentace à la Curry díky počítačovému vědci Danielovi Leivantovi, ve které výrazy (které jsou výrazy čistého lambda-kalkulu) postrádají jakoukoli anotaci typu, a proto podléhají problémům typické nejednoznačnosti.
Prezentace v kostele
Systém F připouští dva druhy objektů: typy a termíny . Termíny lze „sbalit“ a přeložit vypočítatelné funkce, zatímco typy anotují termíny a umožňují jejich zařazení do kategorií.
Syntaxe
Typ systémové F (označený , , atd) jsou vytvořeny ze souboru typy proměnných (jmenovitý , , atd) za použití následujících tří budov pravidla:
NA{\ displaystyle A}
B{\ displaystyle B}
VS{\ displaystyle C}
α{\ displaystyle \ alpha}
β{\ displaystyle \ beta}
y{\ displaystyle \ gamma}![\ gama](https://wikimedia.org/api/rest_v1/media/math/render/svg/a223c880b0ce3da8f64ee33c4f0010beee400b1a)
- ( Proměnná typu ) Pokud je proměnná typu, pak je to typ;α{\ displaystyle \ alpha}
α{\ displaystyle \ alpha}![\ alfa](https://wikimedia.org/api/rest_v1/media/math/render/svg/b79333175c8b3f0840bfb4ec41b8072c83ea88d3)
- ( Typ šipky ) Pokud a jsou typy, pak je to typ;NA{\ displaystyle A}
B{\ displaystyle B}
NA→B{\ displaystyle A \ až B}![A \ až B](https://wikimedia.org/api/rest_v1/media/math/render/svg/d5b8dd84619daff17b52a08b77d15db2b9ad6c2a)
- ( Univerzální typ ) If is a type variable and a type, then is a type.α{\ displaystyle \ alpha}
B{\ displaystyle B}
∀α B{\ displaystyle \ forall \ alpha ~ B}![{\ displaystyle \ forall \ alpha ~ B}](https://wikimedia.org/api/rest_v1/media/math/render/svg/431e4a70c7da3928c2ef4a14f11780a0369867a5)
Stručně řečeno, typy systému F jsou dány gramatikou BNF :
NA,B :: = α | NA→B | ∀α B.{\ displaystyle A, B ~~ :: = ~~ \ alpha ~~ | ~~ A \ až B ~~ | ~~ \ forall \ alpha ~ B.}
Stejně jako v lambda-kalkulu nebo v predikátovém kalkulu vyžaduje přítomnost mutujícího symbolu rozlišování pojmů volné proměnné a vázané proměnné a zavedení obvyklých mechanismů přejmenování umožňujících zpracování až -konverze. Nakonec je typová algebra systému F opatřena substituční operací podobnou operaci lambda-kalkulu a označujeme typ získaný nahrazením všech volných výskytů proměnné typu typem v typu .
∀{\ displaystyle \ forall}
α{\ displaystyle \ alpha}
B{α: =NA}{\ displaystyle B \ {\ alpha: = A \}}
B{\ displaystyle B}
α{\ displaystyle \ alpha}
NA{\ displaystyle A}![NA](https://wikimedia.org/api/rest_v1/media/math/render/svg/7daff47fa58cdfd29dc333def748ff5fa4c923e3)
Tyto termíny (brutto) System F (jmenovitý , atd.) Jsou vytvořeny ze sady, pokud jde o proměnných (označený , , atd), za použití pěti následujících pravidel stavby:
M{\ displaystyle M}
NE{\ displaystyle N}
X{\ displaystyle x}
y{\ displaystyle}
z{\ displaystyle z}![z](https://wikimedia.org/api/rest_v1/media/math/render/svg/bf368e72c009decd9b6686ee84a375632e11de98)
- ( Proměnná ) Pokud je proměnná výrazu, pak je výrazem;X{\ displaystyle x}
X{\ displaystyle x}![X](https://wikimedia.org/api/rest_v1/media/math/render/svg/87f9e315fd7e2ba406057a97300593c4802b53e4)
- ( Abstrakce ) Pokud je proměnná výrazu, typ a výraz, pak je to termín;X{\ displaystyle x}
NA{\ displaystyle A}
M{\ displaystyle M}
λX:NA.M{\ displaystyle \ lambda x: AM}![{\ displaystyle \ lambda x: AM}](https://wikimedia.org/api/rest_v1/media/math/render/svg/dda806775412549996c38fc8814859343d3e3d18)
- ( Přihláška ) Pokud a jsou termíny, pak je to termín;M{\ displaystyle M}
NE{\ displaystyle N}
MNE{\ displaystyle MN}![MN](https://wikimedia.org/api/rest_v1/media/math/render/svg/6fa6819fea85a0b616a35d340ad6461ababdbeee)
- ( Typ abstrakce ) Pokud je proměnná typu a výraz, pak je výraz;α{\ displaystyle \ alpha}
M{\ displaystyle M}
Λα.M{\ displaystyle \ Lambda \ alpha .M}![{\ displaystyle \ Lambda \ alpha .M}](https://wikimedia.org/api/rest_v1/media/math/render/svg/df7ca0f6dcb7bb79b46d9c5f8724829d1243bdf8)
- ( Typ aplikace ) Pokud je termín a typ, pak je termín.M{\ displaystyle M}
NA{\ displaystyle A}
MNA{\ displaystyle MA}![{\ displaystyle MA}](https://wikimedia.org/api/rest_v1/media/math/render/svg/be6250feb34ae98d9b710a8b069d15811718a9c1)
Stručně řečeno, (surové) podmínky systému F jsou dány gramatikou BNF:
M,NE :: = X | λX:NA.M | MNE | Λα.M | MNA.{\ displaystyle M, N ~~ :: = ~~ x ~~ | ~~ \ lambda x \, {:} \, A \ ,. \, M ~~ | ~~ MN ~~ | ~~ \ Lambda \ alpha \ ,. \, M ~~ | ~~ MA.}
Pojmy systému F zahrnují dva variabilní vazebné mechanismy: termín variabilní vazebný mechanismus (konstrukcí ) a typ variabilní vazebný mechanismus (konstrukcí ), oba jsou brány v úvahu na úrovni vztahu -konverze. Tento dvojitý mechanismus přirozeně vede ke dvěma substitučním operacím: substituce známého termínu a substituce známého typu .
λX:NA.M{\ displaystyle \ lambda x \, {:} \, A \ ,. \, M}
Λα.M{\ displaystyle \ Lambda \ alpha \ ,. \, M}
α{\ displaystyle \ alpha}
M{X: =NE}{\ displaystyle M \ {x: = N \}}
M{α: =NA}{\ displaystyle M \ {\ alpha: = A \}}![{\ displaystyle M \ {\ alpha: = A \}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/21877c20ec78fe08e30f474055852ba7df81891f)
-reductionβ{\ displaystyle \ beta}
Přítomnost dvojitého mechanismu abstrakce a aplikace (abstrakce / termínová aplikace a abstrakce / typová aplikace) vede ke dvěma pravidlům -redukce, jejichž sjednocení generuje přechodem do kontextu vztah -redukce v jednom kroku systém F:
β{\ displaystyle \ beta}
β{\ displaystyle \ beta}![\beta](https://wikimedia.org/api/rest_v1/media/math/render/svg/7ed48a5e36207156fb792fa79d29925d2f7901e8)
-
(λX:NA.M)NE⟶M{X: =NE}{\ displaystyle (\ lambda x \, {:} \, A \ ,. \, M) N \ longrightarrow M \ {x: = N \}}
;
-
(Λα.M)NA⟶M{α: =NA}{\ displaystyle (\ Lambda \ alpha \ ,. \, M) A \ longrightarrow M \ {\ alpha: = A \}}
.
Co se týče čistého lambda-kalkulu, -redukce systému F je splývající (z hrubého hlediska) a splňuje vlastnost Church-Rosser :
β{\ displaystyle \ beta}![\beta](https://wikimedia.org/api/rest_v1/media/math/render/svg/7ed48a5e36207156fb792fa79d29925d2f7901e8)
- (Soutok -reduction) Je-li a , pak existuje termín tak, že a ;β{\ displaystyle \ beta}
M⟶∗M1{\ displaystyle M \ longrightarrow ^ {*} M_ {1}}
M⟶∗M2{\ displaystyle M \ longrightarrow ^ {*} M_ {2}}
M′{\ displaystyle M '}
M1⟶∗M′{\ displaystyle M_ {1} \ longrightarrow ^ {*} M '}
M2⟶∗M′{\ displaystyle M_ {2} \ longrightarrow ^ {*} M '}![{\ displaystyle M_ {2} \ longrightarrow ^ {*} M '}](https://wikimedia.org/api/rest_v1/media/math/render/svg/981cb8c25dc25d52b268b157d954ee1b9c5300f5)
- (Majetek církve-Rosserova) U dvou termínů a být -convertible, je nutné a dostačující, že existuje pojem , jako je a .M1{\ displaystyle M_ {1}}
M2{\ displaystyle M_ {2}}
β{\ displaystyle \ beta}
M′{\ displaystyle M '}
M1⟶∗M′{\ displaystyle M_ {1} \ longrightarrow ^ {*} M '}
M2⟶∗M′{\ displaystyle M_ {2} \ longrightarrow ^ {*} M '}![{\ displaystyle M_ {2} \ longrightarrow ^ {*} M '}](https://wikimedia.org/api/rest_v1/media/math/render/svg/981cb8c25dc25d52b268b157d954ee1b9c5300f5)
Typový systém
Volal psaní kontext (notace: , atd.) Jakýkoliv konečný seznam výpisů z formy (což je termín, variabilní a typ), ve kterém je termín proměnná deklarována více než jednou.
Γ{\ displaystyle \ Gamma}
Γ′{\ displaystyle \ Gamma '}
X:NA{\ displaystyle x: A}
X{\ displaystyle x}
NA{\ displaystyle A}![NA](https://wikimedia.org/api/rest_v1/media/math/render/svg/7daff47fa58cdfd29dc333def748ff5fa4c923e3)
Typový systém systému F je postaven na typizačním posouzení formy („v kontextu má termín pro typ “), který je definován z následujících odvozovacích pravidel:
Γ⊢M:NA{\ displaystyle \ Gamma \ vdash M: A}
Γ{\ displaystyle \ Gamma}
M{\ displaystyle M}
NA{\ displaystyle A}![NA](https://wikimedia.org/api/rest_v1/media/math/render/svg/7daff47fa58cdfd29dc333def748ff5fa4c923e3)
- ( Axiom ) pokud ;Γ⊢X:NA{\ displaystyle {\ frac {} {\ Gamma \ vdash x: A}}}
(X:NA)∈Γ{\ displaystyle (x: A) \ v \ Gamma}![{\ displaystyle (x: A) \ v \ Gamma}](https://wikimedia.org/api/rest_v1/media/math/render/svg/cbb7f8119f3d2a5da8bcd8a2f296b9a48bf0470a)
- ( -intro ) ;→{\ displaystyle \ to}
Γ,X:NA⊢M:BΓ⊢λX:NA.M:NA→B{\ displaystyle {\ frac {\ Gamma, x: A \ vdash M: B} {\ Gamma \ vdash \ lambda x \, {:} \, A \ ,. \, M: A \ až B}}}![{\ displaystyle {\ frac {\ Gamma, x: A \ vdash M: B} {\ Gamma \ vdash \ lambda x \, {:} \, A \ ,. \, M: A \ až B}}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/ed3e69192184603b90bb5c8886eedb17dd3f25f6)
- ( -elim ) ;→{\ displaystyle \ to}
Γ⊢M:NA→BΓ⊢NE:NAΓ⊢MNE:B{\ displaystyle {\ frac {\ Gamma \ vdash M: A \ až B \ quad \ Gamma \ vdash N: A} {\ Gamma \ vdash MN: B}}}![{\ displaystyle {\ frac {\ Gamma \ vdash M: A \ až B \ quad \ Gamma \ vdash N: A} {\ Gamma \ vdash MN: B}}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/8fd4463d09a07857d852dd6e52f7f8e98d4bba6a)
- ( -intro ) pokud nemá volný výskyt v ;∀{\ displaystyle \ forall}
Γ⊢M:BΓ⊢Λα.M:∀α B{\ displaystyle {\ frac {\ Gamma \ vdash M: B} {\ Gamma \ vdash \ Lambda \ alpha \ ,. \, M: \ forall \ alpha ~ B}}}
α{\ displaystyle \ alpha}
Γ{\ displaystyle \ Gamma}![\ Gama](https://wikimedia.org/api/rest_v1/media/math/render/svg/4cfde86a3f7ec967af9955d0988592f0693d2b19)
- ( -elim ) .∀{\ displaystyle \ forall}
Γ⊢M:∀α BΓ⊢MNA:B{α: =NA}{\ displaystyle {\ frac {\ Gamma \ vdash M: \ forall \ alpha ~ B} {\ Gamma \ vdash MA: B \ {\ alpha: = A \}}}}![{\ displaystyle {\ frac {\ Gamma \ vdash M: \ forall \ alpha ~ B} {\ Gamma \ vdash MA: B \ {\ alpha: = A \}}}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/d3616a8fa3601706bc4f493594a9bd4c4980e26d)
Dvě hlavní vlastnosti tohoto typu systému jsou vlastnost zachování typu -redukceβ{\ displaystyle \ beta}
a silná normalizační vlastnost :
- ( Zachování typu redukcí ) Pokud a pokud , pak ;Γ⊢M:NA{\ displaystyle \ Gamma \ vdash M: A}
M⟶∗M′{\ displaystyle M \ longrightarrow ^ {*} M '}
Γ⊢M′:NA{\ displaystyle \ Gamma \ vdash M ': A}![{\ displaystyle \ Gamma \ vdash M ': A}](https://wikimedia.org/api/rest_v1/media/math/render/svg/67b9b2b438e37085aa2a7bd58c43c4c2cd15032d)
- ( Silná normalizace ) Pokud , pak je silně normalizovatelná.Γ⊢M:NA{\ displaystyle \ Gamma \ vdash M: A}
M{\ displaystyle M}![M](https://wikimedia.org/api/rest_v1/media/math/render/svg/f82cade9898ced02fdd08712e5f0c0151758a0dd)
První z těchto dvou vlastností je čistě kombinatorická vlastnost, která je demonstrována přímou indukcí na derivaci psaní. Na druhou stranu je silnou normalizační vlastností systému F vlastnost, jejíž důkaz spočívá zásadně na nekombinatorních metodách založených na pojmu redukovatelnosti kandidátů.
Reprezentace datových typů
Aby bylo možné použít jednoduše zadaný lambda-kalkul jako programovací jazyk, je nutné přidat základní typy (boolean, celá čísla atd.) A další redukční pravidla, která rozšiřují expresivní sílu formalismu. Příkladem takového rozšíření je Gödelův T systém, který se získá přidáním primitivních přirozených celých čísel lambda-kalkulu a rekurzního mechanismu podobného primitivní rekurzi (ale expresivnější).
V systému F takové rozšíření není nutné, protože expresivita formalismu umožňuje definovat základní typy a obvyklé konstruktory typů, aniž by bylo nutné upravit buď typový systém, nebo redukční pravidla.
Booleovské a konečné typy
Typ booleů je definován v systému F pomocí
- Boole ≡ ∀y(y→y→y){\ displaystyle {\ textbf {Bool}} ~ \ equiv ~ \ forall \ gamma \, (\ gamma \ to \ gamma \ to \ gamma)}
![{\ displaystyle {\ textbf {Bool}} ~ \ equiv ~ \ forall \ gamma \, (\ gamma \ to \ gamma \ to \ gamma)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/11ee015080606a1bd644751777b866cccdd81ed7)
a konstanty a podle:
skutečný{\ displaystyle {\ textbf {true}}}
Nepravdivé{\ displaystyle {\ textbf {false}}}![{\ displaystyle {\ textbf {false}}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/4fa9a44680206f3cfe44567d4e934b782fad2feb)
-
skutečný ≡ Λy.λX,y:y.X : Boole{\ displaystyle {\ textbf {true}} ~ \ equiv ~ \ Lambda \ gamma \ ,. \, \ lambda x, y \, {:} \, \ gamma \ ,. \, x ~: ~ {\ textbf { Bool}}}
;
-
Nepravdivé ≡ Λy.λX,y:y.y : Boole{\ displaystyle {\ textbf {false}} ~ \ equiv ~ \ Lambda \ gamma \ ,. \, \ lambda x, y \, {:} \, \ gamma \ ,. \, y ~: ~ {\ textbf { Bool}}}
.
Je možné ukázat, že dva výše uvedené výrazy jsou jediné dva výrazy uzavřené v normální formě typu . Datový typ tedy účinně vystihuje pojem boolean.
Boole{\ displaystyle {\ textbf {Bool}}}
Boole{\ displaystyle {\ textbf {Bool}}}![{\ displaystyle {\ textbf {Bool}}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/653b1b6a206bccb8e5bf69525436e779f8ea92b2)
Konstrukt „pokud… pak… jinak…“ je definován
- tisVS M pak NE1 jiný NE2 ≡ MVSNE1NE2{\ displaystyle {\ texttt {if}} _ {C} ~ M ~ {\ texttt {then}} ~ N_ {1} ~ {\ texttt {else}} ~ N_ {2} ~ \ equiv ~ MCN_ {1} N_ {2}}
![{\ displaystyle {\ texttt {if}} _ {C} ~ M ~ {\ texttt {then}} ~ N_ {1} ~ {\ texttt {else}} ~ N_ {2} ~ \ equiv ~ MCN_ {1} N_ {2}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/6215f8cec72bdda8efdd96b416d120f528786785)
kde označuje typ eliminace konstrukce „pokud ...“, tj. typ společný pro dvě větve podmíněného. Tato definice je správná z hlediska psaní, jako z hlediska výpočtu, pokud:
VS{\ displaystyle C}![VS](https://wikimedia.org/api/rest_v1/media/math/render/svg/4fc55753007cd3c18576f7933f6f089196732029)
- V jakémkoli kontextu, kde výraz má typ a kde výrazy a typ mají , je konstrukce dobře napsaná a má typ jako svůj typ ;M{\ displaystyle M}
Boole{\ displaystyle {\ textbf {Bool}}}
NE1{\ displaystyle N_ {1}}
NE2{\ displaystyle N_ {2}}
VS{\ displaystyle C}
tisVS M pak NE1 jiný NE2{\ displaystyle {\ texttt {if}} _ {C} ~ M ~ {\ texttt {then}} ~ N_ {1} ~ {\ texttt {else}} ~ N_ {2}}
VS{\ displaystyle C}![VS](https://wikimedia.org/api/rest_v1/media/math/render/svg/4fc55753007cd3c18576f7933f6f089196732029)
- Pokud se termín redukuje na , pak se konstrukce redukuje na ;M{\ displaystyle M \, \!}
skutečný{\ displaystyle {\ textbf {true}}}
tisVS M pak NE1 jiný NE2{\ displaystyle {\ texttt {if}} _ {C} ~ M ~ {\ texttt {then}} ~ N_ {1} ~ {\ texttt {else}} ~ N_ {2}}
NE1{\ displaystyle N_ {1} \, \!}![N_1 \, \!](https://wikimedia.org/api/rest_v1/media/math/render/svg/931eb7e58bc7c1e65ed813c23059c8988abc81ad)
- Pokud se termín sníží na , pak se konstrukce sníží na .M{\ displaystyle M \, \!}
Nepravdivé{\ displaystyle {\ textbf {false}}}
tisVS M pak NE1 jiný NE2{\ displaystyle {\ texttt {if}} _ {C} ~ M ~ {\ texttt {then}} ~ N_ {1} ~ {\ texttt {else}} ~ N_ {2}}
NE2{\ displaystyle N_ {2} \, \!}![N_2 \, \!](https://wikimedia.org/api/rest_v1/media/math/render/svg/6149f4c0de5332c766bd7f86e6a8c3b52d47667a)
Obecněji lze definovat konečný typ s hodnotami podle:
Ene{\ displaystyle E_ {n}}
ne{\ displaystyle n}
E1,...,Ene{\ displaystyle e_ {1}, \ ldots, e_ {n}}![{\ displaystyle e_ {1}, \ ldots, e_ {n}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/c60c38b7e2450d62e9dc496b89f8e5c96c77cecf)
-
Ene ≡ ∀y(y→⋯→y⏟ne→y){\ displaystyle E_ {n} ~ \ equiv ~ \ forall \ gamma \, (\ underbrace {\ gamma \ to \ cdots \ to \ gamma} _ {n} \ to \ gamma)}
;
-
Ei ≡ Λy.λX1,...,Xne:y.Xi{\ Displaystyle e_ {i} ~ \ equiv ~ \ Lambda \ gamma \ ,. \, \ lambda x_ {1}, \ ldots, x_ {n} \, {:} \, \ gamma \ ,. \, x_ { já}}
(pro všechno ).1≤i≤ne{\ displaystyle 1 \ leq i \ leq n}![{\ displaystyle 1 \ leq i \ leq n}](https://wikimedia.org/api/rest_v1/media/math/render/svg/abbe58b9b83f8b6ec0da570e2249323a8930ef1e)
Opět je možné ukázat, že termíny jsou jedinými uzavřenými termíny ve formě normálního typu . Odpovídající operace filtrování je definována:
E1,...,Ene{\ displaystyle e_ {1}, \ ldots, e_ {n}}
Ene{\ displaystyle E_ {n}}![v](https://wikimedia.org/api/rest_v1/media/math/render/svg/ad6b82f2a00af6c9efd4c16d4e99329605645c0c)
- zápasVS M s E1↦NE1|⋯|Ene↦NEne ≡ MVSNE1⋯NEne{\ displaystyle {\ texttt {match}} _ {C} ~ M ~ {\ texttt {with}} ~ e_ {1} \ mapsto N_ {1} | \ cdots | e_ {n} \ mapsto N_ {n} ~ \ equiv ~ M \, C \, N_ {1} \ cdots N_ {n}}
![{\ displaystyle {\ texttt {match}} _ {C} ~ M ~ {\ texttt {with}} ~ e_ {1} \ mapsto N_ {1} | \ cdots | e_ {n} \ mapsto N_ {n} ~ \ equiv ~ M \, C \, N_ {1} \ cdots N_ {n}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/620cc5e0e4d205b20300373e3a77b7b5806be1c1)
(kde označuje typ větví filtru).
VS{\ displaystyle C}![VS](https://wikimedia.org/api/rest_v1/media/math/render/svg/4fc55753007cd3c18576f7933f6f089196732029)
Zejména :
-
E2 ≡ ∀y(y→y→y) ≡ Boole{\ displaystyle E_ {2} ~ \ equiv ~ \ forall \ gamma \, (\ gamma \ to \ gamma \ to \ gamma) ~ \ equiv ~ {\ textbf {bool}}}
(typ booleanů);
-
E1 ≡ ∀y(y→y) ≡ Jednotka{\ displaystyle E_ {1} ~ \ equiv ~ \ forall \ gamma \, (\ gamma \ to \ gamma) ~ \ equiv ~ {\ textbf {jednotka}}}
(singletonový typ);
-
E0 ≡ ∀yy ≡ Prázdný{\ displaystyle E_ {0} ~ \ equiv ~ \ forall \ gamma \, \ gamma ~ \ equiv ~ {\ textbf {prázdný}}}
(prázdný typ).
Typ není obýván žádným uzavřeným termínem v normální formě a podle silné věty o normalizaci není obýván žádným uzavřeným termínem.
E0{\ displaystyle E_ {0}}![E_0](https://wikimedia.org/api/rest_v1/media/math/render/svg/411d268de7b1cf300d7481e3fe59f3b20887e0d0)
Kartézský součin a přímý součet
Buď a dva typy. Kartézský produkt je definován v systému F o
NA{\ displaystyle A}
B{\ displaystyle B}
NA×B{\ displaystyle A \ krát B}![A \ krát B](https://wikimedia.org/api/rest_v1/media/math/render/svg/65f31ae45b0098f06b5d22c38d317eb097a88fa9)
- NA×B ≡ ∀y((NA→B→y)→y){\ Displaystyle A \ times B ~ \ equiv ~ \ forall \ gamma \, ((A \ to B \ to \ gamma) \ to \ gamma)}
![{\ Displaystyle A \ times B ~ \ equiv ~ \ forall \ gamma \, ((A \ to B \ to \ gamma) \ to \ gamma)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/3a0b8bf3b7f16a9d9788dc24af663cda238301b6)
a stavba páru
-
⟨M;NE⟩ ≡ Λy.λF:(NA→B→y).FMNE : NA×B{\ Displaystyle \ langle M; N \ rangle ~ \ equiv ~ \ Lambda \ gamma \ ,. \, \ lambda f \, {:} \, (A \ až B \ až \ gamma) \ ,. \, f \ , M \, N ~: ~ A \ krát B}
(pokud a )M:NA{\ displaystyle M: A \, \!}
NE:B{\ displaystyle N: B \, \!}![{\ displaystyle N: B \, \!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/4645722c384366ade347eb9b2788a9ce4ad37bcf)
Pokud jde o vyjmenovaných typů, to může být prokázáno, že pouze uzavřené termíny v normální formě typu jsou tvaru , kde a jsou uzavřeny výrazy v normální formě typu a , v tomto pořadí. Odpovídající projekční funkce jsou dány vztahem
NA×B{\ displaystyle A \ krát B}
⟨M;NE⟩{\ displaystyle \ langle M; N \ rangle}
M{\ displaystyle M}
NE{\ displaystyle N}
NA{\ displaystyle A}
B{\ displaystyle B}![B](https://wikimedia.org/api/rest_v1/media/math/render/svg/47136aad860d145f75f3eed3022df827cee94d7a)
- první ≡ Λα,β.λp:(α×β).pα(λX:α.λy:β.X) : ∀α,β(α×β→α){\ displaystyle {\ textbf {fst}} ~ \ equiv ~ \ Lambda \ alfa, \ beta \ ,. \, \ lambda p \, {:} \, (\ alfa \ krát \ beta) \ ,. \, p \, \ alpha \, (\ lambda x \, {:} \, \ alpha \ ,. \, \ lambda y \, {:} \, \ beta \ ,. \, x) ~: ~ \ forall \ alpha , \ beta \, (\ alfa \ krát \ beta \ až \ alfa)}
![{\ displaystyle {\ textbf {fst}} ~ \ equiv ~ \ Lambda \ alfa, \ beta \ ,. \, \ lambda p \, {:} \, (\ alfa \ krát \ beta) \ ,. \, p \, \ alpha \, (\ lambda x \, {:} \, \ alpha \ ,. \, \ lambda y \, {:} \, \ beta \ ,. \, x) ~: ~ \ forall \ alpha , \ beta \, (\ alfa \ krát \ beta \ až \ alfa)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/5a94df198b0fa0e6dbc01855c25a201ce6f4c72a)
- snd ≡ Λα,β.λp:(α×β).pβ(λX:α.λy:β.y) : ∀α,β(α×β→β){\ displaystyle {\ textbf {snd}} ~ \ equiv ~ \ Lambda \ alfa, \ beta \ ,. \, \ lambda p \, {:} \, (\ alfa \ krát \ beta) \ ,. \, p \, \ beta \, (\ lambda x \, {:} \, \ alpha \ ,. \, \ lambda y \, {:} \, \ beta \ ,. \, y) ~: ~ \ forall \ alpha , \ beta \, (\ alpha \ times \ beta \ to \ beta)}
![{\ displaystyle {\ textbf {snd}} ~ \ equiv ~ \ Lambda \ alfa, \ beta \ ,. \, \ lambda p \, {:} \, (\ alfa \ krát \ beta) \ ,. \, p \, \ beta \, (\ lambda x \, {:} \, \ alpha \ ,. \, \ lambda y \, {:} \, \ beta \ ,. \, y) ~: ~ \ forall \ alpha , \ beta \, (\ alpha \ times \ beta \ to \ beta)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/81d99667caa2481463b8e60d55c28006206509e9)
Tyto funkce přirozeně kontrolují rovnosti
a .
prvníNAB⟨M;NE⟩=M{\ displaystyle {\ textbf {fst}} \, A \, B \, \ langle M; N \ rangle = M}
sndNAB⟨M;NE⟩=NE{\ displaystyle {\ textbf {snd}} \, A \, B \, \ langle M; N \ rangle = N}![{\ displaystyle {\ textbf {snd}} \, A \, B \, \ langle M; N \ rangle = N}](https://wikimedia.org/api/rest_v1/media/math/render/svg/da07e72566eae791bd34ed7d40ef227c2c1aeb80)
Přímý součet je definován
NA+B{\ displaystyle A + B}![A + B](https://wikimedia.org/api/rest_v1/media/math/render/svg/4279cdbd3cb8ec4c3423065d9a7d83a82cfc89e3)
- NA+B ≡ ∀y((NA→y)→(B→y)→y){\ displaystyle A + B ~ \ equiv ~ \ forall \ gamma \, ((A \ to \ gamma) \ to (B \ to \ gamma) \ to \ gamma)}
![{\ displaystyle A + B ~ \ equiv ~ \ forall \ gamma \, ((A \ to \ gamma) \ to (B \ to \ gamma) \ to \ gamma)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/0b804a61fa7ef3b7eb0987ef9c8e2c9dbd260a54)
Obyvatelé typů a jsou ponořeni do typu pomocí staveb
NA{\ displaystyle A}
B{\ displaystyle B}
NA+B{\ displaystyle A + B}![A + B](https://wikimedia.org/api/rest_v1/media/math/render/svg/4279cdbd3cb8ec4c3423065d9a7d83a82cfc89e3)
-
inl(M) ≡ Λy.λF:(NA→y).λG:(B→y).FM : NA+B{\ displaystyle {\ textbf {inl}} (M) ~ \ equiv ~ \ Lambda \ gamma \ ,. \, \ lambda f \, {:} \, (A \ na \ gamma) \ ,. \, \ lambda g \, {:} \, (B \ až \ gamma) \ ,. \, f \, M ~: ~ A + B}
(pokud )M:NA{\ displaystyle M: A \, \!}![{\ displaystyle M: A \, \!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/0c21e1ca9d4f46d24a0feb1999745d9111484a62)
-
inr(M) ≡ Λy.λF:(NA→y).λG:(B→y).GM : NA+B{\ displaystyle {\ textbf {inr}} (M) ~ \ equiv ~ \ Lambda \ gamma \ ,. \, \ lambda f \, {:} \, (A \ na \ gamma) \ ,. \, \ lambda g \, {:} \, (B \ až \ gamma) \ ,. \, g \, M ~: ~ A + B}
(pokud )M:B{\ displaystyle M: B \, \!}![{\ displaystyle M: B \, \!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/2f8b3ae68a506a8ef8bf2c29314fbc071ad913fe)
zatímco filtrování prvků typu zajišťuje konstrukce
NA+B{\ displaystyle A + B}![A + B](https://wikimedia.org/api/rest_v1/media/math/render/svg/4279cdbd3cb8ec4c3423065d9a7d83a82cfc89e3)
- zápas NE s inl(X)↦M1 | inr(y)↦M2 ≡ NEVS(λX:NA.M1)(λy:B.M2){\ displaystyle {\ texttt {match}} ~ N ~ {\ texttt {with}} ~ {\ textbf {inl}} (x) \ mapsto M_ {1} ~ | ~ {\ textbf {inr}} (y) \ mapsto M_ {2} ~ \ equiv ~ N \, C \, (\ lambda x \, {:} \, A \ ,. \, M_ {1}) \, (\ lambda y \, {:} \ , B \ ,. \, M_ {2})}
![{\ displaystyle {\ texttt {match}} ~ N ~ {\ texttt {with}} ~ {\ textbf {inl}} (x) \ mapsto M_ {1} ~ | ~ {\ textbf {inr}} (y) \ mapsto M_ {2} ~ \ equiv ~ N \, C \, (\ lambda x \, {:} \, A \ ,. \, M_ {1}) \, (\ lambda y \, {:} \ , B \ ,. \, M_ {2})}](https://wikimedia.org/api/rest_v1/media/math/render/svg/c4bc94ceb5e738ecf479bd318b9a6d56fe68acaf)
který splňuje očekávanou definiční rovnost.
Na rozdíl od kartézského součinu kódování přímého součtu v systému F ne vždy vystihuje pojem disjunktního sjednocení, pokud je v určitých případech možné konstruovat uzavřené termíny v normální formě typu, který není ani z formy (s ) ani formy (s ) .
NA+B{\ displaystyle A + B}
inl(M){\ displaystyle {\ textbf {inl}} (M)}
M:NA{\ displaystyle M: A}
inr(M){\ displaystyle {\ textbf {inr}} (M)}
M:B{\ displaystyle M: B}![{\ displaystyle M: B}](https://wikimedia.org/api/rest_v1/media/math/render/svg/943c98785e1332a55a1484d8c4ca7ca86de9b166)
Celá čísla kostela
Typ církevních celých čísel je definován v systému F pomocí
- NEnat ≡ ∀y(y→(y→y)→y){\ displaystyle \ mathbf {Nat} ~ \ equiv ~ \ forall \ gamma \, (\ gamma \ to (\ gamma \ to \ gamma) \ to \ gamma)}
![{\ displaystyle \ mathbf {Nat} ~ \ equiv ~ \ forall \ gamma \, (\ gamma \ to (\ gamma \ to \ gamma) \ to \ gamma)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/4e0fd65efd0111cb1521fefe26fd137e2327f927)
Každé přirozené číslo je představováno výrazem
ne{\ displaystyle n}![ne](https://wikimedia.org/api/rest_v1/media/math/render/svg/a601995d55609f2d9f5e233e36fbe9ea26011b3b)
- ne¯ ≡ ΛyλX:y.λF:(y→y).F(⋯(F⏟neX)⋯) : NEnat{\ displaystyle {\ bar {n}} ~ \ equiv ~ \ Lambda \ gamma \, \ lambda x \, {:} \, \ gamma \ ,. \, \ lambda f \, {:} \, (\ gamma \ to \ gamma) \ ,. \, \ underbrace {f (\ cdots (f} _ {n} \, x) \ cdots) ~: ~ \ mathbf {Nat}}
![{\ displaystyle {\ bar {n}} ~ \ equiv ~ \ Lambda \ gamma \, \ lambda x \, {:} \, \ gamma \ ,. \, \ lambda f \, {:} \, (\ gamma \ to \ gamma) \ ,. \, \ underbrace {f (\ cdots (f} _ {n} \, x) \ cdots) ~: ~ \ mathbf {Nat}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/c53c9661fcec3743bc055d8d5c20f2932755a087)
Pokud jde o booleovské hodnoty, typ zachycuje pojem přirozené celé číslo, protože jakýkoli uzavřený člen typu v normální formě má formu pro určité přirozené celé číslo .
NEnat{\ displaystyle \ mathbf {Nat}}
NEnat{\ displaystyle \ mathbf {Nat}}
ne¯{\ displaystyle {\ bar {n}}}
ne{\ displaystyle n}![ne](https://wikimedia.org/api/rest_v1/media/math/render/svg/a601995d55609f2d9f5e233e36fbe9ea26011b3b)
Prezentace v kari
Funkce mazání
- |X|=X{\ displaystyle | x | = x}
![{\ displaystyle | x | = x}](https://wikimedia.org/api/rest_v1/media/math/render/svg/55d2c1e557cc3eedc06f8cc736efca5add7066dc)
- |λX:NA.M|=λX.|M|{\ displaystyle | \ lambda x: AM | = \ lambda x. | M |}
![{\ displaystyle | \ lambda x: AM | = \ lambda x. | M |}](https://wikimedia.org/api/rest_v1/media/math/render/svg/7f478c2f6432628ed11b0f70b5fa3d810ffe4af1)
- |MNE|=|M||NE|{\ displaystyle | MN | = | M || N |}
![{\ displaystyle | MN | = | M || N |}](https://wikimedia.org/api/rest_v1/media/math/render/svg/f2f1f66fcf481d0ecc6067fbe861f77dadf8cb1a)
- |Λα.M|=|M|{\ displaystyle | \ Lambda \ alpha .M | = | M |}
![{\ displaystyle | \ Lambda \ alpha .M | = | M |}](https://wikimedia.org/api/rest_v1/media/math/render/svg/a12d8c090ef916a052af24873a6028f03400d943)
- |MNA|=|M|{\ displaystyle | MA | = | M |}
![{\ displaystyle | MA | = | M |}](https://wikimedia.org/api/rest_v1/media/math/render/svg/739490a0a2d482cef77d0505f7a87ee1c73b1b6c)
Typový systém
- ( Axiom ) pokudΓ⊢X:NA{\ displaystyle {\ frac {} {\ Gamma \ vdash x: A}}}
(X:NA)∈Γ{\ displaystyle (x: A) \ v \ Gamma}
- ( -intro )→{\ displaystyle \ to}
Γ,X:NA⊢M:BΓ⊢λX.M:NA→B{\ displaystyle {\ frac {\ Gamma, x: A \ vdash M: B} {\ Gamma \ vdash \ lambda xM: A \ až B}}}
- ( -elim )→{\ displaystyle \ to}
Γ⊢M:NA→BΓ⊢NE:NAΓ⊢MNE:B{\ displaystyle {\ frac {\ Gamma \ vdash M: A \ až B \ quad \ Gamma \ vdash N: A} {\ Gamma \ vdash MN: B}}}
- ( -intro ), pokud nemá volný výskyt v∀{\ displaystyle \ forall}
Γ⊢M:BΓ⊢M:∀α B{\ displaystyle {\ frac {\ Gamma \ vdash M: B} {\ Gamma \ vdash M: \ forall \ alpha ~ B}}}
α{\ displaystyle \ alpha}
Γ{\ displaystyle \ Gamma}
- ( -elim ) .∀{\ displaystyle \ forall}
Γ⊢M:∀α BΓ⊢M:B{α: =NA}{\ displaystyle {\ frac {\ Gamma \ vdash M: \ forall \ alpha ~ B} {\ Gamma \ vdash M: B \ {\ alpha: = A \}}}}![{\ displaystyle {\ frac {\ Gamma \ vdash M: \ forall \ alpha ~ B} {\ Gamma \ vdash M: B \ {\ alpha: = A \}}}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/6c985c1d6f81d93a371d63abc8cc3f69b8f14a98)
Rovnocennost mezi těmito dvěma systémy
Silná normalizační věta
Typovatelné výrazy systému F jsou silně normalizovatelné , jinými slovy redukce výrazů je operace, která vždy končí vytvořením normální formy.
Korespondence s logikou druhého řádu
Prostřednictvím korespondence Curry-Howard odpovídá systém F velmi přesně minimální logice druhého řádu , jejíž vzorce jsou konstruovány z výrokových proměnných pomocí implikace a výrokové kvantifikace:
NA,B : = α | NA⇒B | ∀αB{\ displaystyle A, B ~~: = ~~ \ alpha ~~ | ~~ A \ Rightarrow B ~~ | ~~ \ forall \ alpha \, B}
Připomeňme, že v tomto rámci jsou jednotky (pravda) a (absurdita), spojky (negace), (konjunkce) a (disjunkce) a existenční kvantifikace definovatelné
⊤{\ displaystyle \ top}
⊥{\ displaystyle \ bot}
¬{\ displaystyle \ lnot}
∧{\ displaystyle \ land}
∨{\ displaystyle \ lor}
∃αB(α){\ displaystyle \ existuje \ alpha \, B (\ alpha)}![{\ displaystyle \ existuje \ alpha \, B (\ alpha)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/3cbf9e56a77e69ff6571cee078b9acccdcd91222)
- ⊤ ≡ ∀y(y⇒y){\ Displaystyle \ top ~ \ equiv ~ \ forall \ gamma \, (\ gamma \ Rightarrow \ gamma)}
![{\ Displaystyle \ top ~ \ equiv ~ \ forall \ gamma \, (\ gamma \ Rightarrow \ gamma)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/a176b45b537b5d7285b527219f58511975bd0c55)
- ⊥ ≡ ∀yy{\ Displaystyle \ bot ~ \ equiv ~ \ forall \ gamma \, \ gamma}
![{\ Displaystyle \ bot ~ \ equiv ~ \ forall \ gamma \, \ gamma}](https://wikimedia.org/api/rest_v1/media/math/render/svg/dfc4f489392a77becd46f5b66d9b42e9b8ed1461)
- ¬NA ≡ NA⇒⊥{\ displaystyle \ lnot A ~ \ equiv ~ A \ Rightarrow \ bot}
![{\ displaystyle \ lnot A ~ \ equiv ~ A \ Rightarrow \ bot}](https://wikimedia.org/api/rest_v1/media/math/render/svg/5725b9f639130f49606ea44d27bd4c2c5926b938)
- NA∧B ≡ ∀y((NA⇒B⇒y)⇒y){\ displaystyle A \ land B ~ \ equiv ~ \ forall \ gamma \, ((A \ Rightarrow B \ Rightarrow \ gamma) \ Rightarrow \ gamma)}
![{\ displaystyle A \ land B ~ \ equiv ~ \ forall \ gamma \, ((A \ Rightarrow B \ Rightarrow \ gamma) \ Rightarrow \ gamma)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/26637341a2165e1fc326fbe3fb3734712dc53b70)
- NA∨B ≡ ∀y((NA⇒y)⇒(B⇒y)⇒y){\ displaystyle A \ lor B ~ \ equiv ~ \ forall \ gamma \, ((A \ Rightarrow \ gamma) \ Rightarrow (B \ Rightarrow \ gamma) \ Rightarrow \ gamma)}
![{\ displaystyle A \ lor B ~ \ equiv ~ \ forall \ gamma \, ((A \ Rightarrow \ gamma) \ Rightarrow (B \ Rightarrow \ gamma) \ Rightarrow \ gamma)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/ca4c853d062ad34d1d75004718f8c8c13b424695)
- ∃αB(α) ≡ ∀y(∀α(B(α)⇒y)⇒y){\ displaystyle \ existuje \ alpha \, B (\ alpha) ~ \ equiv ~ \ forall \ gamma \, (\ forall \ alpha \, (B (\ alpha) \ Rightarrow \ gamma) \ Rightarrow \ gamma)}
![{\ displaystyle \ existuje \ alpha \, B (\ alpha) ~ \ equiv ~ \ forall \ gamma \, (\ forall \ alpha \, (B (\ alpha) \ Rightarrow \ gamma) \ Rightarrow \ gamma)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/ea9910787f38b7e240d6233682e64cba0de35555)
(Všimněte si, že prostřednictvím Curryho-Howardovy korespondence absurdita odpovídá prázdnému typu, pravda singletonovému typu, spojení s kartézským součinem a disjunkce s přímým součtem.)
Dokazujeme, že v tomto formalismu je vzorec prokazatelný bez hypotéz právě tehdy, když je odpovídající typ v systému F obýván uzavřeným termínem.
Korespondence s aritmetikou druhého řádu
Bibliografie
-
Lambda-kalkul, typy a modely , Jean-Louis Krivine , kapitola VIII, Masson , 1990, ( ISBN 2-225-82091-0 )
-
Důkazy a typy ,Jean-Yves Girard, Paul Taylor, Yves Lafont, kapitola 11,Cambridge University Press, 1989, ( ISBN 0-521-37181-3 )
<img src="https://fr.wikipedia.org/wiki/Special:CentralAutoLogin/start?type=1x1" alt="" title="" width="1" height="1" style="border: none; position: absolute;">