Práctica 3 (Paradigmas)

Gramáticas a tener en cuenta:

Términos anotados

   M ::= x | λx: σ.M | M M | True | False | if M then M else M | 0 | succ(M) | pred(M) | isZero(M) Donde
   la letra x representa un nombre de variable arbitrario. Tales nombres se toman de un conjunto in�nito
   dado X = {w, w1, w2, . . . , x, x1, x2, . . . , y, y1, y2, . . . , f, f1, f2, . . . }

Términos sin anotaciones

   M0 ::= x | λx.M0 | M0 M0 | True | False | if M0 then M0 else M0 | 0 | succ(M0) | pred(M0) | isZero(M0)

Tipos

   σ ::= Bool | Nat | σ → σ | s
   Donde la letra s representa una variable de tipos arbitraria. Tales nombres se toman de un conjunto in�nito
   dado T = {s, s1, s2, . . . , t, t1, t2, . . . , a, b, c, . . . }

Ejercicio 1

Determinar qué expresiones son sintácticamente válidas y, para las que sean, indicar a qué gramática pertenecen.

i. λx: Bool.succ(x) -- Válida, grámatica con anotaciones.

ii. λx.isZero(x) -- Válida, grámatica sin anotaciones.

iii. s → σ -- No Válida. σ es una metavariable.

iv. Erase(f y) Válida, grámatica sin anotaciones.

v. s -- Válida, grámatica de tipos.

vi. s → (Bool → t) -- Válida, grámatica de tipos.

vii. λx: s1 → s2.if 0 then True else 0 succ(True) -- No Válida.

viii. Erase(λf : Bool → s.λy : Bool.f y) -- Válida, grámatica con anotaciones.

Ejercicio 2

Determinar el resultado de aplicar la sustitución S a las siguientes expresiones

i. S = {t ← Nat} S({x : t → Bool})

  S({x : Nat → Bool})

ii. S = {t1 ← t2 → t3, t ← Bool} S({x : t → Bool}) . S(λx: t1 → Bool.x): S(Nat → t2)

  S({x : Bool → Bool}) . S(λx: t2 → t → Bool.x): S(Nat → t2)