Rules of definitional reflection
Rules of definitional reflection
复制标题
DOI：
10.1109/lics.1993.287585
复制
发表时间：
1993-06
期刊：
影响因子：
--
通讯作者：
P. Schroeder-Heister
中科院分区：
文献类型：
--
作者：
P. Schroeder-Heister
作者讨论了定义反射的两种规则：扩展逻辑编程语言GCLA中使用的定义反射的逻辑版本和定义反射的omega版本。逻辑版本是一个左引入规则，完全类似于根岑风格序列系统中逻辑算子的左引入规则，而omega版本通过与算术中的omega规则相关的原理扩展了逻辑版本。相应地，两种方法对自由变量的解释不同，导致替换下推理规则的闭包原则不同。这种差异对于定义反射的计算解释至关重要
The author discusses two rules of definitional reflection: the logical version of definitional reflection, as used in the extended logic programming language GCLA, and the omega version of definitional reflection. The logical version is a left-introduction rule completely analogous to the left-introduction rules for logical operators in Gentzen-style sequent systems, whereas the omega version extends the logical version by a principle related to the omega rule in arithmetic. Correspondingly, the interpretation of free variables differs between the two approaches, resulting in different principles of closure of inference rules under substitution. This difference is crucial for the computational interpretation of definitional reflection.>