Typovaný NBL a Jednoducho typovaný $\lambda$-kalkul

Majme dané nasledujúce termy: $$ \begin{array}{lcl} t_1 & = & if\ iszero\ 0\ then\ true\ else\ false: Bool \\ t_2 & = & if\ iszero\ (pred\ (succ\ 0))\ then\ true\ else\ false: Bool \\ t_3 & = & succ(\ if\ iszero\ (succ\ (succ\ 0))\ then\ false\ else\ (pred\ (succ\ (succ\ 0)))): Nat \\ t_4 & = & pred(\ iszero(\ if\ iszero\ (pred\ (succ\ (succ\ (succ\ 0))))\ then\ true\ else\ (succ\ (succ\ 0)))) : Nat \\ t_5 & = & succ(\ if\ iszero\ (succ\ (succ\ (pred\ (succ\ (succ\ (succ\ 0)))))) \\ & & \quad \quad \quad then\ (succ\ (succ\ (pred\ (succ\ 0))))\ else\ (pred\ (succ\ (succ\ 0)))) \\ & & \quad \quad \quad else\ (pred\ (succ\ (succ\ 0)))) :Nat\\ \end{array} $$ Overte či sú správne typované.

Majme daný nasledujúci term: $$\lambda x: A \to B. \lambda y: A.\ x\ y: (A \to B) \to A \to B$$

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

Majme daný nasledujúci term: $$\lambda f: A \to B. \lambda x: A. \lambda y: B.\ f\ x\ (f\ y): (A \to B) \to A \to B \to B$$

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

Majme daný nasledujúci term: $$\lambda x: A. \lambda y: B. \lambda z: C.\ x\ y\ z: A \to B \to C \to C$$

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

Majme daný nasledujúci term: $$\lambda x: Bool. \lambda y: Bool.\ and\ x\ y : Bool \to Bool \to Bool$$

1. Overte či je správne typovaný v typovom kontexte: $$\Gamma = \{and: Bool \to Bool \to Bool \}$$
2. Vyhodnoťte ho pre vhodné argumenty (ak je správne typovaný).

Majme daný nasledujúci term: $$\lambda f: A \to Nat \to B. \lambda x: Nat. \lambda y: A.\ f\ y\ (succ\ x):(A \to Nat \to B)\to Nat \to A \to B $$

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

Majme daný nasledujúci term: $$\lambda f: A \to Bool. \lambda x: A. \lambda y: A.\ if\ b\ x\ then\ b\ y\ else\ false : (A \to Bool) \to A \to A \to Bool $$

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

Majme daný nasledujúci term:

$$ \begin{array}{l} \lambda f: Bool \to Bool \to A. \lambda b: B \to Bool. \lambda x: B. \lambda y: Nat.\\ f\ (if\ b\ x\ then\ iszero\ y\ else\ false)\ true :\\ (Bool \to Bool \to A) \to (B \to Bool) \to B \to Nat \to A \end{array} $$

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