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.