logic - 组合逻辑公理

Question

我正在用组合器逻辑进行定理证明的一些实验，这看起来很有希望，但是有一个绊脚石:有人指出，在组合器逻辑中，例如I = SKK，但这不是一个定理，必须将其添加为公理。有人知道需要添加的公理的完整列表吗？

编辑:当然，您可以手动证明I = SKK，但是除非我遗漏了什么，否则它不是带有相等性的组合逻辑系统中的定理。话虽如此，您可以将我宏扩展为SKK ...但是我仍然缺少一些重要的东西。采取容易解决普通一阶逻辑矛盾的子句p(X)和〜p(X)的集合，并将它们转换为SK，执行替换并评估S和K的所有调用，我的程序生成了以下(我在使用Unlambda的反引号的位置):

'eq's's's'ks's's'ks's'kk'k eq's's'ks'kk'kk's'kk'k false 'k true'k true

似乎我需要的是一组适当的规则来处理部分调用“k”和“s”，我只是不明白这些规则应该是什么，因此我在该领域可以找到的所有文献都是为这些而写的。目标对象是数学家而不是程序员。我怀疑答案一经理解就可能很简单。

Answer 1

一些教科书将 I 定义为((S K)K)的别名。在这种情况下，每个definitionem都是相同的(术语)。为了证明它们的相等性(作为函数)，我们只需要证明相等性是自反的，这可以通过自反性公理方案来实现:

命题``E = E''是可推论的(自反性公理方案，针对此处用亚变数E表示的每个可能项进行实例化)

因此，在以下情况中，我想您的问题将探讨另一种方法:当combinator 我未将定义为复合术语 ((SK)K)的 别名别名，而是作为 独立的基本组合器引入的常量本身，其操作语义由axiom 方案明确声明为

``( I E)= E''是可推论的( I-公理方案)

我想你的问题问

我们是否可以正式推断(保留在系统内部)，这样的独立定义的 I 在用作归约函数时的行为与((S K)K)完全一样？

我认为可以，但是我们必须使用更强大的工具。我猜想普通的公理方案还不够，我们还必须声明可扩展性(函数的相等性)，这才是重点。如果我们想将可扩展性形式化为一个公理，则必须使用自由变量来扩展对象语言。

我认为，我们必须采用这种方法来构建组合逻辑，这样就必须允许在对象语言中使用变量。当然，我的意思是“只是” 免费贵重物品。使用绑定变量可能会作弊，我们必须留在组合逻辑领域内。使用免费的变量不是作弊，这是一个诚实的工具。因此，我们可以为您提供所需的正式证明。

除了简单的等价公理和推理规则(及物性，反身性，对称性，莱布尼兹规则)，我们还必须为平等性添加可扩展性推理规则。这是自由变量很重要的地方。

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

一些说明:

实际上，大多数公理都是由无限多个公理实例组成的公理方案。必须为每个可能的E，F，G项实例化实例。在这里，我将斜体用于变量。

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

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

语言

ALPHABET

常数:以下三个称为常数: K ， S ， I 。

我添加常数 I 只是因为您的问题假设我们尚未将组合词 I 定义为复合词 S K ojit上的纯别名/宏，它自己的。

我将用粗体罗马大写字母表示常数。

应用程序的符号:``应用程序''的符号@就足够了(前缀标记为2)。作为语法糖，我在这里使用括号代替显式的应用程序符号:我将同时使用显式的开头(和结束)符号。

变量:尽管组合器逻辑未使用绑定变量，范围等，但是我们可以引入自由变量。我怀疑，它们不仅是语法糖，而且还可以增强演绎系统。我猜想，您的问题将需要使用它们。任何可枚举的无穷集(常量和括号符号的不相交)都将用作变量的字母，在此我将使用未格式化的罗马小写字母x，y，z表示它们。

条款

术语归纳定义:

任何常数都是一个术语

任何变量都是术语

如果E是一个术语，F也是一个术语，那么(E F)也是一个术语

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

E F G H

代替

(((E F)G)H)。

扣除

转换公理方案:

`` K E F = E''是可推论的( K-公理方案)

`` S F G H = F H(G H)''是可推论的( S-公理方案)

`` I E = E''是可推论的( I-公理方案)

我添加第三个转换公理( I 规则)仅是因为您的问题假设我们尚未定义组合器 I 作为 S K 的别名/宏。

平等公理方案和推理规则

``E = E''是可推论的(自反性公理)

如果可以推导“E = F”，那么也可以推导“F = E”(对称推理规则)

如果可以推导“E = F”，也可以推导“F = G”，那么也可以推导“E = G”(传递性规则)

如果可以推导“E = F”，那么也可以推导“E G = F G”( Leibniz规则I )

如果可以推导“E = F”，那么也可以推导“G E = G F”( Leibniz规则II )

题

现在，让我们调查您的问题。我猜想到目前为止定义的推论系统还不足以证明您的问题。

命题“ I = S K K ”是否可以推论？

问题是，我们必须证明功能的等效性。如果两个函数的行为相同，则认为它们是等效的。函数的作用是将其应用于自变量。我们应该证明，如果将两个函数应用于每个可能的参数，它们的作用方式相同。再次，无限的问题!我怀疑，公理计划无法在这里为我们提供帮助。就像是

如果可以推导E F = G F，那么也可以推导E = G

会做不到这一点:我们可以看到这并不能满足我们的需求。使用它，我们可以证明

可以推导`` I 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是 meta 变量，不是对象语言的一部分，但仅使用简要表示公理方案。

(注:更确切地说，应该以更谨慎的方式形式化推理的可扩展性规则，在所有可能的对象变量x，y，z ...以及另一种元上引入元变量x在所有可能的术语实例上的变量E。但是，这两种亚变量加上对象变量之间的区别在这里并不是那么教条，它不会对您的问题产生太大的影响。)

证明

现在让我们证明以下命题`` I = S K K ''。

左侧步骤:

命题`` I x = x''是带有[[E:= x]

的 I-公理方案的实例

右侧步骤:

命题“ S K K x = K x( K x)”是 S-a-Kojit = _ strong_ojit_r ，G:= x]，因此可以推导

命题“ K x( K x)= x”是具有实例化[E:= x，F:= K x]的 K-公理方案的实例，因此可推导

平等的及物性:

语句“ S K K x = K x( K x)”匹配传递性 K = x“匹配此推理规则的第二个前提。实例为[E:= S K K x，F:= K x( K x)，G = x]。因此结论也成立:E =G。用相同的实例重写结论，我们得到语句“ S K K x = x”，因此，这是可推论的。

平等对称:

使用“ S K K x = x”，我们可以推断出“x = S K K x” ojit

平等的及物性:

使用“ I x =”和“x = S K K x”，我们可以推断“ I x = S x =

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

命题“ I x = S K K x”与扩展的第一个前提匹配推论规则:(E x)=(F x_)，带有实例化，F:= S K K ]。因此，结论也必须保持不变，即“E = F”具有相同的实例化([E:= I ，F:= S K K ])，产生命题“ I ojit_r S K K “，演示演示。

Csörnyei，Zoltán(2007):Lambda-kalkulus。一个funkcionálisprogramozásalapjai。布达佩斯:Typotex。 ISBN-978-963-9664-46-3。