Loading article…
証明理論において、相互作用の幾何学(GoI)は、ジャン＝イヴ・ジラールが線状論理の研究の直後に導入した。線状論理では、証明はシーケント計算の平坦な木構造とは対照的に、さまざまな種類のネットワークとして見ることができる。実際の証明ネットをすべての可能なネットワークと区別するために、ジラールはネットワーク内のトリップを含む基準を考案した。トリップは、実際には証明に作用するある種の演算子[明確化が必要]として見ることができる。この観察から、ジラール[1] は証明からこの演算子を直接記述し、演算子レベルでカット除去のプロセスをエンコードする、いわゆる実行式と呼ばれる式を与えた。ジラールによるその後の構築では、証明をフロー[2]またはフォン・ノイマン代数の演算子として表現する変種が提案された。[3]これらのモデルは、後にザイラーの相互作用グラフモデルによって一般化された。[4]
GoIの最初の重要な応用の一つは、ラムダ計算の最適縮約のためのランピングアルゴリズム[6]のより優れた分析[5]でした。GoIは線形論理とPCFのゲームセマンティクスに大きな影響を与えました。
証明の動的解釈を超えて、相互作用の幾何学的構成は線形論理のモデルまたはその断片を提供します。この側面は、線形性を考慮した 実現可能性のバージョンである線形実現可能性という名前でSeiller [7]によって広範に研究されてきました。
GoIはラムダ計算の深層コンパイラ最適化に適用されている。[8] GoIの境界付きバージョンである合成幾何学は、高階プログラミング言語を静的回路に直接コンパイルするために使用されている。 [9]
参考文献
- ^ ジラール、ジャン=イヴ (1989)。「相互作用の幾何学 1: システム F の解釈」。論理と数学の基礎研究。127 : 221–260。
- ^ Girard, Jean-Yves (1995). 「相互作用の幾何学 III: 添加物の調整」.ロンドン数学会講義ノートシリーズ: 329–389.
- ^ Girard, Jean-Yves (2011). 「相互作用の幾何学 V: 超有限因子の論理」理論計算機科学412 ( 20): 1860–1883.
- ^ Seiller, Thomas (2016). 「インタラクショングラフ: 完全線形ロジック」。第31回ACM/IEEEコンピュータサイエンスにおけるロジックシンポジウムの議事録。
- ^ Gonthier, G.; Abadi, MN; Lévy, JJ (1992). 「最適ラムダ縮小の幾何学」。第 19 回 ACM SIGPLAN-SIGACTプログラミング言語の原理に関するシンポジウム議事録- POPL '92。p. 15。doi :10.1145/ 143165.143172。ISBN 0897914538. S2CID 7265545。
- ^ Lamping, J. (1990). 「最適なラムダ計算削減アルゴリズム」。プログラミング言語の原理に関する第 17 回 ACM SIGPLAN-SIGACT シンポジウム議事録 - POPL '90。pp. 16–30。doi :10.1145 / 96709.96711。ISBN 0897913434.S2CID 16333787 。
- ^ ザイラー、トーマス (2024).数理情報学（ハビリテーション論文）。ソルボンヌ大学パリ北校。
- ^ Mackie, I. (1995). 「インタラクションマシンの幾何学」。プログラミング言語の原理に関する第 22 回 ACM SIGPLAN-SIGACT シンポジウム議事録 - POPL '95 。pp . 198–208。doi :10.1145 / 199448.199483。ISBN 0897916921. S2CID 19000897。
- ^ Dan R. Ghica. ハードウェアコンパイルのための関数インターフェイスモデル。MEMOCODE 2011. [1]