gpt4 book ai didi

logic - 组合逻辑公理

转载 作者:行者123 更新时间:2023-12-01 09:10:35 25 4
gpt4 key购买 nike

我正在用组合器逻辑进行定理证明的一些实验,这看起来很有希望,但是有一个绊脚石:有人指出,在组合器逻辑中,例如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”,我只是不明白这些规则应该是什么,因此我在该领域可以找到的所有文献都是为这些而写的。目标对象是数学家而不是程序员。我怀疑答案一经理解就可能很简单。

最佳答案

一些教科书将 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。

    关于logic - 组合逻辑公理,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/1374896/

    25 4 0
    Copyright 2021 - 2024 cfsdn All Rights Reserved 蜀ICP备2022000587号
    广告合作:1813099741@qq.com 6ren.com