Classical notions of computation and the Hasegawa-Thielecke theorem
Éléonore Mangel, Paul-André Melliès and Guillaume Munch-Maccagnoni
本着Curry-Howard在证明和程序之间的对应关系的精神,我们定义和研究经典逻辑的语法和语义,该逻辑配备了计算不自主的否定,使用极化效应演算,线性经典L-演算。 为微积分设计一个表示语义的主要挑战是同时适应逐值调用和逐名调用评估策略,这导致组合的关联性失败。 为了解决这个问题,我们定义了非关联类别的图形态之间的辅助概念,我们用它来制定对称单体封闭duploid和对话duploid的两极化和非关联概念。 我们表明,它们为辅助模型提供了一个直接的风格对应:线性效应辅助分别用于线性延续的(线性)调用-逐推值微积分和对话手性。 特别是,我们表明线性经典L-演算的语法可以在任何对话dulaid中解释,并且它实际上定义了句法对话duploid。 作为一个应用程序,我们通过语义和句法手段建立了长谷川-蒂莱克定理,该定理指出,中央地图和可通俗地图的概念在任何对话duploid中是一致的(特别是对于对称一元类的任何双重否定monad)。
In the spirit of the Curry-Howard correspondence between proofs and programs, we define and study a syntax and semantics for classical logic equipped with a computationally involutive negation, using a polarised effect calculus, the linear classical L-calculus. A main challenge in designing a denotational semantics for the calculus is to accommodate both call-by-value and call-by-name evaluation strategies, which leads to a failure of associativity of composition. In order to tackle this issue, ...
