(2021-05-04) ハンバーガー種の解析

「ハンバーガー種の解析」では、次の四つの記事を解析する。

「ハンバーガー種の解析」では、 \( \Omega \! \! \! \Omega \newcommand{\dprod}[1]{\exists #1 \ldotp \,} \newcommand{\Ha}{H} \newcommand{\Pa}{P} \newcommand{\PL}{P _ {L}} \newcommand{\PM}{P _ {M}} \newcommand{\PR}{P _ {R}} \newcommand{\Me}{M} \newcommand{\Pm}{P _ {m}} \) を使う。

オリョウリ亜種[]

「オリョウリ亜種」では、 Special:Redirect/revision/35952 を参照する。

パンズの例としてパンの ( と ] が示されている。しかし、パンの | はパンズの例として示されていない。

表記[]

ここの数式の中では、ハンバーガーを \( \Ha \) と書く。

ここの数式の中では、パティを \( \Pa \) と書く。

ここの数式の中では、 ( を \( \PL \) と書く。

ここの数式の中では、 | を \( \PM \) と書く。

ここの数式の中では、 ] を \( \PR \) と書く。

ここの数式の中では、肉を \( \Me \) と書く。

ここの数式の中では、パティ素材を \( \Pm \) と書く。

ハンバーガーとパティは相互帰納的に定義される。

ハンバーガーは次のように定義される。

\( x \in P \to \PL x \PR \in \Ha \)
\( s \in \Ha \land t \in \Ha \land s _ {0} \PR = s \land \PL t _ {0} = t \to s _ {0} \PM t _ {0} \in \Ha \)

パティは次のように定義される。

\( \Me \in \Pa \)
\( s \in \Ha \land x \in \Pa \to \Me s x \in \Ha \)

パティ素材は次のように定義される。

\( s \in \Ha \to s \in \Pm \)
\( s \in \Ha \land t \in \Ha \to s \Me t \in \Pm \)

解析[]

まず、ハンバーガーのルール 2 は少々厄介であるから、 EBNF を使用して扱いやすい構文を作成する。

(* Burger burger hexirpii *)
hamburger = "(", patty, { "|", patty } "]";
patty     = "肉", { hamburger, "肉" };

これがオリョウリ亜種のハンバーガーとパティの定義と同値になることは、 \( s \in \Ha \to \dprod{s _ 0} \PL s _ 0 \PR = s \) であることから導かれる。

data Hamburger = Hamburger Patty [Patty]
data Patty = Patty [Hamburger]

Haskell で記述すると上記のようになる。

オッドパティは、ハンバーガーを偶数個含むパティである。

イブンパティは、ハンバーガーを奇数個含むパティである。