带构造函数的Lambda演算的延拓模型及其转换

可在www.sciencedirect.com在线获取理论计算机科学电子笔记286（2012）337-350www.elsevier.com/locate/entcs带构造函数的Lambda演算的延拓模型芭芭拉小1焦点- INRIA博洛尼亚大学（意大利）摘要带构造函数的逻辑演算将映射ML中的模式分解为一些原子规则。其中一些与通常的计算直觉（特别是类型直觉）不匹配。然而，可以为无类型演算定义一个抽象的模型概念，它有一个平凡的语法实例。然而，为这种演算设计一个非句法模型的问题仍然没有解决。在本文中，我们在无类型的设置中回答这个问题，回到lambda演算与构造函数的第一个动机：模拟具有两个独立堆栈的抽象机器。 这立即提供了CPS到通常的lambda演算的转换。 在语义层面上，这种转换将无类型lambda演算的任何延续模型转换为lambda演算与构造函数特别地，任何Scott域都可以变成这样的模型。关键词：λ演算，模式匹配，延续传递样式转换，范畴语义，延续模型。介绍模式匹配是现代函数式编程语言（Haskell，Ocaml）和证明助手（Agda，Coq，Proof Assistant）中的一个关键特性。自90年代后期以来这些演算的语法属性已经在类型化和非类型化的设置中得到了彻底的研究，这使得Jay实现了一种以模式匹配为中心的编程语言[8]。对这些形式主义的更抽象的方法可以更深入地理解它们，并可能在它们之间进行比较。据我们所知，没有（非语法）指称模型已被定义为任何这些演算。由于其简单的语法，带构造函数的lambda演算（或λC-演算）可能是最好的开始。其实，大多数人，1电子邮件：barbara. ens-lyon.org1571-0661 © 2012 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2012.10.001338B. Petit/Electronic Notes in Theoretical Computer Science 286（2012）337模式匹配需要定义一个功能强大的模式替换操作，λC演算的操作语义由原子规则组成：模式替换ML被分解为对常量的简单分析（如Pascal的case1.2）。虽然这最后一条规则初看起来是相当违反直觉的（它在介绍论文中被称为模型的一个朴素定义可以在范畴论中给出，用于带构造函数的无类型lambda演算[12]。然而，似乎很难建立这个定义的非句法实例。这让我们回到了60年代后期理论计算机科学的主要挑战之一对象D=DD）。1970年，Scott[16]解决了这个问题，并提出了一种新的解决方案：这就是所谓的D∞domain。 后来发现，这些领域实际连续化模型（由R和C的互作用刻画，使得C=RC×C）纯lambda演算[15]。这些延续模型的基本思想是使用纯lambda演算到简单类型lambda演算的CPS 我们在本文中使用相同的方法：我们定义一个用构造函数将lambda演算转换为lambda演算，然后在CCC中解释翻译后的术语（带有一些必需的同构）。主要的困难是解释模式分析器（称为case绑定）。事实上，为了使模型的定义在概念上更简单，我们使用了一个case绑定的复合操作，它在CPS中有一个非平凡的翻译。然而，翻译是正确的，并提供了预期的对lambda演算的连续模型与构造函数的合理定义大纲：在第一节中，我们通过为lambda计算定义一个抽象机器，直观地展示了lambda计算的构造函数。CPS翻译自然地产生于这个机器;我们在第二节中将其形式化。二、在最后一节中，我们给出了模型的范畴定义（第二节）。3.1），和连续模型（第3.1节）。3.2）的lambda演算与构造函数，我们表明，第二个形成一个子类的第一个（节。3.3）。最后，我们证明了λC-演算的延拓模型已经存在了很好的实例（例如Scott1带构造函数的1.1第一种方法：两栈抽象机我们用构造函数的有限集合C（c，d等。）和case构造{|θ|} ·t，其中t是项，θ是大小写绑定，即 一B. Petit/Electronic Notes in Theoretical Computer Science 286（2012）337339从构造函数到项的部分函数：θ：={c1<$→t1;···;ck <$→tk}这种情形约束的域{c1;·· ·;ck}用ydom（θ）表示，θci表示项ti. 模式匹配发生在这样一个case绑定与其域的构造函数相关联时，就像对常量的case分析一样：{|θ|} ·c → tif c <$→ t ∈ θ条件分支，测试一个布尔值，如果为真，则返回t或u，分别为false（其中true和false是构造函数），然后写入如果t，u= λx。{|true ›→ t; false ›→ u|}·x.在这种语言中，现在有两种不同的值：函数（通常的λ-抽象）和构造函数2。它们中的每一个都可以由上下文中的相应构造来评估：分别是应用程序的参数和案例构造的案例绑定。我们还可以将Krivine抽象机[5]扩展到这种语法，通过将最初组成求值上下文的参数堆栈替换为两个堆栈：一个（称为“右堆栈”）用于参数，另一个（“左堆栈”）用于case绑定。 当在此机器中评估术语，然后如果它是case构造或case绑定，则与左堆栈交互，如果它是应用程序或 λ-抽象这台机器在图中正式定义1.一、评估术语（如果t，u为假）在这个机器中（从两个空栈开始）确实会导致配置*u*。但这台机器也能模拟匹配复合数据结构。Terms：t，u：= x|tu|λ x.t|C|{1}|θ|}·t用例绑定：θ，φ：= {c1<$→t1;···; ck <$→ tk}（k≥0）应用堆栈：π：=π |t·π案例堆叠：τ：=π |τ·θ过程：s：=τ*不*π执行规则：τ * λx.t * u·π τ* t[x：=u]* π（Pop）τ图1. 一个两个堆栈的抽象机器。[2]第二种价值将在第二节中详细阐述一点二τ* 你* π►τ* t* u· π（推力）·θ*c* π►τ* θc* π（Popc）τ* {|θ|}·t* π►τ·θ* t* π（推力c）340B. Petit/Electronic Notes in Theoretical Computer Science 286（2012）337APPLAMLAM APPCASECONSCASEAPPCASE LAMCASECASE（AL）（λx.t）u→t[x：=u]（LA）λx. tx→t（x∈/fv（t））（CO）{|θ|} ·c→ t（（c <$→ t）∈ θ）（CA）{|θ|}·（tu）→（{|θ|}·t）u（CL）{|θ|}·λx.t→λx. {|θ|}·t（x∈/fv（θ））（CC）{|θ|我们的目标是|φ|}·t→{|θ◦φ|}·t其中θ={c1<$→t1;. ;cn<$→tn}={c1→{|θ|}·t1;. ;cn→{|θ|{\fnSimHei\bord1\shad1\pos （200 ，288 ）}{\fnSimHei\bord1\shad1\pos（200，288）}图2. 带构造函数的λ-演算1.2ML型模式匹配请注意，构造函数，就像任何术语一样，可以应用于任何数量的参数（它们是可变的）。我们称一个数据结构为一个构造函数，它可能应用于一些参数。例如，可以通过数据结构来表示自然数，使用两个构造函数S和0以及自然数的一元编码。predictor函数被写成pred：= λx。{|0<$→0; S<$→λz.z|}·x.它对一个数Sn的应用实际上被求值为n（我们跳过第一个β-约化步骤）：⬦*pred（Sn）*{|θ|} ·Sn*►·θ*Sn*►·θ *S* n·►*λz.z * n·►⬦* n *⬦（其中θ={0<$→0;S<$→λz.z}）。更一般地，与分支“C（x1，...，xk）->t“在类似ML的程序中表现得像一个项，分支c<$→λx1. xk.t在我们的机器中计算。在这个意义上，机器上面提出的方法能够用简单的常数分析规则在精心设计的数据结构上模拟模式匹配。同样的思想也是基于lambda演算的构造函数（或λC演算）。1.3λC演算的操作语义ML风格的模式匹配在双栈抽象机中通过给构造函数一个双重状态来实现：它们可以应用于一些参数以形成一个复合数据结构（在这种情况下，它们与应用程序栈交互），但它们也可以被视为一个常量，由case绑定进行分析（然后与case栈交互）。在语义设置中，这种上下文切换对应于以下case和application构造之间的交换规则：{|θ|}·（tu）（{|θ|}·t）u。这是带构造函数的lambda演算（图2）的一个关键规则，称为CASE APP（或简称CA除了这个规则，微积分还支持通常的β和η-约化（分别为： AL和LA），以及我们认为B. Petit/Electronic Notes in Theoretical Computer Science 286（2012）337341以前看过的，还有一个实例构造和λ-抽象之间的交换规则（CL），以及一个实例绑定的组合规则（CC），λC-演算具有连续性和分离性[1]。写上→n为归约关系的传递闭包→，可以使用规则al、ca和co来检查pred（Sn）→n。尽管规则CASE APP与通常的类型直觉不匹配（相同的子项可以像函数一样应用，或者像数据结构一样匹配模式），但情况组合对应于逻辑中的交换转换[6，Sec.10.4]：{|θ|我们的目标是|c1›→u1;. ;cn<$→un|}·t→{|c1› →{|θ|}·u1;. ;cn→{|θ|}·un|}·t关于求值上下文，该规则相当于将一个case栈的所有case绑定都合并到一个case绑定θ1<$·· ·<$θk中（可选）（左结合性为<$）。我们也考虑下面的λ C -演算的另一种抽象机，我们称之为KAMλC：定义1.1（KAMλC）。 一个过程是一个三重过程*不*π，其中πθθ是可选的大小写绑定（θ或θ），t是项，π是项的堆栈。四个执行规则是θθθ|φ|} ·t *πθφ *t*π其中，如果<$θ<$=<$，则<$θ<$$> φ为φ，如果<$θ <$= θ，则θ<$φ为φ。实际上，从计算的观点来看，规则CASE CASE不是绝对必要的（它只对分离性质是必要的因此，我们也可以考虑没有cc的λC-演算（λ−C-c演算），以及我们提出的第一个抽象机版本。这也将导致一个稍微不同的模型概念（见脚注3和5）。在下一节中，我们将使用这台机器将带有构造函数的lambda演算转换为纯lambda演算。2CPS翻译Plotkin [14]使用堆栈抽象机来定义按名称调用和按值调用λ演算之间的连续传递样式（CPS）转换实际上，机器的栈可以用λ演算中的对来编码。以同样的方式，我们将基于KAMλC定义λC-演算到具有对的lambda演算（或λP-演算）的CPS翻译。一个λC-termt将被一个λP-termt转换，它在一个rgument中对文本k（continuationn）进行一个求值，并返回在机器中用上下文k对t求值的结果342B. Petit/Electronic Notes in Theoretical Computer Science 286（2012）337.Σ我|=x| Mθ，Mπ|⟩ | ⟩|为|M θ * t * m |uπ，Mπ|⟩ | ⟩||Mθ*λx. t*Mπ|=let|x，xπ′|=Mπin|Mθ*t*xπ′|（ifx∈/fv（Mθ，Mπ））|=let| x1 ;.|x1; ... ; xn|n= Mθin| *xi* Mπ||φ|} · t * M π|为|⟨| N 1 ; ··· ; N n|n* t * Mπ| ⟩n* t * Mπ|其中Ni=λ k′。让我们|zθ，zπ|n=k′in|Mθuizπ|如果ci<$→ui∈φNi=<$ifci∈/dom（φ）图3.λC-演算到λP-演算的转化2.1目标演算一个约束是一对约束，|Mθ，Mπ|其中Mθ和Mπ是两个λP项，分别表示求值上下文的实例绑定和应用栈。从现在起，我们将构造函数集C写成{c1，···，cn}，λ C演算的一个情况约束θ将由n元组θ翻译|M1，·· ·，Mn|其中如果（ci<$→ti）∈θ，则Mi是ti，或者如果ci∈/dom（θ），则Mi是一个特殊的常数t（在这里意味着mat c h失效）。λP-演算的语法和规则如下：M、N、P：=x| λx.M|MN|∗ | ⟨|M、N| ⟩ |πi（M）（i∈{1，2}）（λx.M）N→PM[x：=M]; （Mx）→PM（x∈/fv（M））πi（π|M1、M2| n）→PMi ;|π1（M），π2（M）|n →PM我们对变量使用与λ C -演算中相同的名称，尽管我们也可以将某些λP-变量写成k（表示延拓）。我们使用符号|M1，...，ML| πl和πl（M）用于元组的通常编码和具有对的一般化投影。我们也写让|x1，.，XL|对于项（λx1，...， xl.M）πl（P）. πl（P）（当l不指定时 ，它是2），因此，1L让我们|x1， . ，xl|l=|N1， . ，N1|M中的n→P<$M[x1：=N1]. . . [x1：=N1]。2.2CPS翻译则λP-演算中λC-项t的平移为givenbyyt：=λk. 让我们|xθ，xπ| = kin|xθ* t * xπ|其中，在上下文中t的结果是|Mθ，Mπ|其中Mθ和Mπ是两个λP项，表示为|Mθt Mπ|，由图3中的归纳法定义。一个变量、一个λ-抽象和一个应用的翻译（在原谅延续的“情况”部分之后）完全对应于翻译c.b.v.。- c.b.n. [14]《易经》。构造函数ci的转换在于将应用程序上下文赋予case上下文（xi）的第i个组件。 注意，没有给出案例上下文（我们使用术语“x”），因为xi有自己的案例上下文（例如，2.1）。的翻译B. Petit/Electronic Notes in Theoretical Computer Science 286（2012）337343+++一个案例结构相当于组成与案例上下文结合的（翻译的）案例。例2.1设S={ci<$→ui/i∈S<$[1.. n]}和φ={ci<$→si/i∈S′n[1. n]}。则项u ={|φ|我们的目标是|ψ|}·（cjt）（其中j ∈ dom（n））是：|为|⟨| N 1，...，|N1,..., Nn|n*{|ψ|} ·（cjt）* Mπ|(with Ni = λk。让我们|zθ，zπ| = k in |Mθsizπ|如果i∈dom（φ））|为|⟨| P1，…，|P1,..., Pn|n*cjt * Mπ|（其中Pi=λ k′。让我们|zθ′，zπ′|n=k′in|⟨|N1，...，Nn|⟩n٨ui٨zπ′|如果i∈dom（φ））|为|⟨| P1，…，|P1,..., Pn| ⟩n*cj*⟨|tπ，Mπ| ⟩|= let|x1;. ; xn|n= |P1，…，Pn|乌恩在| *xj*|tπ，Mπ| ⟩|=let|x1;. ; xn|n= |P1，…，Pn|nin xj|，|tπ，Mπ| ⟩| ⟩→PPj|，|tπ，Mπ|⟩ |⟩→Plet|zθJ，zπJ|=|，|tπ，Mπ|⟩|塞林|⟨|N1， . ，Nn|n*uj*zπJ|→|⟨|N1， . ，Nn|你好，|tπ，Mπ|⟩|这种转换使lambda演算的模拟与构造函数在lambda演算与对（Theo.2.4）。这个结果来自以下引理（通过对t的平凡归纳证明）：引理2.2设t，tJ，u是三个λC-项，x是t j中的非自由变量. 则对任意λP-项N，Mθ，Mπ，(i) |Mθ* tJ* Mπ|[x：= N]=|Mθ [x：= N]* tJ* Mπ [x：= N]|(ii) |MθtMπ|[x：=u]→P|Mθ[x：=u]*t[x：=u]*Mπ[x：=u]|(iii)Mθ→PMθJ=|Mθt Mπ|→P|MθJ* t *Mπ|Mπ→PMπJ=π|MθtMπ|→|Mθ*t*MπJ|引理2.3对于任意λC-项t，u，任意情况绑定φ，φ，和任意λP-项Mθ，Mπ，|→p|M θ * t [ x：= u ] * MΠ|Mθ* t[x := u] *Mπ||Mθ*λx. tx*Mπ|→P|MθtMπ|如果x∈/fv（t）|φ|} · c * M π| →p|M θ * u * MΠ|如果c <$→ u∈φ|if c ›→ u ∈ φ|φ|} · tu * M π|为|M θ *（{|φ|} · t）u * M π|} · t) u * Mπ||φ|} · λx.t * M π|=|=|Mθ*λx。{|φ|}·t*Mπ|如果x∈/fv（φ）|φ|我们的目标是|ψ|} · t * M π|为|M θ *{|φ◦ψ|}·t*Mπ|}·t * Mπ|注意，在λP-演算中，只有β-约化和η-约化以及常数分析实际上被某些约化步骤所模拟的λ C -规则。其他规则对应于机器对堆栈的管理，并且在CPS翻译期间定理2.4（正确模拟）对于任意λC-项t，tJ，344B. Petit/Electronic Notes in Theoretical Computer Science 286（2012）337×我‡t→tJ意味着t→Ptj。2.3指称模型模拟定理在λp-演算的任何模型中提供了λC-演算的合理解释。事实上，如果[·]是等于等价项的λP-项的非整数，则tλCtJ蕴涵tλPtj（由Theo. 2.4和Church-R osser性质）和hus[t]=[tJ]（对于本文中提出的每一个Ch演算L，我们记L为它的归约规则的自反对称传递闭包）.在下一节中，我们给出了λC-演算模型的范畴定义，并展示了如何将带对的λ演算模型转换为λC-模型。这种模型转换将直接来自我们刚才介绍的CPS3λC演算的经典模型在本节中，我们简要介绍了λC-演算的范畴模型（更多细节和证明可以在[12]中找到），并且我们证明了纯lambda演算的连续模型具有良好的结构，可以被视为λC-模型。记法：在笛卡尔闭范畴（CCC）中，我们写IdA为恒等式变体-ism在A上，f;g是f和g的合成。 我们用A B表示两个对象A和B的乘积，乘以BA是它们的指数，乘以1是终端object. k上的第i个投影态射记为πk（或πi）如果k= 2），则f和g的配对是f ∈f，g∈，ev是赋值态射，Λ（f）是curriedF的形式。3.1λC演算的范畴模型在范畴论中，纯lambda演算的一个模型是一个CCC，它有一个自反对象D=DD。实际上，λ-项在D中被解释，并且DD的p点是从术语到术语的函数（即， 开放术语，抽象为自由变量）。然后一个态射lam：DD→D使得能够从函数x到t的映射的表示构造λx.t的表示。以同样的方式，态射app：D→DD允许解释任何项对另一项的应用。同样，等式app_lam=Id确保解释尊重β-等价。为了在这样的范畴中解释λC-演算，需要一些额外的态射（用于解释构造子和格构造），以及它们之间的一些等式来验证格规则。一个格约束θ将在Dn中得到解释：如果定义了它，则第i个复合点nt对应于θci，否则它是D的一个特殊点（意味着匹配失败）。那么一个态射case：（Dn× D）→ D需要解释case构造{|θ|}·t，给定θ在Dn中的表示和t在D中的表示. 对于每个构造函数ci∈ C，我们都可以得到D的一个p_i_c_i。B. Petit/Electronic Notes in Theoretical Computer Science 286（2012）337345‡我/dom（θ）），那么我们需要一个额外的规则定义3.1（λC-模型）无类型λC-演算的范畴模型是结构（C，D，app，lam，（c）n ，case），其中i i=1• C是一个笛卡尔闭范畴，D是它的一个对象。• app：D→DD和lam：DD→D形成同构：D=DD。• 所有的c_i• 图的四个图4个可换（（D1）对每i ∈ <$1... n））。CASE CONSCASEAPP（Dn×D）×D= Dn×（D×D）Dn=Dn×1case×IdId×（app×Id）（D1）πnId×c我我（D2）D× DDn×（DD×D）app×IdId×evDcaseDn×DnDD×DDD× D电动汽车案例DCASE CASE（D3）Dn×1IdDn× Dn× Dπ2情况1个D‡（D4）（Dn×Dn）×D= Dn×（Dn×D）·×IdId×caseDn× DDn×D案例案例D图4.λC-模型中的交换图图中描述的态射的等式4.确保我们非正式地给出的解释尊重λC-等价。图（D4）和图（D2）的交换如何分别导致规则CASE CONS和CASE APP的有效性是非常清楚的规则CASE CASE的有效性通过态射·：Dn×Dn→Dn（D4）表示，它表示范畴框架中的格约束组合（Lem.3.3）。它被定义为态射的配对（IdDn×πn）;情况，对于1≤i≤n。图（D3）是唯一一个不直接转换λC-演算的归约规则的图。它表示匹配失败和匹配失败3的匹配之间的等价性，并且对于可靠性w.r.t. 规则是这样的。3如果我们丰富λ- 具有显式匹配失败的演算（即， 一个特殊的常数和规则C{|θ|}·c → n如果c ∈{|θ|}·→，用于连接（关闭临界对346B. Petit/Electronic Notes in Theoretical Computer Science 286（2012）337我Γ=f，···，f：Dk→Dn，其中f⎧请注意，没有对应于该规则的图卡色拉姆在定义λC模型。以同样的方式，规则CL封闭了CA和AL之间的一个临界对，与之对应的图的对易（D2J）是由（D2）的对易性和D的反射性引起的，表示为：莱姆3.2.这个图使用了一个态射case：Dn×DD→DD，它抽象了一个变量的case构造：它把一个case绑定θ和一个函数映射x到t变成了函数映射x到{|θ|}·t，它被正式定义为（Dn ×DD ）×D=10×（DD×D）IdDn×evDn情况×DD.引理3.2（Diagram（D2J））如果（app，lam）形成D和DD之间的同构，则（D2）的对易等价于下面图的对易：Dn×DD案例分析DDId×lamDn×D情况林D（D2J）这使得能够在任何λC-模型中定义λ C -项的合理解释：如果t的自由变量包含在Γ=（x1，...，[1][2][3][4][5][6][7][8][9][10][11][12][13][14][15][16][17][18][19][10][11] 五、[xi]Γ=πk：Dk→D[tu]r=Dk[t]r，[u]rD×D应用程序×IdDDD×DevD[λxk+1.t]r =DkΛ（ft） DD拉姆丁其中ft=Dk×D=Dk+1[t]Γ，xk+1[c]r=Dk！Dkc1个D[英|θ|}·t] r= Dk[θ][θ]r，[t] r Dn情况DD我=Γ 1n快！dk;dk如果ci∈/dom（θ）图5. 分类模型中λC项的解释引理3.3（分类事例复合）如果θ和φ是自由变量都在Γ中的两个事例绑定，则它们在任何λC-模型中的解释都是满足的[θ φ]=Dk [θ]Γ，[φ]Γ<$Dn ×Dn•Dn.CC）。我们在这里提出的模型对于扩展的微积分来说仍然是合理的，图（D3）对应于最后一条规则。或×[ui]r 如果ci<$→ui∈θDB. Petit/Electronic Notes in Theoretical Computer Science 286（2012）337347者，如果我们从微积分中去掉规则Case，则（D1）和（D2）的交换是充分的.348B. Petit/Electronic Notes in Theoretical Computer Science 286（2012）337ׇ∼×命题3.4（健全性）如果（C，D，app，lam，（c）n，，case） 是λC-i i=1模型，然后图。 5通过D的点[t]解释每个闭λC-项t，使得tλC tJ=[t]=[tJ]。实际上λC-模型对于子演算甚至是完全的，没有匹配失败[12]。3.2连续模型一个笛卡尔闭范畴是纯λ-演算的模型，如果它有一个等价于它的函数空间的对象D，我们可以在其中解释λ-项。其中有延续模式4（见优秀介绍[15]）：CCC与两个o b∈C和R满足方程C ∈=C ×RC。实际上，取D=RC满足了条件D_（？）=D_D，并导致λ-项由R_C 的 点来解释，也就是说，非正式地通过函数在C中接受一个延续参数，并在R中返回一个结果。功能性术语（即D的一个点）表示为（RC）RC=RC×RC，函数的连续变元也是C的一个点RC. 它表示由后面的延续（在C中）和作为函数参数的项（在RC中）组成的对。这就是为什么我们可以将延续看作参数的堆栈，而将延续模型中的术语解释看作堆栈抽象机器中的过程正如我们之前所看到的（第二节）。2.1），λC-演算的延拓不应该仅仅是一个参数栈，而是由一个情况绑定（即一个点）的Dn）和堆栈（即，满足堆栈方程的某个对象S的点）。 这就产生了以下定义。定义3.5（延拓λC-模型）CCC是延拓λC-模型（或经典λC-模型），如果它有四个对象R，C，S5和D满足以下方程：D=RC;C=Dn×S;S=D×S在下一节中，我们证明了每个连续λC-模型实际上是一个在Def意义下的λC模型3.1. 可能描述变形有点乏味ismsapp，lam，c在延续模型中（还有更多的证明图换）与组成和curried形式;所以我们使用λ-演算用pairs（作为CCCs的内部语言）来定义那些态射。给定一个笛卡尔闭范畴C，我们称它的内部语言为λC-演算，并将C写为该语言中项的等价3.3从延拓λC模型到λC模型设C是一个连续λC-模型（定义3.5）。我们分别将这些项记为↑s、↓s、↑c和↓c。 S→ D ×S，D ×S →S，C → Dn×S和Dn×S →C）的对应4也称为经典模型，因为它们的底层逻辑是经典逻辑[10]。如果没有case复合，case上下文将不仅仅是一个case绑定（在Dn中），而是一个case绑定的堆栈。因此，我们需要第四个对象S′满足方程S′= DnS′，这样一个模型中的项的解释将更加复杂。B. Petit/Electronic Notes in Theoretical Computer Science 286（2012）337349.Σ我.Σ.Σ- 是的Σ‡‡.Σ到保证S_n=D×S和C_n=Dn×S的态射。我们表明C可以具有λC-模型的结构（定义3.1）。 为此，我们参考对于图中定义的λC项第六章术语Mlam、Mapp和Mcase具有免费的Mlam= λk。让我们|xθ，xπ| = ↑ck，令|x，xJπ| = ↑sxπin z x↓c|xθ，xJπ| ΔMapp= λx.λk. 让我们|xθ，xπ| = ↑ck in z↓c|xθ，↓sθ|x，xπ| ⟩| ⟩Mci= λk。让我们|xθ，xπ| = ↑ck，令|x1;. ; xn|在xikM的情况下= λk，让我们|xθ，xπ| =↑ck in让我们|yφ，y|= z in y ↓c| ⟨|M1，...，Mn|n，xπ|你好，其中Mi= λkJ。 让我们|zθ，zπ| = ↑ckJin让我们|x1;. ; xn|n= yφin xi↓c|xθ，zπ|M = λk。让我们|xθ，xπ| = ↑ck，令|x，xJπ| = ↑sxπin x↓c|⟨|x，...， X|n，xπ| ⟩图6.延拓λC-模型态变量z，它将对应于（通过从λC-演算到C的映射）lam的参数。app和case分别。请注意，图6中定义的术语与Sec的CPS 2（图3），假设|MθtMπ|λPt|Mθ，Mπ|- 是的定义3.6定义λC-模型的态射由以下可导出的判断给出：lam=z：D→DMlam：Dapp=z：DMapp：D→D c=Mc：Dcase=z：Dn×DMcase：D定理3.7（C是λC-模型）在一个连续λ C -模型的笛卡尔闭范畴C中，定义在Def. 3.6满足图中的图表 4，态射lam和app构成D与DD之间的同构. 也（C，D，app，lam，（c）n、，case）是一个λC-模型。i i=1草图（Sketch）所有态射上的等式都可以用内部语言证明：两个态射相等，如果它们对应的项是可转换的。例如，等式lam; app = IdDD 由λC-lam ;app的（即： λ z.Map p[z：=Mla m]）和λ z. z，并由λ z导出逆方程。Map p[z：=Mla m]Cλ z. z. 同样，图表的计算来自以下等价：λ z.Mcas e[z：=λ]|π1（z），Mc|Cλ z. πn（（π2（z）（D1）我我λ y。（Mapp[z：=Mcase[z：=π1（y）]]）π2（y）Cλ y。Mcas e[z：=0|π1 1（y），（Map p[z：=π2 1（y）]|π2（y）]（D2）λ y.Mcas e [z：=λ|M·π1（y），π2（y）|碳λ y。Mcas e[z：=0|π11（y），Mcas e[z：=π]|π2 1（y），π2（y）|]|（D4）λ y。MCλ y. Mcas e [z：=0|π1（z），M|（D3）350B. Petit/Electronic Notes in Theoretical Computer Science 286（2012）337我111n在（D4）的交换中，项M·对应于·，态射（IdDn×πn）的配对;情况：M·=λ z。⟨|Mcas e[z：=0|π（z），πn（z）|];. . . ;Mcas e[z：=0|π（z），πn（z）|]|乌恩Q3.4非句法λC模型虽然它是一个先验不容易构建一个λC-模型6（使用Def.3.1），一些著名的范畴实际上是连续λC-模型。事实上，每一个延续m odel（即，每个具有两个R和C的CCC，使得C=RC×C）都存在是一个连续λC-模型，如果我们（通过定义）S=C和D=RC：我们立即得到S=D×S，并且dC=RC×C =RC×（RC×C）=. . . n=（RC）n×C =Dn×S。推论3.8在具有两个对象R和C的 任 何 ccc 中 ， λ C - 演 算 都 有 一 个 合 理 的 解释， 使得C =RC×C。这是 一个好消 息，因 为我们知 道如何 构建这样 的数学结 构。特 别地，任 何Scott3.1]。请注意，相反地，每个延续λC-模型都是一个延续模型：C=Dn×S=Dn×（D×S）=（Dn×S）×D=C ×RC.通过将同构的这种分解插入到连续模型中纯lambda演算的通常解释中，人们实际上得到了在定义3.1中定义的态射lam和app。因此，使用这种同构将连续λC-模型转换为连续模型，然后解释其中的纯λ-项，相当于直接解释λ-项（参见作为λC-项）。结论和进一步的工作我们已经展示了如何在任何连续化模型中（例如在Scott域中）构造λC-演算的解释同构定义态射lam，app，c，case并解释λC-项如图3.6所示五、- 是的最后这项工作提出了几个问题。 第一个是关于λC-演算与Parigot [11]的λμ是否存在一个包含这两个变量的行为良好的微积分？这样的演算会特别有趣，因为λμ演算对应于经典逻辑，而数据结构上的模式匹配通常与构造性证明相关联[4]。第二个是关于lambda演算的范畴模型的完备性。事实上，λC-模型对于λC-演算是完备的，没有匹配失败（或者所有的匹配失败都被识别，如脚注p中所解释的。9）。那么，很自然地会问延拓λC-模型是否[6]部分等价关系范畴中的句法模型除外[12]。B. Petit/Electronic Notes in Theoretical Computer Science 286（2012）337351换句话说，是否每个λC-模型（特别是PERs的语法模型）都等价于连续λC-模型。如果不是，这些类别的内部语言是什么？也许是一种最后，类型化λC-演算的指称模型问题仍然悬而未决。这种演算的语法非常简单，但为它提出的类型系统[13]却不是。给数据类型一个分类定义似乎特别不容易（到目前为止，类型化演算的唯一指称模型是可归约候选的语法模型）。确认感谢Alexandre Miquel提出了双栈抽象机的概念，λC-演算，以及我们在这项工作上进行的所有富有成效的讨论。引用[1] ArielArbiser，AlexandreMiquel，andAlejandroR'ıos. 带构造函数的拉姆巴达演算：SynTax，Conquience和Separation。Journal of Functional Programming，19（5）：581[2] Horatiu Cirstea和Germain Faure。基于模式的微积分的一致性。在Franz Baader，编辑，RTA，计算机科学讲义第4533卷，第78-92页斯普林格。[3] Horatiu Cirstea和Claude Kirchner。作为elan语义的重写演算。亚洲，第84-85页，1998年[4] 蒂埃里·科昆德依赖类型的模式匹配。1992年6月，《证明和程序类型研讨会论文集》[5] 我是C 'egut。 一个抽象的局域网项规范化机。 在1990年关于LISP和函数式编程的A C M会议上，LFP'90，第333-340页，1990年。[6] Jean-Yves Girard，Yves Lafont，and Paul Taylor.证明和类型。剑桥大学出版社，1989年。[7] Martin Hofmann和Thomas Streicher。延拓模型是普适的延拓演算。LICS，第387-395页，1997年[8] 巴里·杰。模式演算：用函数和结构计算。Springer，2009年。[9] C. 巴里·杰和迪莉娅·凯斯纳纯粹的模式演算。见ESOP，第100[10] Yves Lafont、Bernhard Reus和Thomas Streicher。继续语义或用否定来表达隐含技术报告，慕尼黑大学，1993年。[11] 米歇尔·帕里戈。 Lambda-my-calculus：An algorithmic interpretation of classical natural deduction. 在LPAR，第190-201页[12] 芭芭拉·佩蒂特带构造函数的lambda演算的分类模型。http://arxiv.org/abs/1202.4678，2011。[13] 芭芭拉·佩蒂特带构造函数的类型化演算的语义。计算机科学中的逻辑方法，7（1：2），2011。[14] 戈登 D. 普洛特金按名称调用、按值调用和微积分。Theoretical Computer Science，1（2）：125[15] Bernhard Reus和Thomas Streicher。经典逻辑、连续语义和抽象机。Journal of Functional Programming，8（6）：543[16] 戴娜·斯科特。计算的数学理论概要。技术报告，普林斯顿大学，1970年。