Edición de «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 → t3 → Bool.x): S(Nat → t2)