2010-05-07から1日間の記事一覧

Isabelle Tutorial その21

7.4 Case Study: A Context Free Grammer ここでは、HopcroftとUllmanによる文脈自由文法の例*1を取り上げます。生成規則は次のようになっており、これはaとbの数が同じ文字列を生成します。 まず、アルファベットを定義します。 datatype alpha = a | b 便…