🔄 Syntax jazyka
Symboly a ich význam
| 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 |
| [ ] | Typová aplikácia | t [T] |
🎯 Ako používať editor
1. Zadávanie kódu
Formát: Najprv definície (TYPE/DEF), potom hlavný výraz
# Definície typov a funkcií
TYPE bool = ∀A. A → A → A
DEF true : bool = ΛA.λx:A.λy:A.x
DEF not : bool → bool = λb:bool.ΛA.λx:A.λy:A.b [A] y x
# Hlavný výraz
(λx:bool → bool. x) @not @true
Alebo priamo výraz bez definícií
# Jednoduchý výraz bez definícií
(λx:Bool. x) true
2. Rýchle vkladanie symbolov
- Použite paletu symbolov pod editorom
- Alebo píšte LaTeX príkazy:
\lambda, \to, \forall
- Auto-complete: napíšte
\ a potom názov symbolu
🏗️ Typový systém System F
Typové pravidlá
| Pravidlo | Formálne | Význam |
|---|
| T-Var | Γ ⊢ x : T | Premenná má typ z kontextu |
| T-Abs | Γ, x:T ⊢ t : U
Γ ⊢ λx:T.t : T→U | Lambda abstrakcia |
| T-App | Γ ⊢ t : T→U, Γ ⊢ u : T
Γ ⊢ t u : U | Aplikácia funkcie |
| T-TAbs | Γ ⊢ t : T
Γ ⊢ ΛA.t : ∀A.T | Typová abstrakcia |
| T-TApp | Γ ⊢ t : ∀A.T
Γ ⊢ t [U] : T[U/A] | Typová aplikácia |
⚙️ Funkcie editora
| 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 |