J-Calc：直觉主义正义逻辑的类型化λ演算及其在模块化程序设计中的应用

{→}可在www.sciencedirect.com在线获取理论计算机科学电子笔记300（2014）71-87www.elsevier.com/locate/entcsJ-Calc：一种用于直觉主义正义逻辑的Konstantinos Pouliasis康斯坦丁诺斯·普利亚西斯1，2，5计算机科学美国纽约市立大学研究生中心Giuseppe Primiero朱塞佩·普里米罗3，4，5米德尔塞克斯大学联合王国摘要在本文中，我们给出了一个系统J-Calc，它可以被看作是直觉主义正义逻辑片段的类型化λ演算我们对J-Calc有不同的解释，特别是作为一个两阶段的证明系统，在这个系统中，我们证明检查理论T的推导的有效性，一个更强的理论T′和计算作为一个类型系统的单独编译。我们建立了一些第一个元理论结果。关键词：类型λ-演算，正义逻辑，模块化程序设计。1引言对哥德尔的不完备性结果（[ 18 ]）的一个合理的解读是，“真实性”的概念与“特定理论中的真理”的概念这一现象甚至可以用1这项研究是Konstantinos Pouliasis博士研究的一部分他欠教授的。谢尔盖·阿尔捷莫夫2电子邮件：Kpouliasis@gc.cuny.edu3这项研究是在Giuseppe Primiero担任比利时根特大学逻辑与科学哲学中心弗兰德斯研究基金会（FWO）博士后研究员时进行的他感谢财政支持。4电子邮件：G. mdx.ac.uk[5]两位作者都感谢2013年直觉模态逻辑与应用研讨会匿名评审的建设性意见。1571-0661 © 2013 Elsevier B. V.在CC BY-NC-ND许可下开放访问。http://dx.doi.org/10.1016/j.entcs.2013.12.01272K. Pouliasis，G.Primiero/Electronic Notes in Theoretical Computer Science 300（2014）71与非哥德尔方程的关系，例如，通过IΔ0和IΔ1的算术运算[27]，IΔ1和PA，PA和ZF等[29，15]。同样的问题也出现在自动定理证明中。一个很好的例子是类型系统和交互式定理证明器（例如Coq，Agda）的类型函数范式。在这类系统中，当必须保证函数的终止时，可能需要援引更强有力的证明原则。在一个类型系统中推理两种证明对象的需要是最明显的，当人们想要建立一个理论T的不可容许结果时，相反，可以在一些更强的TJ中证明。于是，类型系统必须协调在某个TJ中存在某个类型φ的证明对象和证明φ（在T中）的不可证明性的类型<$s.ProvT（s，φ）的证明对象在这项工作中，我们认为，正义逻辑[7]的显式模态可以用来公理化两个不同演算的对象之间的关系，如上述。众所周知，可证明性谓词可以使用模态进行公理化[14]，[9]。证明逻辑LP[3]更进一步，提供了显式的证明项（证明多项式）来约束对有效性的判断通过将直觉命题演算（IPC）中的推理转换为经典证明，LP通过模态（诱导BHK语义）获得IPC的经典语义在本文中，我们通过创建一个模态类型理论来明确地公理化两种证明对象之间的关系，该理论从两个演算中推理出对象的绑定或链接：一个较低级别的理论T，用Church风格的λ-项表示直觉主义证明对象，用IPC表示;一个更高级别的，可能更强的和经典的（共）理论T，作为基础，用正义来表达它的证明对象。这样一个（共）理论的公理化直接遵循正义化逻辑的证明系统（这里仅限于其适用的K-片段），并用于经典地（意味着真值函数地）解释直觉主义自然演绎的构造。我们的链接系统的基本原则如下：构造必要性=容许有效性=真理（在T）+有效性（在TJ中）因此，一个真（在T中）命题P的必然性对它在TJ中的预期解释的证明（由证明）的存在是敏感的。我们假设一个关于类型Just的解释函数，它将T的类型论域映射到TJ的类型论域。我们使用M：P类判断（读作j：只是P（可以理解为如果把它们分开，这个原则可以用一种评判的方式来重写：M：P+j：JustPQjP true请注意，Q-类型是由对所选解释（TJ）敏感的判断（QjP）索引的。为了完成这幅图，我们需要Qj型的标准元. 自然地，这类见证人是来自T的证明对象之间的联系K. Pouliasis，G.Primiero/Electronic Notes in Theoretical Computer Science 300（2014）7173和TJ与相应的类型（P和Just P）。因此，我们引入了一个链接见证构造函数Link。这就是必然性是如何被引入的：通过用TJ的演绎来检验T的演绎，我们建设性地推理T中有效陈述（通过TJ）的可容许性。因此，该原则成为：M：P+j：JustPLink（M，j）：QjP我们展示了这个原理在我们的系统中是如何容许的所提出的类型理论的一个可能的应用可以是一个精化类型系统。对于具有模块化编程结构或外部函数调用的编程语言，如我们在第5节中所示。在这些语言中（例如ML家族），程序或模块可以调用在其他地方（在另一个模块中，甚至在另一种语言中）实现的外部定义。我们可以将由justifications索引的Q-类型中的函数读作此类语言的链接进程，这些语言执行良好类型构造的映射，剩余程序是指所有模块类型和函数调用的实例都被它们的实际实现替换（即链接到）的程序，这些实现仍然隐藏在模块中。我们用一个真实的例子来展示，只要稍加修改，我们的类型系统就可以在这种设置中找到一个自然的应用程序。在这里，我们关注类型系统本身，而不是它的操作语义。这项工作的支柱是通过源于[5]，[6]的模态表示IPC的证明理论语义的想法与这项工作有关的模式的操作方法见[4]。LP的模块性，即它通过适当改变证明多项式的公理化来实现其他类型的模态推理的能力，随着正义逻辑家族的发展而显示出来[7]。这种能力很容易被保存下来。我们的工作将丰富的类型系统和正义逻辑的模块化结合在证明即程序原则中。因此，我们得到了Curry-Howard对应的扩展（[30]，[17]），并采用直觉主义类型理论的判断方法（[21]，[22]，[23]，[25]，[11]）。我们的系统借鉴了在判断方法中开发的其他模态演算（例如[28]，[19]，[1]，特别是[13]为模态逻辑K）。我们的系统与那些系统的主要区别是，与以前的LP（[2]，[10]）的λ-演算一样，我们的类型系统托管对应公式证明对象的两类类型关系。它可以被看作是一种尝试，为有效性判断增加证明条件，如[28]所示。所得到的类型系统采用依赖类型（[12]，[26]）将两种证明对象与模态联系起来。类型论域和公正项的构造从[8]和[16]中的思想中汲取了很多在[24]中也可以找到使用依赖类型的附加（上下文）术语扩展类型化模态演算。6见[20]。74K. Pouliasis，G.Primiero/Electronic Notes in Theoretical Computer Science 300（2014）71►2类型系统本系统可以被看作是一个演算的推理在三个不同的-阶段。 第一，蕴涵片段中证明对象的推理在没有任何元理论假设的有效性，在第3节介绍的直觉理论T。这种演算由旋转栅门（英语：Turnstile）Γ IPC 7形式化，其中Γ包含T中句子证明的假设。 底层逻辑是直观的，系统对应于简单类型lambda演算的隐含片段。第二，具有正当性的推理，对应于在某些固定的基础系统中关于证明对象的推理：第4节介绍的（共）理论TJ。我们假设TJ为直觉系统T提供了预期的语义。对应的旋转门是ΔJ。从任何具体的元理论中抽象出来，从纯逻辑的角度来看，解释理论至少应该最后，在第6节介绍的两个公理系统的蕴涵片段中，证明对象之间存在联系的推理。这种推理模式在完整的旋转栅门Δ;ΓJC中公理化了。该系统的核心是Q-引入规则，它允许表达关于链接存在的推理。这个想法是完整的规则（即包括上下文）对应于基于其子项上的现有链接为复合项构建链接。因此，完整的旋转门Γ;Δθ是一种模态逻辑，它在两个演算之间“压缩”了相互推理。在这个框架内，我们获得了一个计算的正义逻辑限制到K模态推理的阅读。在任何任意嵌套级别（即任意模态类型）上呈现这种相互推理之前，我们首先引入JCalc1，它是对类型域的限制，最多可达1级Q-嵌套。我们固定了一个可数的命题论域（Pi），它对应于T的句子。这个宇宙的元素可以通过构造或正义来居住。因此，对于每个命题，我们将需要两种居住关系。对于T中的φ型构造M，我们将写作M：φ。我们将写j：Justφ来表达j是一个证明的事实（证明在TJ）的性质。当没有混淆时，我们将用j：：φ来表示它。 M中的一个结构：T中的φ并不必然有它的必要性：为了这个目的， 一个相应的正解j：必须从TJ中得到正解φ 反之亦然，φ在TJ中的正义化（j）只导致它的有效性，而不是它的可容许性建设性必要性（constructive necessity） 这可以用命题类型Q j φ来表示 只有当（较弱的）理论T实际上用一个φ型的构造M“响应”从T j通过推导j而已知的有效事实φ时，才能得到Q j φ的构造。因 此 ，一旦（且仅当）我们有j：：φ，则可以将Qjφ视为[7]人们也可以使用一个额外的常量符号null，并写为null;ΓIPC来表示纯粹在T中的推理，因此，在没有任何元理论环境的情况下。K. Pouliasis，G.Primiero/Electronic Notes in Theoretical Computer Science 300（2014）71750I→E作为一个良好的命题。更强的理论可能能够判断Qjφ（给定j：：φ）并证明例如u：：Qjφ。在这种情况下，TJ换句话说，当用正当化进行推理时，类型的宇宙是上下文相关的。要谈论一个命题的可容许的（或构造的）必然性，我们需要在TJ中存在一个相应的证明对象j，它确立了命题的有效性。3没有基本假设的推理：IPC关于构造性理论（T）的隐含片段的推理，不需要公式化的可证明性陈述，是在简单类型的lambda演算的隐含片段中完成我们首先给出规则中使用的元变量φ的语法φ：= P i|φ→ φ演算通过引入：类型Prop0的论域;构造简单命题假设Γ0的良构上下文的规则;控制RPIPC的规则。Pi∈Prop0ATOM0φ1∈Prop0φ2∈Prop0IM pLφ1→φ2∈Prop0无菌IPCwf无0Γ0φ∈Prop0Γ-EX pΓ0，x：φ=IPCwfΓ0的IPCwfx：Pi∈Γ0Γ-REFLΓ0πIPCx：PiΓ0，x：φ1IPCM：φ2→Γ0IPCM：φ1→φ2Γ0IPCMJ：φ1Γ 0=IPCλx：φ1。M：φ1→ φ2Γ0μIPC（MMJ）：φ24在存在基础的情况下进行推理：正义演算J在最小基础的存在下的推理对应于基础理论TJ中证明对象存在的推理。从逻辑的观点来看，最小的基本假设是TJT中的非逻辑公理越多，TJ应该满足的规范就越多（人们需要更强的基础来证明更强的理论）。抽象076K. Pouliasis，G.Primiero/Electronic Notes in Theoretical Computer Science 300（2014）710►从任何特定的T和TJ，并假设只有T包含最小逻辑，关于在TJ中证明的存在性的规定是：• 有换句话说，TJ的类型的子集应该充当T中的类型的解释;• 为上述IPC片段的公理化特征化的所有实例至少提供• 包含一些肯定前件规则，翻译为：在TJ中存在类型Just（φ→φ）和类型Justφ的证明对象应该意味着存在类型Justφ的证明对象。4.1最小正义逻辑J-Calc1在这些最小的要求下，我们开发了一个最小的正义逻辑，它能够实现模态推理，作为对T和TJ的证明之间存在联系的推理。我们首先实现模态推理限制在度公式（即Q-嵌套的水平）1。这样的演算将被用来作为基础，以建立一个完整的模态演算与正义的公式任意程度。下面是元变量的语法：φ：= P i|Qjφ|φ1→φ2j：= s i|C|j1j2t：= x i|λx i：φ.t|Js：：φ.tC：= K [φ1，φ2] |S [φ1，φ2，φ3] |C1-C2π：=Π s：：φ1。φ2| φ s：：φ1。πT：= φ|只是φ|π s：= s ix：=xi4.1.1最小基础推理J0关于这样一个最小元理论的推理在它自己的旋转门中被公理化了（J）.[9]然而，关于J0的正义型论域（对应于（共）理论TJ中的公式）以及Δ0上下文的wf谓词的判断如下：[8]如果我们扩展我们的片段，我们应该相应地扩展我们的规范，但这可以很容易地直接在完全正当化逻辑中我们选择留在这个片段中，以节省介绍。[9]这是微积分的一部分，它直接对应于仅限于应用片段的证明代数。K. Pouliasis，G.Primiero/Electronic Notes in Theoretical Computer Science 300（2014）7177nilJ0wfNILΔ0<$J0wfΔ0<$J0φ∈Prop0S impLEΔ0<$J0Justφ∈jtype0Δ0<$J0Justφ∈jtype0s/∈ Δ0Δ-AppΔ0<$J0wfs：：φ∈ ΔΔ-REFL0Δ0，s：：φ<$J0wf0Δ0J0s：：φ我们添加逻辑常数，以满足要求，J0包括一个公理化的表征遵循正义逻辑，我们从组合逻辑中定义了包括K，S在内的多态构造函数的签名。这些构造函数的值是公理常数，证明了相应逻辑有效性的所有实例在TJ直觉主义逻辑在J0中的公理化特征与规则模式Times（正义的适用性）一起满足了TJ逻辑推理的最小要求Δ0<$J0只是φ1→φ2→φ1∈j型0KΔ 0J0 K[φ1，φ2]：：φ1→φ2→φ1Δ0<$J0Just（φ1→φ2→φ3）→（φ1→φ2）→（φ1→φ3）∈jtype0SΔ 0J0 S[φ1，φ2，φ3]：：（φ1→φ2→φ3）→（φ1→φ2）→（φ1→φ3）Δ0<$J0j2：：φ1→φ2Δ0<$J0j1：：φ1次Δ0J0j2j1：：φ24.1.2压缩：J-Calc1=IPC+J0+Q−简介在本节中，我们介绍J-Calc1，用于推理链接的存在性，即证明IPC（T）和J0（TJ）中存在证明的构造。通过构造一个链接，我们证明了公式的构造必要性，表明它是真实有效的。链接具有形式为Qjφ的类型，其中j是适当类型的证明。J-Calc1在K中实现了模态逻辑定理，直到1次（即，公式，其中其子公式包括最多1个水平的Q）。我们首先引入上下文和公正类型（分别为Δ0Wf，JustWf）的良构性判断，以及Prop1论域及其上下文：78K. Pouliasis，G.Primiero/Electronic Notes in Theoretical Computer Science 300（2014）7101011JC1Δ0J0wfΔ0;nil ΔJC1wfΔ0WFΔ0; Γ1<$JC1wfΔ0<$J0j：：φJUST WFΔ0; Γ1<$JC1j：：φφ∈Prop0Δ0; Γ1<$JC1j：：φPRO p-INTROJΔ;Γ<$Qφ∈PropΔ0; Γ1<$JC1φ∈ {Prop0，Prop1}x/∈Γ1Γ-AppΔ0; Γ1，x：φJC1wf从Prop0中公式的证明，我们可以推断它们在T中的可容许性。因此，Γ1可能包括来自Prop0和Prop1的假设。对于Prop0，Prop1的居住，我们首先积累扩展到新类型宇宙（Prop1）的直觉推理，适应第3节的规则：Δ0;Γ1<$JC1wfx：φ∈Γ1Γ-REFLΔ0; Γ1<$JC1x：φΔ 0; r 1，x：φ1 <$JC1 M：φ2IΔ 0; Γ 1ΔJC1 λx：φ1。M：φ1→φ2→Δ0; Γ1<$JC1M：φ1→φ2Δ0; Γ1<$JC1MJ：φ1→EΔ 0;Γ εJC1 （MMJ）：φ2为了使这两个演算相关，我们提出了一个提升规则，把严格的Prop0判断转化为对证明链接（Prop1）的判断。在该规则中，]-运算符确保上下文列表]r严格包括Prop0中的假设。操作员]可以是被视为与应用于上下文列表的提升操作相反，该提升操作如下所述在顶层擦除一个级别的加框假设]Γ ：=匹配 Γ，nil| Γ J,xJi:Qjφi⇒] Γ J,xi:φi|Γ J, ⇒ ] Γ J一个相应的迭代let绑定构造（letbinding）同时引入上下文提升。迭代let绑定的目的是提取子项（x1.. xn），并将它们组合到整个项M的目标，从而创建其残差。我们在第5节的例子中展示了这个结构的操作。11K. Pouliasis，G.Primiero/Electronic Notes in Theoretical Computer Science 300（2014）7179设：将Γ与nilint（）=（）| ΓJ,xJi:Qjφi⇒(let∗ΓJ)inletlin k(xi,ji)=xJi|Γ J,⇒ let∗Γ JTheQ-Introduction rule goes as follows:;] r1JC1M：φΔ0; r1JC1j：：φQ-I输入环（M，j）中的Δ0; Γ1<$JC1（令<$Γ）：QφJ最后，在空的Γ1下，我们允许从非空的Δ0抽象。正如我们将看到的，所产生的抽象（J-项）是模态类型的居民，并且对应于连接过程。它们的类型是自然的，因为链接的类型对它的目标代码是敏感的。我们介绍了形成和居住规则：Δ0，s：：φ1;φJC1φ2∈ {Prop0，Prop1}连续性pEΔ0; φJC1 φs：：φ1.φ2∈φΔ0，s：：φ;ΔJC1t：TΔ0，s：：φ1;<$JC1π∈<$Δ0;<$JC1<$s：：φ1.π∈<$中文（简体）P.E.1Δ 0; ΔJC1Js：：φ。 t：φ s：：φ。不Δ 0; ΔJC1t：Δ s：：φ。TΔ 0; φJC1j：：φ-E LIMΔ 0; ΔJC1 （t j）：T[s：=j]5Computational Motivation：一种用于独立编译的类型系统在本节中，我们将展示如何将J-Calc视为一种类型系统，用于在支持单独编译（模块化编程或外部函数调用）的类型化语言中这些语言遵循客户端/服务器的编程方法：客户端代码可以引用服务器在其他地方实现的代码定义;服务器可以是某个模块，或者甚至是提供所需函数调用的另一种语言，但它不需要知道实现（封装）的细节。这种系统中的挑战是提供一种单独编译的机制，使得客户端（或源）代码独立于服务器的实现中的改变而在下文中，我们将J-Calc表示为080K. Pouliasis，G.Primiero/Electronic Notes in Theoretical Computer Science 300（2014）71在这样的环境中连接进程的一种类型系统。按照我们的语言：T的构造在这里表示客户端（或源）表达式，TJ的构造表示目标（或服务器）代码表达式。我们的链接通过Q-Intro规则链接处理生成器，这些生成器使用来自服务器的不同实现我们显示，下面的模块教科书的例子，我们的类型系统提供了这样一种语言所需的抽象，使客户端代码需要编译一次，只，独立于服务器模块可能提供的不同的实现5.1生成泛型代码作为一个例子，我们将使用ML类模块定义。我们首先定义模块的公共签名（即服务器提供给客户端的操作）。这里我们提供一个整数栈的签名模块类型INTSTACK =sig类型intstackval Empty：intstackval push： int->intstack->intstackval pop：int->intstack->intstackend;;这个签名可以用各种方式实现，但我们的目标是只编译一次源代码就生成泛型代码我们以源代码表达式Push 2Empty：intstack为例，并逐步展示了遵循我们的演算的泛型代码的构造。首先，我们通过重写术语来分解签名的用法：]r =x1：int→intstack→intstack，x2：intstackn（x12 x2）：intstack其次，我们假设在有效性上下文中实现了即Δ =s1：：int→intstack→intstack，s2：：intstack=s 12s2：：intstack使用Q-Intro规则，我们得到：Δ; r =xJ1：Qs1（int→intstack→intstack），xJ2：Qs2intstackletlink（x1，s1）=xJ1inletlink（x2，s2）=xJ2inlink（x12x2，s12s2）：Qs12s2intstackK. Pouliasis，G.Primiero/Electronic Notes in Theoretical Computer Science 300（2014）7181►最后，抽象我们得到一个类型化的链接过程生成器，它对服务器提供的不同实现► J s1. J s2. λxJ1.λxJ2. 设在link（x12x2，s1<$2<$s2）中的r为：1. 2. Qs1（int→intstack→intstack）→Qs2intstack→Qs12s2intstack哪里let_r=deflet_link（x1，s1）=xJ1inlet_link（x2，s2）=xJ25.2提供实现服务器可能提供instack模块签名的不同实现。这两种教科书上的方法使用的是整数列表或数组。给定不同的实现，初始源代码具有不同的计算值，因为它引起的链接发生了变化。示意性地：push−l−i−n→k空−l−i−n→kCons：QCons（int→intstack→intstack）[]：Q[]intstackpush2空−l−i−n→kCons2[]：QCons*2*[]intstackpush−l−i−n→k空−l−i−n→kAddarr：QAddarr（int→intstack→intstack）create（）：Qcreate（）intstackpush2空−l−i−n→kAddarray2create（）：QAddarr*2*create（）intstack这两种情况都被我们生成的泛型代码捕获，单独编译源码和实现。在第一种情况下，我们有：Just[intstack]=List，Just[push]=Cons，Just[Empty]=[]由此，我们使用Q−Intro得到以下结果：link（Empty，[]）：Q[]intstack缺点► link（push，Cons）：Q（int→intstack→intstack）最后，使用上一节中获得的链接过程生成器，并在应用程序的标准操作语义（β-归约）和let-binding评估下，我们使用列表实现将源代码链接到其剩余程序► link（push 2 Empty，Cons*2*[]）：QCons*2*[]intstack82K. Pouliasis，G.Primiero/Electronic Notes in Theoretical Computer Science 300（2014）71add *2* create（）JJ类似地，使用完全相同的代码生成器，通过实现关闭ΔJust[intstack]= ArrayJust[push]=addStringJust[Empty]= create（）我们获得链接：► link（push，addition）：Q附加的（int→intstack →intstack）► link（Empty，create（））：Q堆栈间根据之前在应用程序的标准操作语义（β-归约）和let绑定评估下的泛型判断，我们使用Array实现将源代码链接到其剩余程序► link（push2 Empty，addPush* 2 *create（））：Qintstack请注意，客户端代码不需要重新编译。我们的通用代码配置提供了表达的手段来评估源上下文给定的模块签名的不同实现。6完整的微积分：J-CalcJ-Calc1激发了对任意嵌套的模态推理的推广：J-Calc。为了允许这样的推广，我们需要JustQjφ形式的类型的证明。让我们修改一下：如果φ是一个命题（或者，T语言中的一个句子），那么Justφ对应于某个（共）理论TJ中φ的预期解释。在J-Calc1中，我们可以逻辑地推理T的事实（根据TJ有效）的推定可接受性。T中的一个证明与Tjd中同一类型的一个现有证明之间存在联系，将导致构造形式为Qjφ的类型，其中φ是一个简单类型。 为了得到2次或2次以上的模态定理，我们有假设TJ本身可以表达这种联系的存在。也就是假设TJ可以表示T和它自己的可证性谓词。因此，假设j：：φ，我们可以把一个JustQjφ型的证明项读作证明TJ中的一个证明，证明T（x，φ）x，证明T′（x，Justφ）用T表示。我们将通过引入额外的适当常量来指定T期望捕获有了这种证明，我们就可以在一个互感构造中得到作为一个类型宇宙的切片的任何有限i的Propi示意性地：Prop0→Just Prop0→Prop1→Just Prop1，依此类推。这样我们就得到了完整的最小正义逻辑。由于不同类型的判断被不同的类型关系分开，我们不需要像J-Calc1那样提供不同的演算，而是直接提供一个10[10]事实上，在正当化中进行推理时，邻接的Γ语境是纯粹的弱化，因此我们可以将这些判断分离在一个但我们也有收获：我们可以挤两个create（）K. Pouliasis，G.Primiero/Electronic Notes in Theoretical Computer Science 300（2014）7183►JC►∈6.1公正性（有效性）判决正义类型系统必须包括：关于上下文良构性的判断（wf）;关于TJ在它是T的元理论的要求下可以推理什么的11个判断（jtype）;关于正义类型论域的构造的判断（jtype）和关于它的居住的最小要求（即，逻辑常数的最小签名）。术语的语法与第4.1节中的相同，不同的是现在对Prop宇宙的限制被删除。我们逐步引入：Prop的形成规则; jtype的形成规则;构建命题和证明的良构上下文的规则（其中我们将使用以下等式规则进行简化：nil，s1：：φ1，s2：：φ2，... =defs1：：φ1，s2：：φ2，. ） 的。nil;nilJCwfΔ; ΓJCwf无汤姆Δ; Γ<$JCPi∈PropΔ; Γ<$JCφ1∈PropΔ; Γ<$JCφ2∈PropIM pLΔ; Γ<$JCφ1→φ2∈PropΔ; r∈JCj：：φΔ;Γ<$Qjφ∈PropBOXΔ; ΓJCφ支柱JTYPEΔ; Γ<$JCJustφ∈j型仅φ∈j型s/∈ΔΔ-AppΔ，s：：φ;Γ εJCwfΔ; Γ<$JCφ∈Propx/ ∈Γ-AppΔ0; Γ，x：φwf6.1.1道具居住这是该系统的逻辑命题推理的第一部分。Δ; Γ∈JCwfx：φ∈Γ-REFLΔ; ΓJCx：φΔ; r，x：φ1→JCM：φ2→Δ; r ∈JCλx：φ1。M：φ1→ φ2Δ; ΓJCM：φ1→φ2Δ; ΓJCMJ：φ1→EΔ; τ εJC（MMJ）：φ2前提（Δj：：φ，Δ;Γwf）到单个前提（Δ;Γj：：φ）。[11]关于语境有效性判断的类似处理，可以在[26]中找到我84K. Pouliasis，G.Primiero/Electronic Notes in Theoretical Computer Science 300（2014）711226.1.2jtype居住区现在我们进入系统的核心。在下面的判断中，我们提供了正义类型（jtype）的规范元素的构造。这些判断反映了TJ是某些T的元理论的最低要求，如第4.1.1节所述，以及关于内在化证明链接推理本身的具体说明更具体地说，我们要求TJ能够在自身内部捕获关于（T的证明对象与自身之间的）链接的推理，并且还内化T的肯定前件。为了捕获这些可证明性条件，我们添加了常量构造函数！（砰）和卡帕。虽然在下一节中对链接的引入进行了公理化，但关于链接的判断是不正确的。和Kappa构造函数应该与Q-Intro一起查看。他们见证了这样一个事实，即TJ内化了（T的）肯定前件，并将存在（再次是T的）联系起来。仅φ1→φ2→φ1∈j型KΔ; r∈JCK [φ1，φ2]：：φ1→φ2→φ1Δ; Γ<$JCJust（φ1→φ2→φ3）→（φ1→φ2）→（φ1→φ3）∈j型Δ; r∈JCS [φ1，φ2，φ3]：：（φ1→φ2→φ3）→（φ1→φ2）→（φ1→φ3）Δ; ΓJCj2：：φ1→φ2Δ; ΓJCj1：：φ1Δ;nilJCM：QCφΔJj2j1：：φ2蒂梅斯CBANGΔ; ΓJC！C：：QφΔ;Γ<$JCJustQj′φ1∈jtypeΔ;Γ<$JCJustQj（φ1→φ2）∈jtypeΔ;γKappa[j，jJ，φ，φ]：：Qj（φ→φ）→Qj′φ→Qjj′φKA ppA6.2证明链接我们的下一个任务是将K模态的主规则公式化为提升规则通过证明链接从对结构的推理到对有效性的可接受性的推理。为了反映自然演绎中的模态公理K，我们必须获得一个反映以下可证明性原则的规则φ1true，.，φ ntrueφ1valid，.，φ nvalidφvalidQ-I NTROQφ1真，...，Qφntrue，. Qφ真我们继续给居民类似的解释，在第SJC112K. Pouliasis，G.Primiero/Electronic Notes in Theoretical Computer Science 300（2014）7185► ►►4.1.2：12Δ;]rJCM：φΔ; rJCj：：φQ-INTRO在link（M，j）中的Δ;r∈JC（lett∈r）：最后，从空的Γ上下文上的Δ上下文的抽象适用于扩展的类型域：Δ，s：：φ;JCt：TΔ;JCt：s：：φ。TΔ0;JCj：：φ非线性函数Δ;φJCJs：：φ。 t：φ s：：φ。TΔ; T ΔJC（t j）：T[s：=j]7进一步的结果和结论标准的元理论结果可以证明为J-Calc。我们在这里只提到迭代let算子满足标准交换性与替换规则，结构规则可以被证明。我们将跳过索引中的jsjc。定理7.1（弱化）J-Calc在两种推理模式中都满足弱化：(i) 如果Δ; nil j：：φ，且Δ; r wf，则Δ; r j：：φ。(ii) 如果Δ; Γ j：：φ，则Δ，s：：φJ; Γ j：：φ，其中s为新的。(iii) 如果Δ; Γ <$M：φ，则Δ; Γ，x：φJ<$M：φ，其中x为新的。证据 对所有的项，在这两种结构的导出树上进行结构归纳。第一个命题的证明是空洞的，因为在正义化形成中，Γ语境是无关紧要的。 因此，其逆也可以被示出。 Q定理7.2（收缩）J-Calc满足收缩：(i) 若Δ，s：：φ，t：：φ; nil j：：φJ，则Δ，u：：φ; nil j [s t/u]：：φJ。(ii) 若Δ，s：：φ，t：：φ;Γ <$wf，则Δ，u：：φ; Γ[s <$t/u]<$wf。(iii) 如果Δ，s：：φ，t：：φ;Γ<$M：φJ，则Δ，u：：φ; Γ[s<$t/u]<$M[s<$t/u]：φJ[s

下载后可阅读完整内容，剩余1页未读，立即下载