Realizability, introduced by Kleene, can be understood as a concretization of the Brouwer-Heyting-Kolmogorov (BHK) interpretation of proofs, providing a framework to interpret mathematical statements and proofs in terms of their constructive or computational content. Over time, this concept has evolved through various extensions, such as Kreisel's modified realizability or Krivine's classical realizability. Parallel to these developments, Girard's work on linear logic introduced another perspective, often seen as another concrete realization of the BHK interpretation. The resulting constructions, encompassing models like geometry of interaction, ludics, and interaction graphs, were recently unified under the term linear realizability models to stress the intuitive connection with intuitionnistic and classical realizability. The present work establishes for the first time a formal link between linear realizability models and the realizability constructions of Kleene and Krivine. Our approach leverages Miquel's framework: just as linear logic can be viewed as a decomposition of intuitionistic and classical logic, we propose a linear decomposition of implicative algebras and show that linear realisability models provide concrete examples of such decompositions.

翻译：可实现性由 Kleene 引入，可理解为布劳威尔-海廷-柯尔莫哥洛夫（BHK）证明解释的具体化，为从构造性或计算性内容的角度解释数学陈述与证明提供了框架。随着时间推移，这一概念通过多种扩展形式不断演变，例如 Kreisel 的修正可实现性或 Krivine 的经典可实现性。与此同时，Girard 在线性逻辑方面的工作引入了另一种视角，常被视为 BHK 解释的另一种具体实现。由此产生的构造——包括交互几何、博弈学与交互图等模型——近期被统一归入“线性可实现性模型”这一术语，以强调其与直觉主义及经典可实现性之间的直观联系。本研究首次在线性可实现性模型与 Kleene 及 Krivine 的可实现性构造之间建立了形式化联系。我们的方法借鉴了 Miquel 的理论框架：正如线性逻辑可视为直觉主义逻辑与经典逻辑的分解，我们提出了蕴含代数的线性分解，并证明线性可实现性模型为此类分解提供了具体实例。