Väzba let a súčinové typy

Majme daný nasledujúci term: $$let\ x = t_1\ in\ t_2:Nat,$$ kde: $$ \begin{array}{l} t_1 = and\ true\ false \\ t_2 = if\ x\ then\ succ\ 0\ else\ succ\ (succ\ 0) \end{array} $$ a $$\Gamma = \{and: Bool \to Bool \to Bool \}$$

1. Overte či je správne typovaný v typovom kontexte $\Gamma$.
2. Ak je term správne typovaný, vyhodnoťte ho.

Majme daný nasledujúci term: $$ \langle\ pred\ 3, if\ iszero\ 0\ then\ succ\ 0\ else\ succ\ (succ\ 0)\ \rangle.1 $$

1. Overte či je správne typovaný v prázdnom typovom kontexte.
2. Vyhodnoťte ho (ak je správne typovaný).

Majme daný nasledujúci term: $$ (\lambda x: Nat \times Nat. x.2)\ \ \langle\ pred\ 3, if\ iszero\ 0\ then\ succ\ 0\ else\ succ\ (succ\ 0)\ \rangle : Nat $$

1. Overte či je správne typovaný v prázdnom typovom kontexte.
2. Vyhodnoťte ho (ak je správne typovaný).

1. Definujte typ súradnica. ktorý bude pozostávať z bodov $x$ a $y$.
2. Definujte typ obdĺžnik, ktorý bude definovaný jeho uhlopriečkou.
3. Napíšte funkcie, ktoré vrátia obsah obdĺžnika (v prípade potreby definujte pomocné funkcie).
4. Definujte term typu obdĺžnik.
5. Aplikujte funkciu pre výpočet obsahu z bodu 3. na term z bodu 4 a následne:
   • overte či je takýto term správne typovaný,
   • ak áno, vyhodnoťte ho.

1. Definujte záznamový typ "Kniha", ktorý bude obsahovať položky:
   • autor,
   • titul,
   • cena.
2. Napíšte funkcie, ktoré vrátia autora, titul a cenu.
3. Definujte 3 termy typu kniha.
4. Aplikujte funkcie z kroku 2. na termy z kroku 3.
5. Definujte typ záznam pre zoznam troch kníh.
6. Definujte term typu zoznam troch kníh využitím termov z kroku 3.
7. Napíšte funkciu, ktorá vráti najlacnejšiu knihu zo zoznamu.
8. Aplikujte funkciu z kroku 7. na term z kroku 6.