格雷格·梅雷迪思（Greg Meredith）与艾萨克·德弗兰（Isaac DeFrain）和克里斯蒂安·威廉姆斯（Christian Williams）就LADL一起展开深入探讨。
这是RCast第58期。以下为整理稿。
欢迎收听原文音频。
Greg: 本周谈话是有关证明理论（Proof Theory）的深度技术探讨。上次我们简单介绍了一下。我想先介绍一下理论基础。我会用屏幕共享，以便我们进行交谈；图表稍后会提供，以供日后收听播客的人们使用。
我们将采用图富集（graph-enriched）Lawvere理论，并将分阶段提出新的图富集（graph-enriched）Lawvere理论。这种图富集（graph-enriched）Lawvere理论代表了一种计算概念的编码。实际上，这是一个重写系统。该理论的构造函数将是术语构造函数，有一些重写规则。
我们进行图富集（graph-enriched）的方式与Christian和John Baez进行图富集（graph-enriched）的方式有些不同。实际上，我们在最顶层添加了图论。这样做是为了提供一种讨论源和目标的方式，它与标准SOS语义有点相似。从我的角度来看，这只是一种符号上的便利。也许我们稍后还会讨论其他技术细节，但先让我们看一看最小的细节。
我们有一个非频繁发生器常数。由于重写规则是交互式的，因此我们必须至少有一个带两个参数的term构造函数。这就是互动的意义。单个重写规则的左侧将使用两个参数作为构造函数，然后生成一个新术语。
有一个常数C，一个二进制项构造函数K，然后有K的左右标识。它们可能并不总是存在，或者也有可能重合。对于Lambda，你只有左身份，但没有右身份。在Pi演算或Rho演算的情况下，你有两个身份，但它们是重合的，因为术语构造函数K（在这种情况下为par）是共同的。重写规则Rho的来源必须是TU中的K。目标只是T和U的某个函数。它会根据T和U的信息计算一个新的术语。
Christian: 我对Rho演算为什么是重写规则感到有些困惑。现在，只要将它写下来，看起来就像是另一项操作。
Greg: 它是使重写规则几乎没有语义的源代码和目标代码。
Isaac: 因为你将一切都视为边（edge），所以可以谈论源和目标。
Greg: 正是如此。现在，让我们再迈出一步。我们将分两步实现目标。
Isaac: 在继续之前，我能问一个问题吗？
Greg: 当然，请。
Christian: 有了这个目标方程式，你说重写的目标是T和U的F，那么F到底是什么？
Greg: 这是基于T和U所给出的信息来得到一个新的术语的某种计算方式。
Christian: 好的。明白了。
Greg: 例如，对于Lambda，你知道T将成为抽象。假设Lambda X得到M。N是抽象的论点；那就是U。当计算TU的F时，你就会得到M，而这个M则可以在各处代替X。
Isaac: 好的，我懂了。
Greg: 现在，我们将通过引入评估环境来对此进行修正。可以通过以下两种方法来执行此操作。可以使R（这是我们的评估环境，R代表资源）接受一个术语并生成一个术语，或者使R为常数，然后将其提供给K的一侧。两个方法中的任意一个都可行——至少在我们研究的理论中是可行的。由于Lambda的原因，Mike Stay更喜欢此演示。但你可以采用任何一种方式来做。
我们再来添加两个操作。这对应于以下事实：如果我先跳到重写规则，那么我就可以解释其他术语构造函数了。现在，我们要更改重写规则的源。你只需要在有TU的K的R的情况下进行重写。如果您没有R，那么就有K；它不做评估。由于我们已经采用这种方式进行了修正，因此K就变成了某种配对运算符。它实际上是一种张量，因为你不一定有办法将从中得到任何东西。
您可以根据计算反射来考虑这一点。在旧有理论中，KTU提供了执行计算步骤所需的所有信息。现在我们要说的是，你必须要有这个额外的R，但是R没有任何结构。R只是一个门，就像在Rholang中将Phlo（RChain系统中的燃料—编者按）添加到计算步骤中一样。这是一种基本的直觉。
您可以认为否认R会使K具有反射性，而K则可以使计算具体化。你要做的是提取存储在具体化补偿中的信息。我们提供了两种提取器：一个被称为Par，它使用两个术语为你提供一个术语；另一个则被称为Cut。Par的功能基本上就是在我们重新组装时，它可以对它们进行重新组装或并行连接；而cut则是将它们串联起来。
Isaac: 明确地说，你的意思是通过拒绝原始计算或重写资源，可以有效地将其转换为数据，然后将其放入其他计算中。
Greg: 就是这样。我们的第三步也是最后一步，就是再添加一个种类。这是对原始理论的最终扩展。这个额外的种类代表了上下文的概念。当我们的术语数据类型是可微函子时，这个种类对应于Delta T。
Isaac: 就像Connor McBride的拉链一样。
Greg: 就是这样。这意味着我们将添加另一个常量，就是hole，它从一个常量变为上下文类型。然后我们进行左右介绍。你可以在K的左侧放置一个上下文，在右侧放置一个术语，就可以得到一个新的上下文，或者在K a的右侧放置一个上下文，在左侧放置一个术语，就可以得到一个新的上下文。我们将区分上下文何时适用，也就是你何时替代hole。我们将用左右的碰撞来写，这取决于hole是在左侧还是在右侧。
Isaac: 就像抽象化一样，对吗？
Greg: 除了我们只有一个hole之外，这就像抽象化一样。它甚至比线性抽象化还要更严格。
Isaac: 好的。你有了左右抽象化。
Greg: 正确。然后我们就有了替代的概念。如果我有了一个hole并且得到了术语，那么其他所有内容都将保持不变。但是我们还有一些身份。当将at应用于T上的banged hole时，我会得到T，然后将at应用于碰撞上下文时，将at分布在内部。这些是我们添加到该理论的额外方程式。
Christian: 你需要用什么等式来解释par和cut是如何运行的吗？
Greg: 不，不需要。Cut决定了一切。现在我能定义arrow的概念了，这将开启以下内容，因为它们都是用taus来表达的，也就是类型。实际上，arrow是上下文kai的集合，我可以用T来分解上下文。T填充了一侧，而另一侧仍有hole。对于tau中的任何U，当我将U应用于该kai时，如果存在这样的重写B，则B处于tau素数中。
Isaac: 这个arrow，我想，是保证吗？
Greg: 是的。从这个定义到Caires的定义，这里存在一个ISO。但就是如此。这是一个依赖保证的概念。
Isaac: 好的。
Greg: 现在我们可以组成这些类型了。我们从顶部开始，它表示的是所有术语。如果您有tau和tau素数，则可以沿任一方向组成arrow。所有C现在都已被提升为类型。由于这些taus表示集合，所以我们也有空的tau。这是一个常数。在某些情况下，这对应于归谬法。你也可以将taus融合在一起。可以将R应用于tau，这就是一个resource过的tau了。可以从taus得到K。
这样一来我们就有了所有线性类型了。现在我们还有Rho张量，它需要2个taus，基本上就是一个无源的K，但是它是可裁剪的。它表示的是在进行裁剪时您将以哪种方式进行连接。如果K没有指示，你就不知道该如何连接。tars和caps也像张量一样，但它表示的是你要以串联切割的方式打开K。
然后我们会得到一些缩写。实际上，我们有很多取反。这取决于你在arrow末尾处放的是什么。如果您将身份放在末尾的正确身份上，那就像perp运算符，线性取反。如果将空集放在末尾，那就像是classical vacation。然后，你会得到它们的左右版本。
Isaac: 我就能类型提一个问题吗？
Greg: 问吧。
Isaac: 你有空集之类的东西，对吗？你说taus基本是集。这就像一个可实现性问题，对不对？
Greg: 没错。解释起来就是可实现性。
Isaac: 空类型，它与底层是不同的还是相同的呢？
Greg: 它的运行方式基本和底层相同。
Isaac: 好的，明白了。
Greg: 现在我们继续来讲证明规则。我已经对它进行了颜色编码。如果遵循红色的一面，那就是建立术语。如果遵循蓝色的一面，那就是在制作证明。当两面都有时，你就是在输入术语。键入术语时，可以将其视为为术语构造类型，但也可以将其视为从证明中提取术语。两种方式都可。
这就可以追溯到关于按构造校正的整个观点之上。归根结底，按构造校正就是从程序正确的证明中提取程序。概念就是这样。这就像一个旋转栅。我们将根据顺序构建证明。关于这些连续算法，我们既有直觉形式，也有经典形式。在直觉形式中，十字转门的左侧是一些键入上下文，其中可以有逗号，可以解释为一系列假设。而右侧则恰好是一个键入任务。
如果我们用gamma和delta来覆盖键入上下文，则gamma旋转栅T冒号tau为红色gamma认为T是类型tau。这就是我们建立规则的方式。这样做的理由是，我们拥有一个空的键入上下文，可以得出术语C的类型为C。由于每个常量都有其自己的Singleton类型，因此其实质就是在记录该决定。这就是整个系统运行的基础。好吧，其实我们还有另一种方法，那就是公理规则，我们稍后再讨论。
然后张量，就像gamma认为T是类型tau，而delta认为U是类型tau素数一样。如果将gamma与delta一起使用，你有了两个键入上下文，就会得到TU的K是Rho tau张量tau素数的类型。如果您有一个单一的键入上下文gamma，gamma认为T是tau类型，而U是tau素数类型，则gamma认为TU的T的par是Rho par tau tau素数类型。你可以看到该模式。
Christian: 所以下一个剪切会告诉我们，你需要它们处于相同的上下文中？
Greg: 当我们进行剪切时，我们现在有了剪切规则，我们只能剪切张量的pars，并使用有caps或者类似的剪切。如果我有一个par和一个张量，就是K——这是一个资源被拒绝的K——当我剪切它们时，我将提供一个资源，而这个资源将允许它进行演化。在R上下文中，我具有演化的能力，但是我不会在类型中展示所有的演化。我显示的只是结果，就是右侧的RK。
Christian: 为什么是RK?
Greg: 因为如果你实际通过arrow定义运行一遍的话，你就会明白这就是你所能得到的。
Isaac: 我想推测一下它为什么会是RK。因为我们考虑的是tau perp和tau素数的Rho par吗？
Greg: 正是如此。Tau perp耗尽了taus。
Isaac: 好的。我第一次看的时候没弄懂，但听你再解释一遍之后，就清楚多了。
Greg: 就是这样。基本上，这就像是一个广义分类组合。当A对B，B和B对C时，它们的极性相反。当你将它们插入到一起时，B就会被找出。这是这种追踪的通用版。
Christian: 但是在你不需要的那一部分的组合里——哦，我知道了。双重性正在par之间发生。
Greg: 没错。注意我们所说的并行是什么意思。现在，我们将看到N系列版本——我进行了序列化，这里我使用的是单个gamma——我们可以制作带有delta的gamma版本；我仍然没有决定哪个更好。最好将其分离为一个认为U是类型tau素数的delta。无论如何，关键是要声明意图。你形成了一个K。这变成了一种原理键入，因为此时程序员会向我们提供与Rho caps相关的信息，他们会说：“我打算将此方式以串行方式，而不是并行方式使用。”
Christian: 所以你得做出选择？
Greg: 是的，你要做选择。程序会指示“这就是我要使用的方式。”这是一种类型注释。
Isaac: 我想问一问，这是否对应于Rholang所拥有的较新的句法——显然，我们仍然有并行构成，但也有顺序构成。这和它有关吗？
Greg: 间接相关。
Isaac: 好吧。
Greg: 它属于同一个领域，但目的完完全全不同。
Isaac: 明白了。
Greg: 就像我们把U的T打包成K一样，我们也可以拆包，也就是说，把U中的T打包在cup中，然后我们知道当你有一个T和一个 U打包在cup中时，如果你把它和cap剪切到一起，它们将能被提取出来。
这就是一回事，但是请注意，我们的类型更加复杂。现在，我们必须使用arrow来正确地进行排序。在反序列化剪切中，我们坚持认为T是tau双素数arrow tau perp类型，而U为A tau双素数arrow类型——我说的对吗？我觉得哪里还需要再加一个额外的perp。左侧还有tau素数arrow tau，所以素数是tau素数arrow tau——哦，不，我说的是对的。
我们将运行KTU，以便将tau双素数供给arrow，它将为我们提供tau perp。然后tau素数将被提供给tau素数arrow tau。你将要运行一个tau perp和一个tau，然后它们将一起运行，我们就能得到我们所需要的。Arrow基本上可以帮助我们实现序列化。
Christian: perp是什么来着？
Greg: Perp只是一个缩写。它是arrow的一种形式。如果你把它们堆在一起，我们实际上得到的就是一个双重否定翻译
Christian: 为什么专注于这些相互抵消的类型就足够了？
Greg: 基本上，它所给予我们的是一种会话类型功能。这一切表明，我们既具有原始的模型理论能力（即Caires能力），又具有会话类型能力。我们将两者结合在一起。这些证明规则都与会话类型相关。
Isaac: 你能否再详细解释一下会话类型，以及你对此的看法吗？我对会话类型所知不多。
Greg: 会话类型在很大程度上是从线性逻辑的角度来看待的，例如Wadler的论文“会话作为类型”，应该是这个名字。
Isaac: 这是关于特定渠道的资源或类似的概念。
Greg: 基本上是。说到底就是发生在某些渠道组上的会话。这让人会想起某些情况下你所看到的通用版本，例如当某个程序打开了与数据库的会话时。您知道那具有非常特殊的形态，就是“打开会话，进行大量读写操作，关闭会话”。
会话类型概括了你可以执行的操作，但更进一步——它超越了那个程度。不是轻视Phil，但在很多方面Wadler的语义都非常不令人满意，因为张量意味着顺序合成。
我们可以看到剪切只是par或序列化的一种特殊情况。带有tau perp的T素数和带有tau的T的普通剪切，这实际上只是另一种特殊情况。你可以据此建立线性切割的概念。
Isaac: 你是在说明剪切-消除是从哪里来的。
Greg: 是的。这很明显，但是任何使用剪切的证明都可以变成不使用剪切的证明。方法是——无论在哪里得到一个剪切，都将其替换为重写规则的右侧。
Isaac: 那讲得通了。
Greg: 证明标准化与运行程序完全相同。我们有最紧密的Curry-Howard相关。我们有公理的概念，它建立在上下文的概念之上。如果在键入上下文中将hole键入为tau，则将获得该hole在旋转栅的右侧为tau类型。这就是公理。
然后可以做左右剪切。我们可以通过履行全部义务来形成Lambda，说：“嘿，您确实需要将它应用于某些东西上。“如果我将gamma连同hole键入为tau一起认为U是tau素数，那么gamma认为U bang 在左箭arrow tau的尖arrow上键入tau素数。我”杀“了它。从另一方面说会比较容易。因此，如果gamma与hole一起被键入tau，而T属于类型tau素数，则gamma认为bang T属于类型tau arrow tau素数。所以，如果你给我一个tau，我就给你一个tau。这基本上就是这两项规则所表达的意思。
Christian: 这就是说整体是tau类型的Hole，那么是否具有确定的唯一类型，或者可以是多种类型的呢？
Greg: 如果hole是tau型，则表示你可以证明hole是tau型。无论哪种方式都可。
Christian: 好的。但是我们可以使一个上下文具有任何类型的hole。
Greg: 公理是这么说的。
Christian: 好的。
Isaac: 键入hole的意思只是说上下文需要某种类型吗？
Greg: 是的。就像一个简单的Lamda演算。将hole视为变量，该变量具有特定类型。我们可以进行上下文剪切，可以在左侧或右侧进行剪切。我以右侧为例。右侧的是，如果gamma认为bang T是tau arrow tau素数类型，而delta认为U是tau素数类型——我错了吗？啊，我做到了。有个错别字。Delta认为U是tau类型，那么gamma与delta一起认为RKTU是R tau素数。它完全符合你的期望。它记录的是重写完成后的类型。你看不到内部正在发生的重写。这样说明白吗？
Isaac: 明白。只能看到结果类型。
Greg: 正是如此。这个术语已准备好重写了。它是带有R的TU的K。意料之中。现在我们会得到一个单面序列。所有东西都推到旋转栅右侧了。一切都根据perp运算符进行。现在，实际上，我们不仅在右侧有一个带perp的公理，而且左侧应该也有一个。但是我还没把放入规则。其他也都一样。
真正的区别是，你的系统是否只允许使用双perp关闭（在这种情况下，你会得到一个经典的gadget），或者你的系统是否不采用双perp关闭（在这种情况下，你会得到直观设置）？举例来说，Lambda的封闭度并不高。你可以在Lambda中找到一个可以做到的子集，但是Lambda本身并没有遵循排除中间定律。你会使用直观版本。
Christian: 这两个推论是否是形成tau三角tau素数的唯一方法？
Greg: 这就是你所能用的唯一方法。
Christian: 并且你可以使用那种方法得到任何东西？
Greg: 我认为如此。我们会在证明中再看。
Isaac: 我对你所说的双perp关闭有一种感觉，它可能来自思考向量空间和互积。这可能不是正确的方法……
Greg: 实际上，这是一种非常好的方法。通过双perp关闭，如果你从perp中得到perp，就能回到初始位置。
Isaac: 好吧，这和我想的一样。你还提到了一些极的概念。它看起来很像你所定义的其他符号——我暂时想不起来，但是它就像是Curry符号或你想用其他名称来称呼也行。
Greg: 如果你从拓扑方面考虑，并且将perping或取反或任何事物解释为闭包（如果我有一些拓扑空间，然后我将其闭包，然后将N闭包），那么第二次它就不会移动，因为它已经关闭了。但是在第一次的时候我我可能会包含更多的点。例如，如果我采用一个没有端点的单位间隔，而我现在采用闭包，那么我就是在填充端点。然后，当我再次关闭时，我不会添加任何新点，但它是相同的空间。第一次我确实添加了端点。双perping不会使我进入原始空间。这是一种直观版本。如果你有两次封闭操作或某种复杂的操作，你可以使用经典方法。否则，你还是会使用直观版本。Christian，请注意，U是一些特别复杂的上下文。在上面会有一个hole。
Christian: 为什么?
Greg: U不是一个hole，它是一个上下文。
Christian: 所有这些都是上下文？
Greg: 正是如此。我从一个hole开始，然后可以用hole和各种东西来构建K。特别是，我可以从两个hole开始，然后从中得到带有两个hole的K。然后我可以填补其中一个hole，对另一个hole进行抽象。这样一来，你就能得到全部richness。基本上，U内部有一个非常深的hole。输入上下文记录了你在某个时刻将不得不解决这一问题。
Christian: 我感觉刚开始时，你描述的是如何归纳地将上下文建立成为术语，但是我不记得你是怎么通过它们的相应类型判断来构建所有上下文的了。
Greg: 那就是这个。那就是这个在做的事情。
Christian: 现在，你没有包括任何构造函数。
Greg: 就在这里。所有这些规则在这里都适用
Christian: 好吧。
Isaac: 我很高兴你明确地说明了U里面有hole，因为我没有将其视为上下文。现在这样更容易理解了。
Greg: 也许我应该用kai，而不是U。
Isaac: 那也许会有用。
Greg: 好主意。非常感谢。这是个很棒的反馈。基本上就是这样。显然，细节还有很多。我现在对hole构造足够自信，然后就可以进行实施了。我可能会在圣诞节期间这样做。应该会很有趣。
如上所述，我们凭空引入了这个R。如果有需要，我们可以将原始理论分为红色和黑色。对于其中一种理论，R可以是另一种颜色，反之亦然。你不必凭空捏造R。
您还可以概括上下文，以提供更丰富的标称现象。然后，你可以呈现出所有这些名称。剩下的就是采用高阶语法的et al方法进行标称处理，或者把closet方法与标称Lawvere理论一起使用。这样就搞定了。我们把Lambda和Pi的主要部分都考虑在内了。我感兴趣的是在环境演算（不是基于替换的演算）上进行运行，然后查看我会得到哪种逻辑。但还有算法。
Isaac: 您说环境演算不是基于替换的演算。这我知道，但我研究环境演算已经有一段时间了，那么减少环境演算的概念是什么？
Greg: 这是整树重写。
Isaac: 哦，对。
Greg: 当N到达术语时，它会移至环境中。当out到达一个环境时，它将移出环境。它在重新配置整树，这就是为什么它不能很好地处理互联网问题的原因，因为你是在重新配置整个互联网。它不是本地的。
Isaac: 听上去很贵。
Greg: 是的。即使重写规则是本地的，重写规则的效果也是全局的。Pi和Rho以及类似的概念则要好得多，因为它们实际上是本地交换，而环境则不是本地交换。
Isaac: 这一点很棒。
Greg: 我进行过大量的讨论，尝试了不同的计算方法，然后说：“由于这个原因这个不好，而由于那个原因那个也不好。”但我从来没有写下来过，并且让人们清楚地明白为什么联接演算无法对互联网进行编程。
Isaac: 如果你愿意这么做的话，一定会很有趣。
Greg: 是的。
Isaac: 也许这个优先级很低。
Greg: 对我来说优先级不高，但我很希望能找人一起合作。
Christian: 你在这篇论文中所描述的是一类丰富的Lawvere理论，你认为它算是某种相互作用理论吗？
Greg: 是的，没错。
Christian: 然后，你对这种结构进行了描述，你可以全部增强它们，并为它们配备资源和上下文以及这些有用的类型。
Greg: 是的。
Christian: 而且你将会对此做一些证明。
Greg: 就我们希望在不久的将来发表的论文的格式而言，正是如此。在介绍完最低限度的理论之后，我们会将其应用于Lambda和Rho。这取决于我们是否会进行到标称上。我们可能只会将其应用于SKI和Rho组合器。Rho组合器的好处是我不必处理标称问题。我不需要外来名称。这表明了适用于一对具有良好特性的特定重写系统的理论。
然后我们会进行剪切-消除的证明，所有Curry-Howard相关的好东西，然后再展示一些特性。在2005年的名称空间逻辑论文中，有一件很酷的事情，是我列出了所有我能想到的特性。“这个很酷。我们可以做一个防火墙。我可以编码XML模式。”
我想说明一下，这里有一些非常有趣的特性，例如无死锁或从较高安全性上下文到较低安全性上下文的信息不泄漏。我们可以很容易地在相应的类型系统中写下这些特性。那样应该就绰绰有余了，因为你已经拥有了一个广泛适用的算法。该算法的输出包括一个带有有趣特性的类型系统。相应系统具有剪切-消除标准化特性。这足以构成一份像样的论文了。
Isaac: 你知道重写系统会对正在构建的系统产生任何影响吗？
Greg: 这将使它更有可能具有原理类型。
Christian: 关于类型，我们还有一个问题。你在上半部分所讨论的是丰富的Lawvere理论，然后下半部分则是某种类型系统，但是该类型系统究竟发生在哪里？你是纯粹在语法上谈论它，还是要尝试将其放入Lawvere理论框架中？
Greg: 你要问的是，类型系统的本体状态是什么？
Christian: 对。
Greg: 老实说，我认为我们得到的是另一个类别，而类型则应该是该类别的对象。Lawvere理论发生在一个类别中，类型系统则发生在另一个类别中。我们应该做的是要看到这个类别，然后看到态射是该类别中的证明。如果我们做对了，那么该类别与Lawvere理论产生的类别之间将存在某种关系。两者之间会存在一些函子。
微信扫一扫 
