交互几何

交互几何（GoI）是由Jean-YvesGirard在其线性逻辑工作后不久提出的。在线性逻辑中，证明可以被看作是各种网络，与序列微积分的扁平树状结构相对应。为了将真正的证明网与所有可能的网络区分开来，吉拉德设计了一个涉及网络中的跳动的标准。行程实际上可以被看作是作用于证明的某种运算符。根据这一观察，吉拉德从证明中直接描述了这一算子，并给出了一个公式，即所谓的执行公式，在算子的层面上编码了切割消除的过程。GoI最早的重要应用之一是更好地分析了Lamping对λ微积分的最优还原算法。

GoI对线性逻辑和PCF的博弈语义学有很大影响。GoI已被应用于λ计算的深度编译器优化。被称为”合成几何”的GoI的有界版本已被用于将高阶编程语言直接编译为静态电路。