記事「再帰代入系 1」は既にアップロードしました。いま、「その2」を書こうとしています。感触としては、再帰代入系の説明は、「その4」か「その5」くらいまでかかりそうです。
再帰代入系の説明が終われば、僕としてはホッと一安心でしょう。なぜなら、構文的な議論のほとんどは、再帰代入系の性質に依存するからです。BNFのような実例からはじめたほうが説明としては親切でしょうが、背景を説明しきらないと、どうも落ち着かないのです。
再帰代入系(の圏)は、曖昧な形では1995年くらいから漠然と認識してましたが、全体の構造がだいたい分かったのは1999から2000年くらいです(あまり時期を特定できませんが)。しかし、その頃はたぶんうまく説明できなかったでしょう。説明のための適切な言葉を持っていなかったので。
トレース付きモノイド圏(traced monoidal categories)が非常に適切な言葉を提供することを知ったのは、たぶん、ここ2年くらい(?)でしょう。それでやっと、なにをどういう順番で説明すべきかの目星が付いたのです。
再帰代入系の構造を独力で整理するのは無理だったでしょうから、トレース付きモノイド圏を知ったのはラッキーでした。