このブログの更新は Twitterアカウント @m_hiyama で通知されます。
Follow @m_hiyama

メールでのご連絡は hiyama{at}chimaira{dot}org まで。

はじめてのメールはスパムと判定されることがあります。最初は、信頼されているドメインから差し障りのない文面を送っていただけると、スパムと判定されにくいと思います。

参照用 記事

ラムダ期?

間欠的にラムダ計算に対する興味が再燃するのですが、今はその時期かも。Coqを触ったみたのが刺激になったようです。

最近の「型付きラムダ計算のモデルの作り方」、「セマンティック駆動な圏的ラムダ計算とシーケント」と、ラムダ計算の記事が続いてます。その前の「豊饒圏をちゃんと定義したい」も、デカルト閉圏が指数を内部ホムとしての自己豊饒圏になっていることが背景の事情です。

デカルト閉圏より弱い構造の圏でもラムダ計算+シーケント計算をやりたいですね。「セマンティック駆動な圏的ラムダ計算とシーケント」でシーケント計算を定義しましたが、「圏論からシーケント計算へ」でもやはり圏的シーケント計算を定義してます。この2つの定式化は意図的に違ったものにしてますが、これらを比較すれば「使いやすいシーケント計算」とはどんものか? 多少は見当がつくかも知れません。

一方で、ラムダ計算の表現力を強化して、指数を扱えないかな、とか。「セマンティック駆動な圏的ラムダ計算とシーケント」で「指数の計算がほとんど出来ないのです。」と書いたのですが、通常のラムダ計算の構文で指数を扱うのは無理っぽいですね。継続(continuation)を入れて、指数の計算が半分くらい出来るかな、というレベルでしょう。

十分な表現力を持ったラムダ計算なら、飛び先ラベルとgoto文も扱えるでしょう。「goto、大域変数、例外、双対性」でそんな話をしているんですが、「goto文を含むプログラムの意味はベース圏上の前層のなかに棲んでいる、と考えることができます。」と書いているだけで、具体的に記述構文を示したわけじゃないです。

うまい構文があれば「goto付きラムダ計算」ができます。denotational/functionalなgotoプログラムって、頭痛がしそうに素敵じゃないですか。