Revisión actual |
Tu texto |
Línea 196: |
Línea 196: |
|
| |
|
| f) succ(succ(0)) -------- Es un valor | | f) succ(succ(0)) -------- Es un valor |
|
| |
|
| |
| == Ejercicio 12 (Programa, Forma Normal) ==
| |
| Para el siguiente ejercicio, considerar el cálculo sin la regla pred(0) → 0
| |
|
| |
| Un programa es un término que tipa en el contexto vacío (es decir, no puede contener variables libres).
| |
|
| |
| Para cada una de las siguientes expresiones
| |
|
| |
| a) Determinar si puede ser considerada un programa.
| |
|
| |
| b) Si vale (a), ¾Cuál es el resultado de su evaluación? Determinar si se trata de una forma normal, y en caso
| |
| de serlo, si es un valor o un error.
| |
|
| |
| i (λx: Bool. x) true -- Es un programa, da true
| |
| ii λx: Nat. pred(succ(x)) -- Es un programa, da la identidad
| |
| iii λx: Nat. pred(succ(y)) -- No es un programa, tiene variables libres
| |
| iv (λx: Bool. pred(isZero(x))) true -- Es un programa, da error
| |
| v (λf : Nat → Bool. f 0) (λx: Nat. isZero(x)) -- Es un programa, da true
| |
| vi (λf : Nat → Bool. x) (λx: Nat. isZero(x)) -- No es un programa, tiene variables libres
| |
| vii (λf : Nat → Bool. f pred(0)) (λx: Nat. isZero(x)) -- Es un programa, da error porque se saco pred(0)
| |
| viii fix (λy : Nat. succ(y)) -- Es un programa, da error porque no termina
| |
|
| |
| == Ejercicio 13 (Determinismo) ==
| |
| a) Es cierto que la relación definida → es determinística (o una función parcial)? Más precisamente, pasa que si M → N y M → N`
| |
| entonces N = N` ? -- SI
| |
|
| |
| b) Vale lo mismo con muchos pasos? Es decir, ¾es cierto que si M →→ M` y M →→ M`` entonces M` = M``? -- SI
| |
|
| |
| c) Acaso es cierto que si M → M` y M →→ M`` entonces M` = M``? -- NO
| |
|
| |
| == Ejercicio 14 ==
| |
|
| |
| a) Da lo mismo evaluar succ(pred(M)) que pred(succ(M))? ¾Por qué? -- No, porque pred(succ(0)) = 0 pero succ(pred(0)) = 1
| |
|
| |
| b) Es verdad que para todo M vale que isZero(succ(M)) →→ false? Si no lo es, ¾para qué términos vale? -- Vale para todo M nat
| |
|
| |
| c) Para qué términos M vale que isZero(pred(M)) →→ true? (Hay infinitos). -- Pueden ser combinaciones de pred^n(succ^n(0)) para un n entero.
| |