题

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

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

''eq ''s ''s ''s 'ks ''s 's 'ks s ''s 'k k 'k eq 's 's 'ks s 'k k 'k k ''s 'k k 'k false 'k 是真的 'k 是真的

看来我可能需要的是一组适当的规则来处理部分调用“k”和“”，我只是没有看到这些规则应该是什么，并且我在该领域可以找到的所有文献都是为目标受众是数学家而不是程序员。我怀疑一旦你理解了它，答案可能会很简单。

有帮助吗？

解决方案

有些教科书定义 我 作为纯粹的别名 ((S·K)·K). 。在这种情况下它们是相同的（作为术语） 根据定义em. 。为了证明它们相等（作为函数），我们只需要证明相等是自反的，这可以通过自反公理方案来实现：

  • 命题``乙 = 乙'' 是可推论的（反身性 公理方案，为此处由元变量表示的每个可能项进行实例化 乙)

因此，我认为您的问题研究了另一种方法：当组合器 我 没有被定义为 仅仅是别名 对于复合词 ((S·K)·K), ，但引入为 独立基本组合器 常量本身，其操作语义被声明 明确地由公理 方案

  • ``(我 乙) = 乙'' 是可推论的（公理 方案）

我想你的问题是问

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

我认为我们可以，但我们必须诉诸更强大的工具。我猜想通常的公理方案是不够的，我们还必须声明外延性属性（函数相等），这是要点。如果我们想将外延性形式化为公理，我们必须用以下内容来增强我们的对象语言 自由变量.

我认为，我们必须采用这种构建组合逻辑的方法，即我们还必须允许在对象语言中使用变量。哦当然，我的意思是“只是” 自由的 贵重物品。使用绑定变量是作弊行为，我们必须保持在组合逻辑的范围内。使用自由变量并不是作弊，而是一个诚实的工具。因此，我们可以提供您所需的正式证明。

除了简单的等式公理和推理规则（传递性、自反性、对称性、莱布尼茨规则）之外，我们还必须添加一个 外延性 平等的推理规则。这就是自由变量的重要性。

2007 年 Csörnyei：157-158，我发现了以下方法。我想这样就可以证明了。

一些备注：

大多数公理实际上都是 公理方案, ，由无限多个公理实例组成。必须为每个可能的实例实例化 乙, F, G 条款。在这里，我对元变量使用斜体。

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

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

语言

字母

常数:以下三个称为常量： K, S, 我.

我添加了常数 我 只是因为你的问题预设了我们还没有定义组合器 我 作为单纯的 别名/宏 对于复合词 S K K, ，但它本身就是一个独立的常数。

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

申请签名:“application”的符号 @ 就足够了（带有 arity 2 的前缀表示法）。作为语法糖，我在这里使用括号而不是显式的应用符号：我将使用明确的开始（和结束）标志。

变量:虽然组合器逻辑不使用绑定变量、作用域等，但我们可以引入自由变量。我怀疑，它们不仅是语法糖，还可以强化演绎系统。我猜想，您的问题将需要它们的使用。任何可枚举的无限集（常量和括号符号不相交）都将用作变量的字母表，我将在这里用无格式的罗马小写字母 x、y、z 来表示它们...

条款

术语归纳定义：

  • 任何常数都是一个项
  • 任何变量都是一个术语
  • 如果 乙 是一个术语，并且 F 也是一个术语，那么也 (乙 F) 是一个术语

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

乙 F G H

代替

(((乙 F) G) H).

扣除

转换公理方案：

  • ``K 乙 F = 乙'' 是可推论的（K公理 方案）
  • ``S F G H = F H (G H)'' 可推导出 (S-公理 方案）
  • ``我 乙 = 乙'' 是可推论的（公理 方案）

我添加了第三个转换公理（我 规则）只是因为你的问题预设我们没有 定义的 组合器 我 作为别名/宏 S K K.

等式公理方案和推理规则

  • ``乙 = 乙'' 是可推论的（反身性 公理）
  • 如果 ”乙 = F“ 是可推论的，那么 ”F = 乙” 也可推论（对称 推理规则）
  • 如果 ”乙 = F“ 是可推导的，并且 ”F = G“可推得也，则也”乙 = G" 是可约化的 (传递性 规则）
  • 如果 ”乙 = F“ 是可推论的，那么 ”乙 G = F G” 也可推论（莱布尼茨法则 I)
  • 如果 ”乙 = F“ 是可推论的，那么 ”G 乙 = G F” 也可推论（莱布尼茨法则 II)

