Zadanie

1.) Netypovaný jazyk NBL. (1 príklad)

• Formulácia vzorového termu t.
• Konštruovanie stromu abstraktnej syntaxe.
• Overenie, či term t patrí do jazyka termov NBL.
• Identifikácia konštánt termu t.
• Zistenie veľkosti termu t.
• Výpočet hĺbky stromu abstraktnej syntaxe termu t.
• Vyhodnotenie termu t.

2.) Netypovaný λ-kalkul.

• Doplňte resp. odstráňte čo najviac zátvoriek z termov netypovaného λ-kalkulu. (2 príklady).
  • Vzor: (λx.x z) (λy.w) (λw.w y z x) = ((λx.(x z)) (λy.w)) (λw.(((w y) z) x))
• Vyhodnotenie termov netypovaného λ-kalkulu (beta-redukcia). (2 príklady, aspoň jeden term s využitím alfa-redukcie a minimálne 4 kroky redukcie).
• Vyhodnotiť 3 termy využitím Churchových kombinátorov. (aspoň 1 pre aritmetické operácie, 1 pre booleovské operácie, zároveň definujte aspoň jednu vlastnú funkciu a použite ju vo výpočte).
• Rekurzia v netypovanom λ-kalkule. 1 príklad na rekurzívnu funkciu vypočítanú kombinátorom fixného bodu v netypovanom λ-kalkule (nie faktoriál a sčítanie - príklady z prednášky, resp. cvičenia).

3.) Typovaný jazyk NBL. (1 príklad)

• Formulácia vzorového termu t.
• Overenie, či term t je správne typovaný.
• Vyhodnotenie termu t.

4.) Jednoducho typovaný λ-kalkul.

Jednoducho typovaný λ-kalkul

• Rozšírte množinu základných typov o nový typ.
• Rozšírte syntax $\lambda_\to$ o prvky takéhoto typu.
• Rozšírte syntax $\lambda_\to$ o aspon 3 operácie nad takýmto typom a definujte k ním príslušné typovacie a vyhodnocovacie pravidlá.

Jednoducho typovaný λ-kalkul s NBL.

• Overenie či term t jednoducho typovaného λ-kalkulu s funkčným typom a s NBL je správne typovaný.
• Vyhodnotenie termu t pre argument n.

Jednoducho typovaný λ-kalkul so súčinovým typom.

• Formulácia termu t s využitím binárneho súčinového typu.
• Overenie, či term t je správne typovaný.
• Vyhodnotenie termu t.

Jednoducho typovaný λ-kalkul so súčtovým typom.

• Formulácia termu t s využitím binárneho súčtového typu.
• Overenie, či term t je správne typovaný.
• Vyhodnotenie termu t.

5.) Údajové štruktúry v jednoducho typovanom λ-kalkule.

• Definícia a vzorové riešenie úlohy na údajovú štruktúru záznam.
• Definícia a vzorové riešenie úlohy na údajovú štruktúru variant.
• Definícia a vzorové riešenie úlohy na údajovú štruktúru variant s využitím enumeračného typu.

Pri každej údajovej štruktúre overte, či je formulovaný term t správne typovaný a vyhodnoťte ho.

6.) Odvodené tvary termov jednoducho typovaného λ-kalkulu.

Vymyslieť a vyriešiť po 1 príklad na každý z definovaných odvodených tvarov termov jednoducho typovaného λ-kalkulu:

• Let väzba (let binding).
• Zoradenie (sequencing).
• Zastúpenie (wildcards).
• Pripísanie (ascription).

Následne:

• Overiť typ termu t.
• Vyhodnotiť term t.
• Prepísať term t do základného jazyka λ-kalkulu.

7.) Rekurzia v jednoducho typovanom λ-kalkule.

Rozšírte rekurzívnu funkciu z úlohy 2 pridaním typov.

• Definícia funkcie vyššieho rádu, ktorej parametrom bude daná rekurzívna funkcia.
• Aplikácia operátora $fix$ na funkciu vyššieho rádu.
• Overiť typ termu.
• Vyhodnotiť term.
• Prepísať term t do konštrukcie $let~rec$.

8.) Zoznamy v jednoducho typovanom λ-kalkule.

Zvoľte si jednu z funkcií v knižnici List jazyka OCaml (nie $is\_empty, length, append, cons, hd, tl$), resp. vymyslite si vlastnú funkciu. Nasledne Vašou úlohou je:

• Napísať zvolenú funkciu ako term $t$ nášho jazyka.
• Overte typ $t$.
• Vyhodnotiť $t$ pre ľubovoľný vhodný argument.
• V prípade rekurzívnej definície $t$, prepísať $t$ do konštrukcie $let~rec$.

9.) Rekurzívne typy.

Navrhnite rekurzívny typ na reprezentáciu ľubovoľnej rekurzívnej štruktúry: (napr. prirodzené čísla, binárne stromy, zoznamy, binárne čísla...) či už ako variantový typ alebo ako súčtový typ, a definujte:

• Príslušné hodnoty resp. konštruktory nad nimi.
• Aspoň jednu funkciu nad hodnotami daného typu.
• Aplikujte danú funkciu na ľubovoľnú hodnotu daného typu, overte či je takýto program správne typovaný a ak áno, vyhodnoťte ho.

9.) Typová rekonštrukcia - odvodenie typu.

• Pokúste sa nájsť najvšeobecnejší typ, pre jednu z Vami formulovaných termov z úlohy č. 2 (v prípade rozsiahlej komplexnosti navrhnutých termov, ich môžete zjednodušiť, prípadne upraviť pre potreby tejto úlohy).

10.) Let polymorfizmus.

• Odstrante typové anotácie z termu let väzby z úlohy č.6 a najdite najvšeobecnejší typ daného termu.

Forma odovzdania

Termín pre odovzdanie finálnej verzie zadania je koniec 12. týždňa semestra v systéme moodle v kurze TT.

Odovzdávanie zadania bude prebiehať priebežne, prostredníctvom systému moodle.

• Pre priebežné odovzdávky v 4. 8. a 12. týždni bude vytvorená aktivita na odovzdanie vypracovanej časti zadania.
• V danom týždni je potrebné vypracovať časť zadania, podľa obsahu cvičenia z predchádzajúcich týždňov.
• Zadanie nie je potrebné rozdeliť do viacerých projektov ale priebežne dopĺňať.
• V aktuálnej odovzdávke sú povolené zmeny aj v už odovzdaných častiach zadania.
• Neospravedlnené nedodržanie termínu odovzdávky bude sankcionované stratou 3 bodov.

V 13. týždni semestra prebehne obhajoba zadania.

Zadanie je možné vypracovať dvoma spôsobmi:

• Využitím typografického systému LaTeX (max. 30 bodov).
• Ručne s možnosťou získania max. 20 bodov.

Zadanie v úvodnej časti bude obsahovať titulnú stranu a súhrn rozsahu vyriešených úloh.

• V prípade zvolenia 1. možnosti poprosím vo finálnom odovzdávaní o nahratie vypracovaného zadania spolu so zdrojovými kódmi (2 subory: pdf subor a zip subor), pričom v priebežných odovzdávkach 4. a 8. týždni je potrebné nahrať len pdf súbor.
• V prípade voľby 2. možnosti vás poprosím o odovzdanie zadania vo forme jedného pdf súboru.