デカルト閉圏は計算(computations)のモデルとして大変に使いやすいものです。しかし、どうもデカルト閉圏が矮小化されて理解され、応用範囲を狭めているような印象も持ちます。デカルト閉圏が型付きラムダ計算のモデルであるのは事実ですが、このことが強調されすぎて、デカルト閉圏は「型付きラムダ計算にしか適用できない」という誤解があるのかもしれません。 静的に強く型付けされるプログラミング言語処理系は、デカルト閉圏でうまくモデル化できます。いま、「プログラミング言語」ではなくて、「プログラミング言語処理系」と言ったのに注意してください。プログラミング言語の構文に意味を付与する話ではなくて、コンパイラやランタイムを含んだメカニズム全体の定式化にもデカルト閉圏が使えます。 デカルト閉圏とプログラミング言語処理系 デカルト閉圏の特徴は、C(A×B, C) = C(A, [B, C]) という同型があ