Systém F

Symbol	Význam	Príklad
λ	Lambda abstrakcia (term)	λx:T. t
Λ	Typová abstrakcia	ΛA. t
→	Funkčný typ	T → U
∀	Univerzálny kvantifikátor	∀A. T
⊢	Turnstile (oddelenie kontextu)	Γ ⊢ t : T
@	Referencia na definíciu	@not
∈	Patrí do	x:T ∈ Γ
[ ]	Typová aplikácia	t [T]
[ ↦ ]	Substitúcia	[X ↦ A]T

Pravidlo	Formálne	Význam
T-Var	𝑥 : 𝑇 ∈ Γ Γ ⊢ 𝑥 : 𝑇	Premenná má typ z kontextu
T-Abs	Γ, 𝑥 : 𝑇 ⊢ 𝑡 : 𝑈 Γ ⊢ λ𝑥:𝑇. 𝑡 : 𝑇 → 𝑈	Lambda abstrakcia
T-App	Γ ⊢ 𝑡 : 𝑇 → 𝑈 , Γ ⊢ 𝑢 : 𝑇 Γ ⊢ 𝑡 𝑢 : 𝑈	Aplikácia funkcie
T-DefRef	DEF 𝑑 : 𝑇 = 𝑡 ∈ Δ Γ ⊢ @𝑑 : 𝑇	Referencia na definovanú premennú
T-TAbs	Γ, 𝑋 ⊢ 𝑡 : 𝑇 Γ ⊢ Λ𝑋. 𝑡 : ∀𝑋. 𝑇	Typová abstrakcia
T-TApp	Γ ⊢ 𝑡 : ∀𝑋. 𝑇 Γ ⊢ 𝑡[A] : [𝑋 ↦ A]𝑇	Typová aplikácia

Pravidlo	Formálne	Význam
E-App1	𝑡₁ → 𝑡′₁ 𝑡₁ 𝑡₂ → 𝑡′₁ 𝑡₂	Redukcia aplikácie vľavo
E-App2	𝑡₂ → 𝑡′₂ 𝑣₁ 𝑡₂ → 𝑣₁ 𝑡′₂	Redukcia aplikácie vpravo (ak ľavý je hodnota)
E-Abs	(λ𝑥:𝑇. 𝑡) 𝑣 → [𝑥 ↦ 𝑣]𝑡	Beta-redukcia (aplikácia lambda abstrakcie)
E-TApp	𝑡 → 𝑡′ 𝑡[𝑇₁] → 𝑡′[𝑇₁]	Redukcia typovej aplikácie v terme
E-TAbs	(Λ𝑋. 𝑡)[𝑇] → [𝑋 ↦ 𝑇]𝑡	Typová beta-redukcia (aplikácia typovej abstrakcie)
E-DefRef	DEF 𝑑 : 𝑇 = 𝑡 ∈ Δ @𝑑 → 𝑡	Rozvinutie definície

Funkcia	Popis
Syntax kontrola	Realtime kontrola syntaxe
Dôkazový strom	Vizualizácia typovej kontroly
Evaluácia	Redukcia lambda výrazov
Zoom & Pan	Približovanie a posúvanie proof tree
LaTeX export	Export dôkazov do LaTeX
Auto-complete	Automatické dopĺňanie symbolov

Editor Kódu

Symboly:

Nápoveda a Príklady

TYPE bool = ∀A. A → A → A
DEF true : bool = ΛA.λx:A.λy:A.x
DEF false : bool = ΛA.λx:A.λy:A.y

(λx:bool . x) @true

Zadajte kód pre kontrolu syntaxe...