繰り返しx*と強い繰り返しx+、長谷川の不動点補題

正規表現において、x* と x+ のどっちを基礎においてもかまわない。

• x* = 1 + x+
• x+ = (x*)x

トレースを使ったスターの定義 Tr(∇;f;Δ) は、どちらかというと+の定義だと思ったほうがいいような気がしてきた。絵を見てもx+の絵だし、次の等式が状況証拠：

• x+ = (1 + x+)x

この等式の両辺に1を足せば：

• x* = 1 + (x*)x

となって、通常の不動点方程式となる。ところが、x+ = (1 + x+)x は、次のトレースに関する公式から出るのだ。

• Tr(f) = <A, Tr(f;π²_B,X;Δ_X)>;f;π¹_B,X

プログラミングでは、whileとdo-whileの違いだが、do-whileから公理化するアプローチも別に悪い点はない。

もし、Tr'(f) = <A, Tr(f;π²_B,X;Δ_X)> とするなら、Tr':(A,X →B, X)→(A→A,X) だが、このTr'のほうが*に近い存在だろう。先に出したトレースの公式は、長谷川さんが彼の定理（カザネスク／ステファネスク／ハイランド／長谷川）の補題として使っている。けっこうキモな公式だから、長谷川の不動点補題と呼んでおこう。