R8
De Razonamiento automático (2018-19)
Revisión del 10:02 9 feb 2019 de Jalonso (discusión | contribuciones) (Página creada con «<source lang="isabelle"> chapter {* R8: Gramáticas libres de contexto *} theory R8_Gramaticas_libre_de_contexto imports Main begin text {* En esta relación se definen…»)
chapter {* R8: Gramáticas libres de contexto *}
theory R8_Gramaticas_libre_de_contexto
imports Main
begin
text {*
En esta relación se definen dos gramáticas libres de contexto y se
demuestra que son equivalentes. Además, se define por recursión una
función para reconocer las palabras de la gramática y se demuestra que
es correcta y completa. *}
text {*
---------------------------------------------------------------------
Ejercicio 1. Una gramática libre de contexto para las expresiones
parentizadas es
S ⟶ ε | '(' S ')' | SS
definir inductivamente la gramática S usando A y B para '(' y ')',
respectivamente.
------------------------------------------------------------------ *}
datatype alfabeto = A | B
inductive_set S :: "alfabeto list set" where
S1: "[] ∈ S"
| S2: "w ∈ S ⟹ [A] @ w @ [B] ∈ S"
| S3: "v ∈ S ⟹ w ∈ S ⟹ v @ w ∈ S"
text {*
---------------------------------------------------------------------
Ejercicio 2. Otra gramática libre de contexto para las expresiones
parentizadas es
T ⟶ ε | T '(' T ')'
definir inductivamente la gramática T usando A y B para '(' y ')',
respectivamente.
------------------------------------------------------------------ *}
inductive_set T :: "alfabeto list set" where
T1: "[] ∈ T"
| T2: "v ∈ T ⟹ w ∈ T ⟹ v @ [A] @ w @ [B] ∈ T"
text {*
---------------------------------------------------------------------
Ejercicio 3. Demostrar que T está contenido en S.
------------------------------------------------------------------ *}
lemma T_en_S:
assumes "w ∈ T"
shows "w ∈ S"
oops
text {*
---------------------------------------------------------------------
Ejercicio 4. Demostrar que S está contenido en T.
------------------------------------------------------------------ *}
lemma S_en_T:
"w ∈ S ⟹ w ∈ T"
oops
text {*
---------------------------------------------------------------------
Ejercicio 4. Demostrar que S y T son iguales.
------------------------------------------------------------------ *}
lemma S_igual_T:
"S = T"
oops
text {*
---------------------------------------------------------------------
Ejercicio 5. En lugar de una gramática, se puede usar el siguiente
procedimiento para determinar si la cadena es una sucesión de
paréntesis bien balanceada: se recorre la cadena de izquierda a
derecha contando cuántos paréntesis de necesitan para que esté bien
balanceada. Si el contador al final de la cadena es 0, la cadena está
bien balanceada.
Definir la función
balanceada :: alfabeto list ⇒ bool
tal que (balanceada w) se verifica si w está bien balanceada. Por
ejemplo,
balanceada [A,A,B,B] = True
balanceada [A,B,A,B] = True
balanceada [A,B,B,A] = False
Indicación: Definir balanceada usando la función auxiliar
balanceada_aux :: alfabeto list ⇒ nat ⇒ bool
tal que (balanceada_aux w 0) se verifica si w está bien balanceada.
------------------------------------------------------------------ *}
fun balanceada :: "alfabeto list ⇒ bool" where
"balanceada w = undefined"
text {*
---------------------------------------------------------------------
Ejercicio 6. Demostrar que balanceada es un reconocedor correcto de la
gramática S; es decir,
w ∈ S ⟹ balanceada w
------------------------------------------------------------------ *}
lemma balanceada_correcto:
"w ∈ S ⟹ balanceada w"
oops
text {*
---------------------------------------------------------------------
Ejercicio 7. Demostrar que balanceada es un reconocedor completo de
la gramática S; es decir,
balanceada w ⟹ w ∈ S
------------------------------------------------------------------ *}
lemma balanceada_completo:
assumes "balanceada w"
shows "w ∈ S"
oops
end