a) x
b) x x
✅ Expresiones sintácticamente válidas, son términos.
c) M
d) M M
❌ No son expresiones sintácticamente válidas. M representa un término cualquiera en la gramática pero no es un término en si mismo.
e) true false
f) true succ(false true)
✅ Expresiones sintácticamente válidas, son términos (pero no tipan).
g) λx.isZero(x)
❌ No es una expresión sintácticamente válida, falta el tipo de la variable x.
h) λx: σ. succ(x)
❌ No es una expresión sintácticamente válida. σ denota un tipo cualquiera, pero no es una expresión de tipo en sí mismo.
i) λx: Bool. succ(x)
✅ Expresión sintácticamente válida, es un término (pero no tipa).
j) λx: if true then Bool else Nat. x
❌ No es una expresión sintácticamente válida, en las ramas del if deben aparecer términos, y ni Bool ni Nat son términos (son tipos).
k) σ
❌ No es una expresión sintácticamente válida por la misma razón que el inciso h).
l) Bool
m) Bool → Bool
n) Bool → Bool → Nat
✅ Expresiones sintácticamente válidas, son expresiones de tipo.
ñ) (Bool → Bool) → Nat
✅ Expresión sintácticamente válida, es una expresión de tipo. Los paréntesis modifican la asociatividad por defecto de → (es igual al tipado de funciones de Haskell, asocia a derecha).
o) succ true
❌ No es una expresión sintácticamente válida, faltan los paréntesis del constructor succ.
p) λx: Bool. if 0 then true else 0 succ(true)
✅ Expresión sintácticamente válida, es un término (pero no tipa).