(*
$Id: ex.thy,v 1.3 2012/01/04 13:40:21 webertj Exp $
Author: Tobias Nipkow
*)
header {* Context-Free Grammars *}
(*<*) theory ex imports Main begin (*>*)
text {* This exercise is concerned with context-free grammars (CFGs).
Please read Section~7.4 in the tutorial which explains how to model
CFGs as inductive definitions. Our particular example is about
defining valid sequences of parentheses. *}
subsection {* Two grammars *}
text {* The most natural definition of valid sequences of parentheses is this:
\[ S \quad\to\quad \varepsilon \quad\mid\quad '('~S~')' \quad\mid\quad S~S \]
where $\varepsilon$ is the empty word.
A second, somewhat unusual grammar is the following one:
\[ T \quad\to\quad \varepsilon \quad\mid\quad T~'('~T~')' \]
Model both grammars as inductive sets $S$ and $T$ and prove $S = T$. *}
subsection {* A recursive function *}
text {* Instead of a grammar, we can also define valid sequences of
parentheses via a test function: traverse the word from left to right
while counting how many closing parentheses are still needed. If the
counter is 0 at the end, the sequence is valid.
Define this recursive function and prove that a word is in $S$ iff it
is accepted by your function. The $\Longrightarrow$ direction is easy,
the other direction more complicated. *}
(*<*) end (*>*)