Diferencia entre revisiones de «Práctica 3 (Paradigmas)»

De Cuba-Wiki
(Ej 1 resuelto)
 
 
(No se muestran 3 ediciones intermedias de otro usuario)
Línea 6: Línea 6:
     dado X = {w, w1, w2, . . . , x, x1, x2, . . . , y, y1, y2, . . . , f, f1, f2, . . . }
     dado X = {w, w1, w2, . . . , x, x1, x2, . . . , y, y1, y2, . . . , f, f1, f2, . . . }
Términos sin anotaciones
Términos sin anotaciones
     M0
     M0 ::= x | λx.M0 | M0 M0 | True | False | if M0 then M0 else M0 | 0 | succ(M0) | pred(M0) | isZero(M0)
    ::= x | λx.M0
    | M0 M0
    | True | False | if M0
    then M0
    else M0
    | 0 | succ(M0
    ) | pred(M0
    ) | isZero(M0
    )
Tipos
Tipos
     σ ::= Bool | Nat | σ → σ | s
     σ ::= Bool | Nat | σ → σ | s
Línea 23: Línea 14:


== Ejercicio 1 ==
== Ejercicio 1 ==
Determinar qué expresiones son sintácticamente válidas y, para las que sean, indicar a qué gramática pertenecen.
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.
i. λx: Bool.succ(x)  -- Válida, grámatica con anotaciones.
ii. λx.isZero(x)  -- Válida, grámatica sin anotaciones.
ii. λx.isZero(x)  -- Válida, grámatica sin anotaciones.
iii. s → σ  -- No Válida. σ es una metavariable.
iii. s → σ  -- No Válida. σ es una metavariable.
iv. Erase(f y) Válida, grámatica sin anotaciones.
iv. Erase(f y) Válida, grámatica sin anotaciones.
v. s -- Válida, grámatica de tipos.
v. s -- Válida, grámatica de tipos.
vi. s → (Bool → t) -- 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
 
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.
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)

Revisión actual - 22:16 26 sep 2022

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)