交互式实现器和单子
Interactive Realizers and Monads
摘要：
我们提出了一个可实现的解释系统的量词自由算术，这是相当于经典算术的片段没有“嵌套”量词，这里称为EM 1-算术。我们将经典证明解释为交互式学习策略，即通过与“环境”和彼此交互来经历知识和学习的几个阶段的过程。我们通过两个合适的单子的建设给出了一个分类介绍的解释。
英文摘要：
We propose a realizability interpretation of a system for quantifier free arithmetic which is equivalent to the fragment of classical arithmetic without "nested" quantifiers, called here EM1-arithmetic. We interpret classical proofs as interactive learning strategies, namely as processes going through several stages of knowledge and learning by interacting with the "environment" and with each other. We give a categorical presentation of the interpretation through the construction of two suitable monads.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
