组合逻辑公理

Question

我正在使用组合逻辑进行定理验证的一些实验,这看起来很有希望,但是有一个绊脚石:已经指出在组合逻辑中,确实例如I = SKK但这不是一个定理,它必须添加为公理.有谁知道需要添加的公理的完整列表？

编辑:您当然可以手工证明我= SKK,但除非我遗漏了某些东西,否则它不是具有相等性的组合逻辑系统中的定理.话虽如此,你可以将我扩展到SKK ......但我仍然缺少一些重要的东西.取一组子句p(X)和~p(X),这很容易解决普通一阶逻辑中的矛盾,并将它们转换为SK,执行替换并评估S和K的所有调用,我的程序生成以下(我使用'用于Unlambda的反击):

''eq''s'''''''''''''''''''''''''''''''''''''''''''''''''''''''''''''''''''''''''''''''''''''''''''''''''''''''' 'k true'k true

看起来我可能需要的是一套适当的规则来处理部分调用'k和',我只是没有看到这些规则应该是什么,我在这个领域找到的所有文献都是为数学家的目标受众而不是程序员.我怀疑一旦你明白答案可能很简单.

Answer 1

有些教科书将我定义为((SK)K)的别名.在这种情况下,它们与每个定义相同(作为术语).为了证明它们的平等(作为函数),我们只需要证明平等是反身的,这可以通过反身性公理方案来实现:

• 命题" E = E "是可推导的(反身性公理方案,为每个可能的术语实例化,这里用元变量E表示)

因此,我想在下面,你的问题研究另一种方法:当组合子I没有被定义为复合词((SK)K)的别名时,而是作为独立的基本组合子常量引入,其操作语义由公理方案明确声明

• ``(I E)= E ''是可推导的(I-axiom scheme)

我想你的问题是问的

我们是否可以正式推断(保留在系统内部),这种独立定义的I在用作减少函数的情况下与((SK)K)完全相同 ？

我认为我们可以,但我们必须采用更强大的工具.我猜想通常的公理方案是不够的,我们还必须声明扩展性属性(函数的相等性),这是主要观点.如果我们想将扩展性形式化为公理,我们必须用自由变量来扩充我们的对象语言.

我认为,我们必须采用这种方法来构建组合逻辑,我们必须允许在对象语言中使用变量.当然,我的意思是"只是" 免费的贵重物品.使用绑定变量将是作弊,我们必须保持在组合逻辑的范围内.使用免费的变量不是作弊,它是一个诚实的工具.因此,我们可以做您需要的正式证明.

除了直截了当的平等公理和推理规则(传递性,反身性,对称性,莱布尼兹规则)之外,我们还必须增加一个推理平等的可扩展性规则.这是自由变量重要的点.

在Csörnyei2007:157-158中,我发现了以下方法.我认为这样可以证明这一点.

一些评论:

大多数公理实际上是公理方案,由无限多个公理实例组成.必须针对每个可能的E,F,G术语实例化实例.在这里,我使用斜体来表示变量.

公理方案的表面无限性质不会引起可计算性问题,因为它们可以在有限的时间内得到解决:我们的公理系统是递归的.这意味着聪明的解析器可以在有限的时间内(此外,非常有效地)决定给定的命题是否是公理方案的实例.因此,公理方案的使用既不会引起理论上的问题也不会引起实际问题.

现在让我们看看我们的框架:

语言

字母

常量:以下三个称为常量:K,S,I.

我添加常数我只是因为你的问题预先假定我们没有将组合子I定义为复合项S K K的仅仅别名/宏,但它本身就是一个独立的常量.

我将用粗体罗马大写字母表示常量.

申请标志:"申请"的标志@就足够了(带有arity 2的前缀表示法).作为语法糖,我在这里使用parantheses而不是显式的应用程序符号:我将使用显式的开启(和结束)标志.

变量:尽管组合逻辑没有使用绑定变量,范围等,但我们可以引入自由变量.我怀疑,他们不仅是语法糖,他们也可以强化演绎系统.我猜想,你的问题需要他们的使用.任何可枚举的无限集(常量和括号的不相交)都将作为变量的字母表,我将在这里用无格式的罗马小写字母x,y,z表示它们......

条款

条款以归纳方式定义:

• 任何常数都是一个术语
• 任何变量都是一个术语
• 如果E是一个术语,而F也是一个术语,那么(E F)也是一个术语

我有时使用实用约定作为语法糖,例如写

E F G H

代替

((E F)G)H).

扣除

转换公理方案:

• `` K E F = E ''是可推导的(K-axiom方案)
• ` S F G H = F H(G H)''是可推导的(S-axiom方案)
• `` 我 E = E ''是可推导的(I-axiom scheme)

我添加了第三个转换公理(我的规则)只是因为你的问题预先假定我们没有将组合子I 定义为S K K的别名/宏.

平等公理方案和推理规则

• `` E = E ''是可推导的(Reflexivity公理)
• 如果" E = F "是可推导的,那么" F = E "也是可推导的(推论的对称性规则)
• 如果" E = F "是可推导的,并且" F = G "也是可推导的,则" E = G "也可以减少(传递规则)
• 如果" E = F "是可推导的,则" E G = F G "也是可推导的(Leibniz规则I)
• 如果" E = F "是可推导的,则" G E = G F "也是可推导的(莱布尼兹规则II)

题

现在让我们调查您的问题.我猜想到目前为止定义的演绎系统还不足以证明你的问题.

命题" I = S K K "是否可以推导？

问题是,我们必须证明函数的等价性.如果它们的行为方式相同,我们认为两个函数是等价的.函数的作用是将它们应用于参数.我们应该证明,如果应用于每个可能的参数,两个函数的行为方式相同.再次,无限的问题!我怀疑,公理计划无法帮助我们.就像是

如果E F = G F是可推导的,则E = G也是可推导的

将无法完成这项工作:我们可以看到这不会产生我们想要的东西.使用它,我们可以证明这一点

" 我 E = S K K E "可以推断

对于每个E项实例,但这些结果只是分开的实例,并且不能作为整体用于进一步扣除.我们只有具体的结果(无限多),无法总结它们:

• 它适用于E:= K.
• 适用于E:= S.
• 它适用于E:= K K.
• .
• .
• .

...

我们不能将这些碎片化的结果实例汇总成一个好的结果,说明扩展性!我们不能将这些低价值的碎片倒入漏斗中,这种推断规则会将它们融合成一个更有价值的结果.

我们必须增强演绎系统的力量.我们必须找到一个可以解决问题的正式工具.你的问题导致了扩展性,我认为,声明扩展性需求,我们可以提出适用于*****任意*****实例的命题.这就是为什么我认为我们必须在对象语言中允许自由变量.我猜想以下额外的推理规则可以完成这项工作:

• 如果变量x不是E和F的术语的一部分,并且陈述(E x)=(F x)是可推导的,那么E = F也是可推导的(推理的可扩展性规则)

这个公理中的难点很容易导致混淆:x是一个对象变量,是我们对象语言的完全解放和尊重的部分,而E和G是元变量,不是对象语言的一部分,而只是用于简洁的表示法公理方案.

(注:更准确地说,推理的外延性规则应该更谨慎的方式形式化,引入元变量X所有可能的对象变量X,Y,Z ...,并且也是另一种元变量Ë在所有可能的术语实例.但是这两种元变量加上对象变量之间的区别在这里并不那么有说服力,它不会过多地影响你的问题.)

证明

让我们现在证明" I = S K K " 的命题.

左手步骤:

• 命题`` I x = x''是具有实例的I-axiom方案的实例[ E:= x]

右手边的步骤:

• 命题" S K K x = K x(K x)"是具有实例化的S-axiom方案的实例[ E:= K,F:= K,G:= x],因此它是可推导的
• 命题" K x(K x)= x"是具有实例化的K-axiom方案的实例[ E:= x,F:= K x],因此它是可推导的

平等的及物性:

• 陈述" S K K x = K x(K x)"与推理的及物性规则的第一前提相匹配,并且陈述" K x(K x)= x"与该推理规则的第二前提相匹配.实例化是[ E:= S K K x,F:= K x(K x),G = x].因此,结论也成立:ë = g ^.用相同的实例重写结论,我们得到声明" S K K. x = x",因此,这是可推导的.

对称性:

• 使用" S K K x = x",我们可以推断"x = S K K x"

平等的及物性:

• 使用" I x = x"和"x = S K K x",我们可以推断" I x = S K K x"

现在我们为关键点铺平了道路:

• 命题" I x = S K K x"与推理的扩展规则的第一前提匹配:(E x)=(F x),具有实例化[ E:= I,F:= S K K ].因此,结论也必须成立,即具有相同实例的" E = F "([ E:= I,F:= S K K ]),产生命题" I = S K K"",quod erat demonstrandum.

Csörnyei,Zoltán(2007):Lambda-kalkulus.一个funkcionális纲要alapjai.布达佩斯:Typotex.ISBN-978-963-9664-46-3.