1 π-序列的实数计算及有效性证明

第1章第1章可在www.sciencedirect.com在线获取理论计算机科学电子笔记298（2013）383-402www.elsevier.com/locate/entcs实数计算寺山庆一 Tsuiki2京都大学日本京都摘要本文提出并研究了1 π-序列的一种演算XPCF，1 π-序列是{0，1，π}的无限序列，至多有一个拷贝的底.它在实数计算中有应用，因为单位区间I是一个拓扑嵌入在1个序列的集合<$ω中的实函数和一个关于I的实函数可以写成程序其输入和输出1个π序列。 在XPCF中，我们定义了一个关于ω的函数仅通过指定其第一个数字是0和1的情况下的行为然后，通过取通过用0和1填充底部获得的序列的值的交集来计算从底部开始的序列的值这个演算的归约规则的有效性是由域理论语义的充分性定理证明的一些例子程序，包括加法和乘法显示。XPCF和相关语言的表达能力也进行了研究。保留字：底部，流，实数计算，域模型，PCF，充分性，并行或1介绍流是一种用于表达无限序列的有用数据结构，可以通过带符号的数字扩展[1，2]或实数的其他扩展[6]来实现流的实数计算。然而，由于流只能从左到右单向访问，如果存在底部，即，一个在流中其求值不终止的项，那么当程序试图读入底部单元格的值时，它就卡住了，并且不能输入序列的其余部分，尽管它可能包含有价值的数据。通常，底部被认为是一种编程错误，在正确的程序中应该然而，众所周知，可能包含底的无限序列在表示连续拓扑空间时是有用的，如1Email：t e rayama@i. H. 你好。阿正杰2Email：tsu iki@i. H. 你好。梭JP1571-0661 © 2013 Elsevier B. V.在CC BY-NC-ND许可下开放访问。http://dx.doi.org/10.1016/j.entcs.2013.09.023384K. 寺山湾Tsuiki/电子笔记在理论计算机科学298（2013）383第1章a，n第1章R.在这里，我们称一个最多只能包含一个bottom拷贝的无穷序列为1 π-序列。在[8]和[15]中表明，R和I =[0， 1]可以是拓扑地嵌入到空间<$ω中对于{0， 1}，在[15]中，这种嵌入被称为格雷嵌入R的符号数展开和其他可接受的表示在无限多个实数中的每一个都满足被无限多个码表示的性质的意义上是冗余的[4，17]。另一方面，通过格雷嵌入，可以通过用至多一个拷贝的实数扩展代码空间来为每个实数分配唯一的代码。文[ 16 ]中的嵌入结果推广到其它拓扑空间，并证明了任何n维可分度量空间都可以拓扑地嵌入到空间中n个序列。[8]将1 π-序列表示为从Nπ到{-1，1，π}的函数，并使用并行if算子pif来访问1π-序列，并表明实数算法-Rithms可以用PCF +pif表示。为了评估pifL M N，需要并行地评估L、M和N。因此，PIF操作符导致所有部件的爆炸，并且使效率降低到最低。MartinEscard'o提出了Real PCF[6]，它是PCF的实数扩展。它是基于区间域的，并使用了一种并行的条件算子另一方面，[15]将双头数限制为1，并引入了一种IM2机器（IndeterministicMultiheads Type2 Machine），它可以扩展流访问1个双头序列。然而，IM2机器的行为需要通过一组重叠规则来指定，因此可用IM2机器表示的函数通常是多值函数。此外，IM2机的程序是复杂的，因为需要表达其行为，用于来自额外头的输入。本文介绍了一种1阶序列的演算XPCF，用它可以表示对1阶序列的扩展流访问它是PCF的一个扩展，数据类型为1 π-序列的S，并且基于1 π-序列的代数域BD[16]。除了构造函数0：S→S和1：S →S之外，数据类型S还具有在一个序列前加上一个数字，构造函数0：S→S和1：S→S插入一个数字作为序列的第二个元素。然而，S上的函数通过仅在参数具有0N和1N的形式的情况下表达其行为来定义，其中表达式<$0x→M0; 1x→M1 <$。 它的意思是一个关于<$ω的函数toapply[[λx. M0]]如果该规则项为0，则可以将[[λx. M1]]如果一个数组为1，且为PP，如果参数是s，则两者都到s，并取结果之和。 XPCF可以被认为是Real PCF的代数域变体。这种演算相对于其域理论模型具有计算充分性。通过Gray嵌入给出了XPCF的一些例子程序，包括I上的加法和我们还研究了这种语言的表达能力，并表明XPCF具有与PCF +pif相同的表达能力。不包含S的类型，BD的所有可计算元素都可以在类型S上表达，如果我们用XPCF操作符扩展XPCF，那么所有可计算元素都可以在语义域中的元素是可表达的。如[7]所示，任何适合于区间的实数演算都-K. 寺山湾Tsuiki/电子笔记在理论计算机科学298（2013）383385第1章⊥⊥⊥55443 32 21 10.0 0.51.0二进制扩展0.0 0.51.0Gray扩展Fig. 1. I的二进制和格雷展开主模型，其中可以表示平均函数，没有顺序约简策略。他们的证明也适用于我们的模型与一些修改，因此任何顺序约简策略的演算是不适当的。设计了一种XPCF的顺序约简策略，并用Haskell实现了该策略。虽然它是不够的，有些条款不能减少到他们的外延，它顺序评估许多条款，如加法和乘法。在下一节中，我们首先解释I在ω中的Gray嵌入和1 π-序列的BD结构域。在第3节中，我们定义了XPCF的语法和语义，在第4节中，我们通过一些程序示例展示了如何在XPCF中表达实函数第五节给出了XPCF的约简规则，第六节给出了XPCF的充分性。在第7节中，我们研究了表达性XPCF的力量记法：回想一下，我们修复了={ 0， 1}。我们用Γω表示特征标集Γ的有限序列的集合，用Γω表示 Γ的无限序列的集合。我们定义了一个Scott域，即：有界完备ω-代数DCPO。令={}，且ω是无穷序列的集合。阿维尼翁由排序0和排序1生成的顺序。 在ω上，我们将阶定义为如果s（n）≠ t（n），则对每个n.（ω，ω）是Scott域。我们定义ω={s ∈⊥ω|s最多包含一个{}。第1章2实数计算与1 π-序列2.1灰度嵌入格雷展开是I作为无穷序列的展开，它不同于普通的二进制展开[15]。它基于格雷码[10]，这是一种与二进制码不同的自然数编码。图1显示了I的二进制和格雷展开。在x的二进制展开式中，展开式的头部h指示x是在[0，1/2]中还是在[1/2，1]中，并且尾部是f（x，h）的展开式，对于f，函数定义为：Σ386K. 寺山湾Tsuiki/电子笔记在理论计算机科学298（2013）383第1章第1章第1章第1章⊥第1章第1章⊥第1章⊥2x（如果h= 0）f（x，h）=.2x− 1（如果h= 1）因此，对于二进制展开，1/ 2展开的尾部取决于头部字符h的选择，而1/2有两个展开1000.0111On另一方面，Gray展开式的头部与二元展开式的头部相同，而尾部是t（x）的展开式，其中t是所谓的帐篷函数：1/2x（0≤ x ≤ 1/ 2）t（x）=0.2（1− x）（1/ 21/ 2）格雷嵌入是从I到ω的函数，定义为ω（x）（n）=P（tn（x））（n = 0，1，. . . ）.R在{−1，1}ω中的嵌入在[8]中由Gianantonio独立地定义Gray嵌入本质上与他对I的嵌入的限制相同。我们称1阶序列<$（x）为x的修正Gray展开式。灰色嵌入π实际上是一个拓扑嵌入，其拓扑为πω的Scott拓扑的子空间拓扑2.21π-序列的整环我们解释了1 π-序列的域BD[16]。让我们是有限的1次方的集合，的序列。 这里，p ∈<$是<$的有限1 <$-序列，如果<$至多出现在p中有一次，并且n不是p的最后一个字符。我们有一个={，0，1，0，1，.}其中，空序列是空序列。 我们可以把它看作是作为ω的子集通过识别其中p ∈<$ω∈<$ω。 我们定义BD=BD∪Σω，这是一个斯科特子域100，1美元第1章第1章具有最小元素<$BD=<$的<$ω，如图2所示。对于c ∈f，我们还表示K. 寺山湾Tsuiki/电子笔记在理论计算机科学298（2013）383387䃨䌥䎹㻘㻝㼧䃨㻜䃨 䃨䃨㻜㻝㻜 㻝㻝㻜㻝㻜䎹㻝㻜䃨第1章第1章第1章第1章⊥⊥第1章㼧··································䌥䠆䎹㻘㻝·················㻜㻜 㻜䎹㻜 㻜 䎹㻝㻜㻝 䎹㻜㻜 䎹㻜㻝 䎹㻝㻝 䎹㻝㻜㻝㻝㻝 䎹㻜 㻝 䎹㻝 㻝㻜㻜䎹㻜䎹 㻝㻝䃔ᵪᵰᵢ㼧ω······································㻜㻜㻜 㻜㻜䎹 㻝 㻜㻜㻝 㻜䎹 㻝㻜㻜㻝㻝 㻜㻝䎹 㻝 㻜㻝㻜䎹㻝㻜㻜 㻝㻝㻜 㻝㻝䎹㻝㻝㻝㻝 㻝䎹㻝㻜 㻝㻜㻝 㻝㻜䎹㻝㻝㻜㻜㻜㻜㻜䎹㻝 㻜㻝 䎹 㻝㻜㻝㻝㻝䎹㻝㻝㻜㻜䎹㻝㻝䃔ᵠᵢᵰᵢ图二. 结构域BD图3. 域名RD通过c从BD到BD的连续函数来前置c，并通过c表示从BD到BD的连续函数，插入c作为第二个字符，其中c（n）被定义为n c。我们有方程b <$c=c <$b，其中b，c ∈c。我们认为每个有限序列s = d0d1. . . dn−1of {0，1，0，1}表示该线性项td0（d1（. . . （dn−1（）of每个无穷序列s = d0d1. . . 的{0，1，0，1}表示等式（sn）n=0，1，. 在BD对于sn=d0（d1（. . . （dn−1（n）。不要让它成为一种无形的东西，. 特别是这个等式是ceb0b1。 . . bm−1c0c1. . . cn−1repres entsb0b1. . . bm−1<$c0c1。 . .cn−1∈N（orb0b1. . . bm−1ifn=0），且该inf inite eqnceb0b1。 . . bm−1c0c1. . .representsb0b1. . . bm−1<$c0c1。 . . ∈ω。由于BD是Scott域，因此满足（即， 最大下界）存在于BD的任何子集。我们显式地显示它，因为它在XPCF的语义中起着重要的作用第一，显然定义了在{0， 1，n}上的满足是自然地延伸到满足sω t in ωas（sω t）（n）=s（n）<$t（n）。让⊥⊥⊥trunc是来自ω到BD以截短第二次测序后的序列如果一个序列包含多个拷贝，则它构成一个有限的1 π-序列，并返回自己，如果没有。命题2.2s，t ∈BD的交sω t）。我们定义了BD的子域RD，用于通过Gray表示来表示I我们定义RD={p ∈ 10 n：p ∈ N，n ∈ {0，1，. . . ，ω}} ∞.这是一个斯科特域。 设LRD是nω的子集{p < $10ω：p ∈ n <$0} n <$0 ω. LRD是极限的集合（即，非紧凑）的RD元件，如图3所示。LRD由s ∈ S（I）和那些通过用0和1填充s ∈S（I）的底部而获得的序列组成我们可以看到I是LRD的一个收缩，并且I同胚于LRD的极小元集，其中收缩映射δ：LRD→I定义为δ（s）=x，如果δ（x）≤ s。可以看出三元组（RD，LRD，δ）是I在[3]意义下的收缩域表示，我们称映射δ：LRD→I为Gray表示。㻜㻜㻝㻜ω㻜㻝㻝㻜ω㻜㻝㻜ω㻝㻝㻜ω㻜䎹㻝㻜ωω䎹㻝㻜ω㻜ω㻝䎹㻝㻜䠍㻜388K. 寺山湾Tsuiki/电子笔记在理论计算机科学298（2013）383我们可以考虑基于Gray嵌入的I的两种编码 第一个是通过嵌入将x与（x）标识而获得的，另一个是Gray表示δ。例如，对于1/2 ∈I，<$10ω是唯一的码。 另一方面，对于δ的1/2，有三个码<$10ω，010 ω和110 ω。基于这些编码，我们有两个概念：BD上的函数实现I上的函数。定义2.3设F是从BDn到BD的函数，f是从In到I的（部分）实函数。(1) F精确实现F，如果，对于每个（ x1，.. . ，xn）∈dom（ f），F（x1），. . . ，n（xn））= n（f（x1，. . . ，xn））。(2) F实现f，如果，对于每个（ p1，.. . ，pn）∈（δn）−1（dom（ f）），δ（F（p1，. . . ，pn））= f（δ（p1），. . . ，δ（pn））。3XPCF的命名和指称语义在本文中，我们用无衬线字体写语法实体的类型和常量，用粗体字写程序名和语义域名。3.1PCF我们在表1中回顾了PCF语言的语法、语义和归约规则。见[11]或一些教科书，如[14]的PCF的细节。PCF的基类型为布尔值B和整数N对于项M，FV（M）表示M的自由变量，如果FV（M）为空，则M是闭的一个程序一种接地类型的封闭术语一个环境ρ是一个类型相关映射，S变量集{Dσ|σ type} and, for a ∈ Dσ ，ρ[a/xσ]是环境它将xσ映射到a，将任何其他变量yσ映射到ρ（yσ）。如果M是一个闭项，则[[M]]（ρ）不依赖于ρ，我们将[[M]]（ρ）写成[[ M ]]。PCF的操作语义由直接归约关系给出表1中程序M的评估结果是常数c，定义为：EvalPCF（M）=ciffMc.下面的定理通常被称为PCF的非线性性质。它断言操作语义和指称语义是一致的。定理3.1（[11，定理3.1]）对于任何PCF程序M和常数c，EvalPCF（M）=ciff[[M]]=[[c]]。3.2XPCF的语法和语义表2列出了XPCF的语法和指称语义。我们仅列出与PCF规范相比的差异它有一个接地类型S，K. 寺山湾Tsuiki/电子笔记在理论计算机科学298（2013）383389PCF的厚度类型：σ：：= B|N | σ → σ变量（类型为σ）：xσ：：= xσ，yσ，zσ，.常数：c：：=tt，ff，ifσ，Yτ，kn，inc，dec，zero（σ：ground type，τ：type，n ∈N）项：M：：=xσ|C|（MM）|（λxσ.M）打字规则：xσ：σ tt：B ff：B kn：N inc：N →Ndec：N→N零：N→B如果σ：B→ σM：τM：σ → τ N：σYσ：（σ → σ）→ σ λxσ.M：σ→τ MN：τPCF的指称语义域：DB：真值的平坦域{AB，tt，ff}DN：平坦域{N，0，1，.} 自然数。Dσ→τ：从Dσ到Dτ的连续函数的域[Dσ→ Dτ]，最小元素记为<$σ→τ。常数的解释[[tt]]=tt。[[f f]]=ff[[kn]]=n.n+1（n=/<$N）n−1（n≥1）[[inc]]=λn ∈ DN.[[dec]]= λn ∈ DN.<$N（n=<$N）<$N（n ∈ {<$N，0}）n=0。[[zero]]= λn ∈ DN. ff（n> 0） [[Yσ]]= λF ∈ Dσ→σ.n∈NFn（<$σ）B（n=N）（b=tt）[[ifσ]]= λb ∈ DB.λx ∈ Dσ.λy ∈ Dσ.（b= ff）⊥σ(b=⊥B)指称语义：(i)[[xσ]]（ρ）=ρ（xσ）（ii）[[c]]（ρ）=[[c]](iii)[[M N]]（ρ）=[[M]]（ρ）（[[N]]（ρ）） （iv）[[λxσ.M]]（ρ）= λa ∈ Dσ.[[M]]（ρ[a/xσ]）PCF的操作语义缩减规则：（λxσ. M）N<$M [N/xσ]YσM<$M（YσM） inckn<$kn+1 deckn+1 d e c k n +1d ecknzerok0ttzerokn+1d ffffσtMN <$MifσfMN<$NM <$M′N <$N′（如果M是if、inc、dec或零）M N<$M′N M N<$M N′σ表1PCF的语义和语义390K. 寺山湾Tsuiki/电子笔记在理论计算机科学298（2013）383PCF的扩展如下。公司简介类型：S常数：0、1、0、1条款：100xS→M; 1xS→M |1xS→M; 1xS→M打字规则：0：S→S 1：S→S 0：S→S 1：S →SM0：σM1：σM0：σM1：σ0xS→M0;1xS→M1XPCF的指称语义PCF的语义扩展如下。域：DS=BD常数的解释：[[0]] = 0∈ DS→S（其中0（s）= 0s fors ∈DS）[[1]] = 1∈ DS→S （其中1（s）= 1s fors ∈ DS）[[0]]= 0∈ DS→S（其中0（as）=a 0s fora ∈ DS，s ∈ DS，0（s）=0）[[1]]= 1∈ DS→S（其中1（as）=a 1s fora ∈ D S，s ∈ DS，1（s）=1）指称语义：（v）[[0xS→M0;1xS→M1]]（ρ）=⊥σ(ifs =ǫ)[[M]](ρ[s′/xS])(ifs=0s′)λs∈ DS。0[[M]]（ρ[s′/xS]）（如果s= 1s′）1<$[[M0]]（ρ[s′/xS]）<$[[M1]]（ρ[s′/xS]）（ifs=<$s′）（vi）[[xS→M0;1xS→M1xS]]（ρ）=[[M0]]（ρ[[[M]](ρ[s′/xS])(ifs=0s′)λs∈ DS。0[[M]]（ρ[s′/xS]）（如果s= 1s′）1<$[[M0]]（ρ[s′/xS]）<$[[M1]]（ρ[s′/xS]）（ifs=<$s′）表2XPCF的命名和指称语义DS=BD具有S → S类型的常数0，1，0，1，它们分别表示函数0，1，0，1。 对于类型为S的变量，为了简单起见，我们省略了类型，并将xS写成x。对于σ型的M0和 M1项，我们有S → σ型的函数项和。变量x是一个有界变量，它是由0x→M0;1x→M1x和0x→M0; 1x→M1x构成的。我们称之为广义条件检验，其中，M = 0x →M0; 1x →M1是广义条件检验. 对于这两个函数f0=[[λxS. M0]]ndf1=[[λxS. M1]]从DS到Dσ，K. 寺山湾Tsuiki/电子笔记在理论计算机科学298（2013）383391如果角元为0 s，则f=[[0xS→ M0;1xS→ M1s]]：DS→Dσr∈nsf0（s），如果角元为1 s，则f =f1（s）. 对于变元以f开头的情形，我们定义f（s）= f0（s）<$f1（s），它是f0（s）和f1（s）在Dσ中的交.在这里，DN和DB上的交被明确定义，D S上的交在2.2节中解释，并且两个函数g，h ∈Dσ→τ的交是逐点交函数（g<$h）（x）=g（x）<$h（x）。 Wedef inef（ε）=εσ。 但是，这是一个非常有趣的故事。 我们采用按值调用语义来处理一个应用程序，该应用程序的结构为：1x 0xS→M0; 1xS→M1。在此情况下，[nn0xS→M0;1xS→M1nn请注意，如果我们识别出和ω，并将s′与ω匹配，其中s′=，则0xS→ M0;1xS→ M1的语义的最后一种情况包含了第一种情况。在[[0xS→M0;1xS→M1阶]]和[[0xS→M0;1xS→ M1阶]]之间的函数不一定是连续的.我们引入两种扩展条件项的目的是在编写程序时使用了，而仅用于归约步骤，我们将在第5节中解释。我们称一个闭基型项为程序，如果它不包含扩展条件项的形式为S →0xS→M0;1xS→M1→ S。4XPCF的程序示例将第一位数反转的函数nh写为：nh= 100x→1x; 1x→0x 100。注意，对于s ∈<$ω，[[nh]]（<$s）= 0s <$1s =<$s。将第二位数反转的函数ns写为：ns= 10x→0（nh x）; 1x→1（nh x）n.下面的项head：S→B和tail：S→S是DS上的head和tail函数。head=100x→ff;1x→tt，尾= 100x→x; 1x→x。在这里，我们分别用ff，tt，B∈ DB标识0，1，∈注意，这里没有cons函数：B→S→S，因为如果我们在1-序列前加上，那么结果可能不是1-序列。反转所有数字的函数inv写为inv = YS→S（λfS→S. λ0x→1（f x）; 1x→0（f x）λ）.为了简单起见，我们使用递归定义符号来表示用Y运算符定义的项。例如，inv可以写成inv=0x→1（invx）; 1x→0（inv x）我们展示了实数和实函数是如何在XPCF中表达的。以来<$（0）= 0ω，<$（1）= 10ω和<$（1/2）=<$10ω，我们可以将这些数字表示为0=YS0，392K. 寺山湾Tsuiki/电子笔记在理论计算机科学298（2013）3831=1（YS0），1/2= 1（YS0）。在2.1节中，我们定义了BD上的函数（精确）实现I上的函数的概念。 我们说一个封闭的XPCF项（精确地）实现了一个实函数，如果它表示一个（精确地）实现该函数的函数。程序div2 = λxS。0x.实现了函数div 2（x）= x/2，但并没有完全实现它，因为[[div 2]]（10 ω）=010 ω，而<$（1/2）=<$10ω。也有一个程序，它完全实现了div2，这是后面给出的 由于补码函数comp（x）= 1 − x是通过将第一位数反转的函数来实现的，所以comp是通过程序nh来精确实现的。tent函数t由tail精确实现。实现加法（平均）av，减法sub，乘法的程序MULT和精确实现DIV2的程序DIV2B可以如下编写。av=100x→100y →0（avx y）;1y→1（ns（avx（nhy）n;1x→ 100y→1（ns（av（nhx）y））;1y→1（avxy）sub=0x→0y→0（subx y）;1y→YS0 y;1x→0y→nh（avx y）;1y→0（suby x）mult=100x→ 100y→0（0（multx y））;1y→0（multx（1y））n;1x→100y →0（mult（1x）y）;1y→av（nh（avx y））（1（nh（mult（nhx）（nhy））））div2b=0x→0（0x）;1x→1（fx）f=0x→0（fx）;1x→0（1x）这里，[[f]]是满足[[f]]（0ω）=<$0ω和[[f]]（x）= 0x的函数，如果x包含特征1。5XPCF的操作语义5.1XPCF的操作语义表3显示了XPCF的归约规则。对于d∈ {0，1，0，1}，我们说一项如果M约化为dM′，则S型的M输出d。我们解释了项<$0x→M0;1x→M1 <$N的约化是如何进行的。规则（COND0）、（COND1）、（COND0）和（COND1）的第一行是用于应用项<$0x→ M0;1x→M1<$N的约简。注意，如果[[N]]不被下一节中的充分性定理所证明，则闭项N被（APP-R）约化为这四种形式之一。如果N的形式为0N′，则应用（COND 0），并且新的形式为M0[0x/x]和M1[1x/x]。在此之后，M0和M1仅由（左）和（右）用x的第一个字符为0的附加信息来评估。如果M0[0x/x]不存在x，则M0[0 x/x ]也存在x，因此，预期该评估在其需要K. 寺山湾Tsuiki/电子笔记在理论计算机科学298（2013）383393XPCF约化规则除了PCF的归约规则外，我们还有以下规则。（COND0）<$0x→M0;1x→M1<$（0N）<$M0[N/x]⟨⟨0x→M0;1x→M1⟩⟩(0N)⊲M0[N/x]（COND1）<$0x→M0;1x→M1<$（1N）<$M1[N/x]⟨⟨0x→M0;1x→M1⟩⟩(1N)⊲M1[N/x]（COND0）0x→M0[0x/x];1x→M1[0x/x]N⟨⟨0x→M0;1x→M1⟩⟩(0N)⊲⟨⟨0x→M0[0x/x];1x→M1[0x/x]⟩⟩N（COND1）0x→M0;1x→M1（1N）0x→M0[1x/x];1x→M1[1x/x]N⟨⟨0x→M0;1x→M1⟩⟩(1N)⊲⟨⟨0x→M0[1x/x];1x→M1[1x/x]⟩⟩N(OUT1）n =0x→dM0;1x→dM1n = Nn =d（n =0x→M0;1x→M1n = N）（d∈{0，1，0，1}）（OUT2）n =0x→b（cM0）;1x→b′（cM1）n =N n =c（n=0x→bM0;1x→b′M1n = N）（b，b′∈{0，1}andb=/b′）（OUT3）N）（b，c∈ {0，1}）（OUT4）N）（b，c ∈ {0，1 }）（OUT）c（c ∈ {tt，ff，kn}）(BAR)b（cM）<$c（bM）（b，c∈ {0，1}）（PERM）0x→M0; 1x→M1NL⊲0x→M0L;1x→M1L⟨⟨0x→M0;1x→M1⟩⟩N L⊲⟨⟨0x→M0L;1x→M1L⟩⟩N(Ifx∈FV（L），然后重命名绑定变量x以避免变量冲突。（左）M0M′0⟨⟨0x→M0;1x→M1⟩⟩⊲⟨⟨0x→M′;1x→M1⟩⟩0（右）M1M′1⟨⟨0x→M0;1x→M1⟩⟩⊲⟨⟨0x→M0;1x→M′⟩⟩ 1（APP-R）N<$N′（如果M是0，1，0，1，<$0x→M;1x→M <$0或<$0x→M;1x→M <$0）MN<$MN′0 1 0 1表3 XPCFvalueoffx. 因此，（BAR）规则用于将M0[0x/x]和M1[0x/x]的输出变换为形式b0b1。. . bkc0c1. . . cj对于bi，ci∈ {0，1}。在那之后，如果他们在第一个或第二个数字，然后按照规则（OUT 1）到（OUT 5）输出，并重复它，直到没有更多的输出是可能的。因此，我们得到一个术语，表格d0d1。. . di（n =0x → M′; 1x → M′n = N′），我们可以继续这个过程，0 1子项0x → M′;1x → M′N′与（APP-R），因为所有规则适用于0 10x→M0;1x→M1N。可以看出，上述减少过程未能减少对于M 0和M 1函数类型项，n 0x→M0; 1x→M1n n N L，并且[[N]]= n s，因为L394K. 寺山湾Tsuiki/电子笔记在理论计算机科学298（2013）383的输出不能馈送到函数项M0和M1。 用于评价K. 寺山湾Tsuiki/电子笔记在理论计算机科学298（2013）383395这个术语，我们需要（PERM）规则。 设M 0x→M0; 1x→M1x：S → S → S，M0和M1是形式为M 0y →. ;1y →. - 是的我们首先用（PERM）规则将项<$0x→M0; 1x →M1<$NL约简为<$0x →（M0L）; 1x →（M1L）<$N，然后按我们解释的那样约简它。（PERM）规则对应-将λ项（λx.M）NL约化为（λx.M）NL。（ML））N，并且它类似于证明理论中用于证明规范化的置换转换规则[12]。有人可能会问，为什么我们要区分0x→M0;1x→M1和0x →M0;1x→M 1因为如果我们用后者然而，严格的<$0x→M0;1x→M1<$在编写递归定义的函数中起着重要的作用S上的许多函数用Y算子定义为F = YS→S（λf.M），其中M=0x→M0; 1x→M1<$，并将其约化为M[YS→S（λ f . M） ]。M ）/F]，其中不能以任何方式进行。如果M=λf0x→M0;1x→ M1λf，则YS→S（λf.M）在M0和M1中的副本可按规则约简（左）和（右），因此即使没有参数给函数项F，它也会导致无限计算。5.2XPCF的一种顺序策略尽管需要并行地评估M0、M1和N，以评估M=0x→M0; 1x→M1 N，我们上面提到的过程几乎是顺序的，因为M0和M1的求值预计会终止，因为它们在许多情况下包含自由变量x。 在某些情况下，M 0的求值不会终止，它会输出无穷多个数字。然而，如果M0具有d0d1M′的形式，那么，从（OUT 1）到（OUT 4）的形式，可以认为M0具有足够的输出以使M进行输出并终止其归约并进行M 1的评估。我们还需要注意M0具有形式m00;1y →M11mL的情况。 在这种情况下，如果我们根据我们上面提到的过程，L减少到0L1电话：021-88888888⊲∗···⊲∗0nLn 你好，例如，然后重复（COND0）的应用而不实例化N到X的输出。然而，我们可以通过定义以下内容来处理许多情况：如果M00和M11不能约化，并且y在M00和M11中的所有出现都具有c0c1的形式，则L不能约化。. . 对于k> 1和ci∈{0，1}。 注意，在这种情况下，y的进一步数字不会改变以下情况：M00不能减少。在此基础上，设计了XPCF的序贯约简策略。我们用Haskell实现了它正如[7]中所证明的，在区间域模型中，一个适当的实数演算，其中平均函数是可定义的，没有连续的减少策略。在我们的模型中也是如此，这种顺序策略是不够的。 因此，它不评估所有项 其外延。然而，我们观察到第4节中的术语的应用随着我们的实现而减少，我们期望它评估许多396K. 寺山湾Tsuiki/电子笔记在理论计算机科学298（2013）3836XPCF的计算充分性我们证明了XPCF的可靠性和完备性。我们首先表明，两种替代的减少规则的XPCF保持意义。引理6.1（i）对于项M：τ和N：σ，变量xσ和环境ρ，[[M [N/xσ]（ρ）=[[M]]（ρ[[N]]/xσ]）。（ii）对于项M和b ∈ {0，1，0，1}，[[M [bx/x]（ρ）=[[M]]（ρ [[b]]ρ（x）/x]）.证据 通过对M.✷根据引理6.1，下面的命题成立。命题6.2对于XPCF项M，N和环境ρ，如果M<$N，则[[M]]（ρ）=[[N]]（ρ）。证据 证明了对于每一条约简规则，其左右两边的指称语义是一致的。✷在PCF中，σ型程序M的求值结果是σ型常数，如果它存在的话。另一方面，在XPCF中，我们考虑将{0，1，0，1}中的数字输出为M的非终止计算。. . d0（d1···（dn−1M′））<$。. . .注意，序列d0，d1，不是唯一由M决定的。 比如说，对于λ S = YS →S（λx S .x S），项M =<$$> 0x → 0（Y 0）; 1x → 1（Y 0）<$$>（1 <$S）被简化为形式为10nM′和0nN′的项。然而，根据命题6.2，如果M≠d0 （ d1··· （ dn−1M ′ ） ） ， 则 新 的 w 具 有 d0 （ d1. （ dn−1<$ ） ） <$d0 （ d1（dn−1[[M′]]））=[[M]]，因此输出由M的符号[[M]]限定，并且具有最小的上界。因此，我们定义一个从σ型XPCF程序到Dσ元素的评价函数Eval如下。定义6.3（i）对于类型N或B的XPCF程序M，我们定义：.评价（M）=[[EvalPCF（M）]] 如果EvalPCF（M）x是，否则的话。(ii)对于类型S的XPCF程序M，我们定义.Eval（M）= {d0（d1. （dn−1（）|Md0（d1···（dn−1M ′））forsomeM ′}其中di∈ {0，1，0，1}且di=[[di]]，其中0 ≤ i q[M′]，使得p <$q。如果存在约简序列M[s[S]/x]q[M′]，则通过忽略与约简有关的约简，存在约简序列M[s[x]/x]q[M′′]。 因此，M[s[x]/x]输出q，使得p ≠ q。✷命题6.7每个XPCF项都是可计算的。证据 我们证明了它的结构归纳条款。为了证明Yσ对于XPCF类型σ的可计算性，我们使用了[11]中句法信息序的一p ∈πp ∈πq∈398K. 寺山湾Tsuiki/电子笔记在理论计算机科学298（2013）383个扩展，这里我们省略了它。本文仅对0，1，0，1，0，0，1，0，0，1，0，0K. 寺山湾Tsuiki/电子笔记在理论计算机科学298（2013）383399第1章第1章第1章第1章第1章第1章1第1章第1章第1章1.情况d∈ {0，1，0，1}。 我们证明，对于任何M型可S，dM是可计算的。 因为函数[[d]]：DS→ DS是连续的，对于任何∗第1章当p其中q[[M]]，p∈ [[d]]（q）。 由于M是可计算的，M输出q′∈<$$>，使得q <$q′。因此，dM输出满足p <$[[d]]（q）<$[[ d]]（q′）的[[ d]]（q ′），因此d是可计算的我们证明了如果σ型项M0和M1是可计算的，则σ 0x→M0;1x→ M1也是可计算的.当N1：S，N2，.时，a型基类型τ的m=0x→M=0;1x→M=1<$N1N2···Nn是可计算的，这是不可能的Nn是闭可计算项，M0和M1分别是闭可计算项对M0和M1的所有可查性的限制。我们只给出了τ=S的情形。Case[[N1]]=0. 根据规则，我们有以下几个等式：[[0x→M0;1x→M1<$N1N2···Nn]]=[[N0x→MN0;1x→MN1x]]（N）（[[N2]]）··