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)