问题

现在让我们调查您的问题。我猜想目前定义的推导系统还不足以证明你的问题。

是命题“我 = S K K“可推论？

问题是，我们必须证明函数的等价性。如果两个函数的行为方式相同，我们就认为它们是等效的。函数的作用是将它们应用于参数。我们应该证明，如果应用于每个可能的参数，这两个函数的行为方式相同。又是无穷大的问题！我怀疑，公理方案在这里帮不了我们。就像是

如果 乙 F = G F 是可推导的，那么也 乙 = G 是可推论的

将无法完成这项工作：我们可以看到这并没有产生我们想要的结果。使用它，我们可以证明

``我 乙 = S K K 乙'' 是可推论的

对于每个 乙 术语实例，但这些结果只是单独的实例，不能作为一个整体来进一步推论。我们只有具体的结果（无限多），无法总结它们：

  • 它适用于 乙 := K
  • 成立于 乙 := S
  • 它适用于 乙 := K K
  • .
  • .
  • .

...

我们无法将这些零碎的结果实例总结为一个伟大的结果，说明外延性！我们不能将这些低价值的碎片倒入漏斗中，以将它们融合在一起形成一个更有价值的结果的推理规则。

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

  • 如果变量 x 也不是项的一部分 乙 也不 F, ，和声明（乙 x) = (F x) 是可推论的，那么 乙 = F 也可推论（外延性 推理规则）

这个公理的难点在于，很容易导致混乱：x 是一个 目的 变量，完全解放和尊重我们的对象语言的一部分，同时 乙 和 G 是 元变量，不是对象语言的一部分，但仅用于公理方案的简洁表示法。

（评论：更准确地说，推理的外延规则应该以更仔细的方式形式化，引入一个 元多变的 X 综合所有可能的情况 目的 变量 x、y、z...，还有另一种 元多变的 乙 综合所有可能的情况 术语实例. 。但是两种元变量加上对象变量之间的区别在这里并不是那么说教，它不会对您的问题产生太大影响。）

证明

现在让我们证明这个命题``我 = S K K''.

左侧步骤：

  • 命题``我 x = x'' 是一个实例 公理 具有实例化的方案[乙 := x]

右侧步骤：

  • 命题“S K K x = K X （K x)" 是一个实例 S-公理 具有实例化的方案[乙 := K, F := K, G := x]，因此可推论
  • 命题“K X （K x) = x" 是一个实例 K公理 具有实例化的方案[乙 :=x, F := K x]，因此可推导出

平等的传递性：

  • 陈述 ”S K K x = K X （K x)" 匹配第一个前提 及物性 推理规则和陈述“K X （K x) = x" 匹配该推理规则的第二个前提。实例化是[乙 := 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”

平等的传递性：

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

现在我们已经为关键点铺平了道路：

  • 命题“我 x = S K K x" 与第一个前提匹配 扩大 推理规则：（乙 x) = (F x)，带有实例化 [乙 := 我, F := S K K]。因此结论也必定成立，即“乙 = F" 具有相同的实例化 ([乙 := 我, F := S K K]），产生命题“我 = S K K”，quoderat demostrandum。

佐尔坦·乔尔内伊 (2007)： Lambda-kalkulus。Alapjai 的功能程序。 布达佩斯：打字机。ISBN-978-963-9664-46-3。

其他提示

您不需要定义我作为公理。起始于以下：

I.x = x
K.x y = x
S.x y z = x z (y z)

由于SKanything = anything，然后SKanything是恒等函数，就像I。

所以，I = SKK和I = SKS。不需要定义我作为公理，你可以将其定义为语法糖，其别名SKK。

S和K的定义是只公理。

通常的公理是完全的β为均等，但不给ETA平等。库里发现了一组大约三十公理常使用的获得对完整性的β-ETA平等。他们列在辛德雷和塞尔丁的介绍组合程序和lambda演算的。

罗杰·欣德利，库里的最后一个问题，列出了一些额外的必要条件，我们可能要通过演算和说明，我们没有满足所有这些映射之间的映射。你可能不会在意了所有的标准。

许可以下： CC-BY-SA 和 归因
不隶属于 StackOverflow
scroll top