Jalonso: Protegió «R8» ([Editar=Solo administradores] (indefinido) [Trasladar=Solo administradores] (indefinido))

2019-02-09T08:02:12Z

Protegió «R8» ([Editar=Solo administradores] (indefinido) [Trasladar=Solo administradores] (indefinido))

Jalonso: Página creada con « chapter {* R8: Gramáticas libres de contexto } theory R8_Gramaticas_libre_de_contexto imports Main begin text { En esta relación se definen…»

2019-02-09T08:02:03Z

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…»

Página nueva

<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 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
</source>

← Revisión anterior	Revisión del 08:02 9 feb 2019
(Sin diferencias)

R8 - Historial de revisiones

Jalonso: Protegió «R8» ([Editar=Solo administradores] (indefinido) [Trasladar=Solo administradores] (indefinido))

Jalonso: Página creada con « chapter {* R8: Gramáticas libres de contexto *} theory R8_Gramaticas_libre_de_contexto imports Main begin text {* En esta relación se definen…»

Jalonso: Página creada con « chapter {* R8: Gramáticas libres de contexto } theory R8_Gramaticas_libre_de_contexto imports Main begin text { En esta relación se definen…»