Type homogeneity is not a restriction for safe recursion schemes William Blum January 10, 2017 7 1 0 2 Abstract n Knapik et al. introduced the safety restriction which constrains both a thetypesandsyntaxoftheproductionrulesdefiningahigher-orderrecur- J sion scheme [10]. This restriction gives rise to an equi-expressivity result 9 betweenorder-npushdownautomataandorder-nsaferecursionschemes, when such devices are used as tree generators. ] We show that the typing constraint of safety, called homogeneity, is O unnecessary in the sense that imposing the syntactic restriction alone is L sufficient to provetheequi-expressivity result for trees. . s c [ 1 Introduction 1 v The conceptofsafety wasintroducedby Knapiket al. inthe contextofhigher- 8 orderrecursionschemesandstudiedfurtherin[10,7]. Intheoriginalpaperthey 1 show that, when used as tree generators, safe recursion schemes are equivalent 1 tosafe pushdownautomata[10]. Inits originaldefinition, safetyconsistsoftwo 2 fairly technical constraints: 0 . 1 1. Type-Homogeneitywhichimposesatype constraintonthe rulesofthe 0 recursion scheme; 7 1 2. A syntactic restriction on the relative order of sub-terms occurring in : v the right hand side of the recursion scheme rules. i X Knapik et al.’s result begged a question: what is the automaton equivalent r of ‘unsafe‘ recursion schemes? This question was answered a few years later a in a paper introducing a new kind of automata called Higher-Order Collapsi- ble PushdownAutomata(CPDA), whichis shownto be equivalentto (possibly unsafe) higher-order recursion schemes [9]. More specifically they describe an algorithm that, given an order-n recursive schemes G, constructs an equiva- lent order-n CPDA (in the sense that they both generate the same tree), and conversely. We will refer to them as the HMOS transformation procedures. The safety restriction was further studied in the context of the lambda cal- culus in the author’s D.Phil. thesis [2]. Somewhat surprisingly, in the lambda calculus setting, the type-homogeneity constraint is not necessary to define a useful calculus. One can define a notion of safe simply-typed lambda calculus by imposing solely the syntactic constraint above, that we name ‘incremental- binding’,ontothestandardsimply-typedlambdacalculus. Theauthor’sD.Phil. 1 thesisgivesexpressivityresultsandpresentsafully-abstractgamemodelforthis calculus [2]. This paper reconciles the above observation made in the lambda calculus with higher-order recursion schemes: we show that if a recursionscheme meets thesyntacticcriteriaofthesafetyrestriction,thenregardlessofwhetherthetype homogenityismet,theautomatonconstructedusingtheHMOSprocedurefrom [9]canbe convertedinto anequivalentorder-n(non-collapsible)push-downau- tomaton (PDA). Conversely, given an order-n PDA, the recursion scheme gen- eratedbytheHMOStransformationinducesanequivalentincrementally-bound andhomogeneously-typedrecursionscheme. Consequently,forgeneratingtrees, pushdown automata are just as expressive as incrementally-bound recursion schemes. (In what follows, by abuse of language, we will use “incremental- binding” to refer to the syntactic constraint 2. above, even though the concept of binders is foreign to recursion schemes.) Further, composingthe above two transformationsyields a methods to con- vert any incrementally-bound recursion scheme into an equivalent safe one in the original sense (i.e., incrementally-bound and type-homogeneous). Type- homogeneity is therefore not a proper restriction for safe recursion schemes. This generalizes Knapik et al.’s result on equi-expressivity of pushdown au- tomata and safe recursion schemes [10]. Remark 1.1. The resultpresented inthis paper wasprivately circulatedfor the firsttimein2009andsharedonmypersonalwebsitebutwasneverpublishedin ajournalorconference[3]. Theresultwasfirstconjecturedintheauthor’sthesis in [2]. A partial proof was then privately circulated by the author in a 2008 note. Based on this note, Broadbent [5] adjusted the definition of stack safety to make the inductive proof work, which filled the remaining gap in the proof. The author thencirculatedanupdated proofbasedonyetanotherdefinitionof stack safety which is also the one used in the present paper. 2 Background We first recall some basic notations and recall the definition of higher-order automata and higher-order recursion schemes from the literature [10, 8]. Weconsidersimpletypesoverasingleatomo. WecallΣaranked alphabet if each symbol f ∈ Σ is assigned a type of the form o −→ ··· −→o −→ o. We write arity(f) for any typed-term f to denote the arity of its type. Given a set of typed symbols S, the set of applicative terms generated from S, is defined as the closure of S under the application rule: if m and n are twoapplicative terms of respective type A→B and A then (mn) is also an applicative term of type B. A Σ-labelled tree is a possibly infinite tree where each nodes of the tree is labelled with a symbol in Σ with arity matching the number of children nodes in the tree. 2.1 Higher-order stacks and recursion schemes Higher-orderstacks Thenotionofhigher-orderstacksisdefinedinductively. We first fix the base alphabet as a finite set Γ. An order-1 stack over Γ is a 2 sequence of elements of γ ∈ Γ∗. For n ∈ N an order-(n+1)-stack is defined as a stack of order-n stacks. The order of a stack s is written ord(s). The ith elementsinastacks,fori≥0,isdenoteds sothatastacksconsistsofordered i elements s , ... s where k ≥0 is called the length of the stack. The stack can 1 k then be represented by the notation [s ,···s ]. The first element s and last 1 k 1 element s are respectively called the ‘bottom’ and ‘top’ elements of the stack. k The empty stack of order 1 is denoted ⊥ and represent the stack consisting 1 of no element. We then define the empty (n+1)-stack ⊥ as the singleton n+1 sequence [⊥ ]. n The following operations are defined for an order-1 stack s: pusha[s ···s ] := [s ···s a] 1 1 m 1 m pop [s ···s s ] := [s ···s ] 1 1 m m+1 1 m and for an order-(n+1) stacks t: push [t ···t ] := [t ···t t ] n+1 1 m 1 m m pop [t ···t t ] := [t ···t ]. n+1 1 m m+1 1 m The top of a stack for i≥1 is defined as the top (i−1)-stack of s (so that i pop returnsswithitstop(i−1)-stackremoved). Formally,fors=[s ···s ], i 1 l+1 l≥0 and 1≤i≤ord(s): s if i=ord(s) top [s ···s ] := l+1 i 1 l+1 (topisl+1 if i<ord(s). Following[9],wedefinethenaturalnotionofstackprefix: foragivenn-stack s, for any lower-level stack m occurring in s, the prefix s of s at m consists 6m of the stack obtained from s by removing all the elements ‘above’ m using a succession of ‘pop‘ operations. Formally: Definition2.1(Stackprefix). Lets=[s ···s ]beahigher-orderstack. Then 1 m s is defined as [s ···s ] for 1 ≤ i ≤ m; and for a stack t occurring in s we 6si 1 i i define s as [s ···s ]. 6t 1 i6t Similarly we define the strict stack prefix s<s and s respectively as i <t [s ···s ] and [s ···t ]. 1 i−1 1 <si For any operation φ operating on a higher-order stack and k ≥1 we denote φk the repeated application of φ exactly k times: φk s=φ(···(φ s)···) with k application of φ for any stack s. Higher-order stacks with links We recall the notion of higher-order stack with links where each order-1 element is equipped with a link to another stack [8]: Definition 2.2 (Higher order stack with links (or CPDA stack)). For a stack alphabet Γ and a distinguished bottom-of-stack symbol ⊥ ∈ Γ. An order-0 CPDA stack is just a stack symbol. An order-(n+1) CPDA stack s is a non- empty sequence (written [s ···s ]) of order n CPDA stacks such that every 1 l non-⊥ symbol a that occurs in s has a link to a stack of some order k (where 0≤k ≤n) situated below it in s; we call the link a (k+1)-link. 3 An element of a higher order CPDA stack is written a(j,k) where a∈Γ and the exponent (j,k) encodes the pointer associated to the stack symbol. Think ofit asa shorthandforthe iteratedstack operationpopk (i.e., k applicationsof j pop ). The value j is called the order of the link, and k is called the height j of the link for 1≤j ≤n and k ≥1, such that if j =1 then k =1. Definition 2.3. Let s be a higher-order stack. We define shji as the operation thatreplaceseverylinkoccurringinsoftheform(j,k)with(j,k+1). Formally, a(j,k)hji =a(j,k+1) a(j,k)hj′i =a(j,k) when j 6=j′, [s ...s ]hji =[shji...shji] . 1 p 1 p Thisoperationclearlycommuteswithprefixing. Wewillthereforewriteshji 6m as an abbreviation for (shji) =(s )hji, for all stack s and stack-symbol m 6m 6m occurring in s. The top and pop operations are defined identically to standard higher-order stacks. The push operation is defined similarly to higher-order stacks except thatthe pushoperationnowassignsapointertoeveryelementpushedontothe stack. Also, in addition to the standard push and pop operations, the CPDA introduces a new collapse operation that ‘collapses’ a given stack to the target of the pointer associatedwith the top order-1 element in the stack. The idea is thatifthetop-1elementisasymbolawithalinktosome(j−1)-stack,thenthe collapse operation produces the same effect as successively performing k times the pop operation. j We reproduce here the definition of the push and collpase operations from [9]: Definition 2.4 (Higher-orderCPDAoperations). We defineCPDAoperations intermsofthestandardstackoperationsofanorder-nPDAwithanadequately defined alphabet encoding elements of the form b(o,h) where b ∈ Γ and link indices o,h≥0. For 1≤i≤ord(s) and 2≤j ≤ord(s): pushb,i s=pushb(i,1) s 1 1 collapse s=pophs where top s=a(o,h) o 1 [s ... s shji ] if j =ords; push [s ...s ]= 1 l+1 l+1 j 1 l+1 [s ... s push s ] if j <ords. (cid:26) 1 l+1 j l+1 s Convention 2.|1. In{zthe }rest of the paper we will adopt the following abbrevia- tions: • “pusha,j” for the operation push a(j,1); 1 1 • “pusha” for the operation push a(j,k) where the components j and k are 1 1 undetermined. Convention 2.2 (Topstackconvention). Intheoriginaldefinition,theoperation top , that returns the top (i − 1)-stack of a higher-order stack, removes any i dangling pointer resulting from the operation. Here, we suppose that top is i 4 defined in such a way that all pointers are preserved. From an implementation viewpoint, since links areencoded aspairs ofintegers,this means that top just i returns an unmodified copy of the top (i−1)-stack. Definition 2.5. A tree generatingorder-n collapsible pushdown automa- ton, n-CPDA for short, is a tuple hΣ,Γ,Q,δ,q i where Σ is a rankedalphabet, 0 Γ is a stack alphabet, Q is a finite set of states, q is the initial state, and δ is 0 a transition function Q×Γ−→Q×Op+Out where • Op denotes the set of operations on higher-order stacks with links from Definition 2.4.; • Out = {(f,q ,··· ,q ) : f ∈ Σ,q ∈ Q} denotes the set of possible 1 arity(f) i output emitted at each step of the transition function. An order-n CPDA stack is called a configuration of an order-n CPDA. This definition extends the notion of tree-generatingPushdown Automa- ton (PDA) which are similarly defined on regular higher-order stack with no links and without the collapse stack operation. Tree accepted by a CPDA/PDA One can think of a CPDA (resp. PDA) as a state machine equipped with a higher-orderstacks. At eachtransition,the CPDA can either (i) applies some operation to the stack and update its state, (ii) output the root node f ∈Σ of the generated tree together with new states foreachbranchofthetreeroot. Theinfinite tree acceptedbytheautomaton can then be obtained by recursively spawning new automatons at each child of the node starting with the specified state q . The formal definition of the i generated tree can be found in [10, 8]. Higher-order recursion schemes Definition 2.6. A higher-order recursion scheme is a tuple hΣ,N,R,Si, where Σ is a ranked alphabet of terminals; N is a finite set of typed non- terminals; S is a distinguished ground-type symbol of N, called the start symbol; R is a finite set of production rules. For each non-terminal F : (A ,...,A ,o)∈N there is exactly one rule ofthe form: Fz ...z →e where 1 n 1 m each z (called parameter) is a variable of type A and e is an applicative term i i of type o generated from the typed symbols in Σ∪N ∪{z :A ,...,z :A }. 1 1 m m We say that the recursion scheme is order-n just in case the order of the highest-order non-terminal is n. Tree-generated by a recursion scheme An applicative term generated from the terminal symbols Σ only (without non-terminals), is viewed as a Σ- labelledtree andcalledavalue tree. Arecursionscheme defines a(potentially infinite)valuetreeobtainedbyunfoldingitsrewriterulesadinfinitum,replacing formal by actual parameters each time, starting from the start symbol S. It is formally defined as the least upper bound of the induced schematological tree grammar inthecontinuousalgebraofrankedtreeswiththeappropriateordering [10, 7]. 5 Example 2.1. LetGbethefollowingorder-2recursionscheme: S → Ha g Hz → F (gz) a g F φ → φ(φ(F h)) a h with non-terminals S : o, F : ((o,o),o), H : (o,o) and h terminals g,h,a of arity 2,1,0 respectively. Then the tree ... generatedbyGisdefinedbytheinfinitetermga(ga(h(h(h ···)))) pictured on the right. 2.2 Computation tree Informally,the computation tree of a higher-orderrecursionscheme from [11]is definedasafinitetreerepresentationoftheη-long normal form ofthe(possibly infinite)lambdatermsinherenttotheproductionrulesoftherecursionscheme. Fix a higher-order recursion scheme R = hΣ,N,R,Si. Observe that pro- duction rules naturally map to simply-typed lambda terms by (i) currying the rule: replacingvariablesdefinedonthe left-handsidebyasuccessionoflambda abstractionsontheright-handside,(ii)interpretingterminalsandnon-terminal occurring in the applicative term of the right-hand side as free variables. Sup- posed that F : A → ··· → A ∈ N for some m ≥ 0. Then the rule 1 m Fz ...z →f(G(Fz )) corresponds to the simply-typed lambda-term: 1 m 1 λz ...z .f(G(Fz )) 1 m 1 oftypeA →···→A →owithfreevariablesf,F,Gofappropriatetype. For 1 m each non-terminal F we denote this term Λ(F). We recallthat a simply-typed lambda term is in η-long normal form if it can be written λx.s s ...s (where λx is an abbreviation for λx ...λx for 0 1 m 1 n somen≥0)wheres s ...s isofgroundtype,eachs forj ∈1..misinη-long 0 1 m j normalform, andeither s is a variable andm≥0; ors is anabstractionλy.s 0 0 for some η-long normal form s and m≥ 1. It is convenient to write the η-long normal form of terms of ground type as λ.N for some term N where ‘λ.’ is referred to as a ‘dummy lambda’. Observe that a purely applicative term can trivially be converted to η-long normal form by recursively η-expanding every subexpression. Wedefinethecomputationtreeofasimply-typedtermasanabstractsyntax tree of its eta-long normal form: Definition 2.7 (Computation tree of a simply-typed term ([2])). Let M be a simply-typed term of type T with variables names V. The computation tree τ(M) with labels taken from {@}∪V ∪{λx ...x | x ,...,x ∈V,n∈N}, is 1 n 1 n defined inductively on the η-long normal form of M as follows. τ(λx.zs ...s ) = λxhz hτ(s ),...,τ(s )ii 1 m 1 m where m≥0, z ∈V, τ(λx.(λy.t)s ...s ) = λxh@hτ(λy.t),τ(s ),...,τ(s )ii 1 m 1 m where m≥1, y ∈V. wherelht ,...,t iforn≥0succinctlydenotesalabelledtreewithrootlabelled 1 n landnorderedchildrentreest ,...,t . Theunderlinedexpressionscorrespond 1 n to the nodes of the tree for m>0, and leaves for m=0. 6 We borrow terminology from the lambda calculus when referring to the computation tree. In particular we will sometime refer to the ‘binder‘ of a variable node as the uniquely defined lambda node that binds the variable in the corresponding lambda term. Givenasimply-typedlambdatermM withfreevariablesinN∪Σ,wedefine theunfolding of M asthesimply-typedlambdatermM obtainedbyreplacing everyvariableN ∈N by the termΛ(N)using capture-permitting substitution. The unfolding ofthe computationtree τ(M) is defined as the computationtree of the unfolding of M. Definition 2.8. The (possibly infinite) computation tree of a recursion scheme R is defined as the recursive unfolding of the computation tree of the simply-typed term Λ(S). (An alternative definition can be found in [11].) Remark 2.1. The repeated unfolding operation does not incur capture of vari- ables since the lambda terms representing rewrite rules of a recursion scheme only have free variables in N ∪Σ, and leave all variables in N ∪Σ unbound. Incremental binding We recallthat the order of a simple type is defined as ord(o) = 0 for any base type o, and ord(A → B) = max(ord(A)+1,ord(B)). Wedefinetheorderofavariablenodeastheorderofitsassociatedsimpletype, and the order of a lambda node λx ···x for n>0 as 1+max ordx . 1 n 0≤i≤n i We now recall the following notion from the author’s thesis [2, 4] which relates to the syntactic restriction of safety: Definition 2.9 ([2, 4]). The computation tree of a closed lambda term is incrementally-bound if every variable node x is bound by the first lambda node in the path from it to the root that has order strictly greater than x. By extension, we say that the computation tree of an open term M with free variables x ,···x , n ≥ 0 is incrementally-bound if so is the computation 1 n tree of closed term λx .···λx .M. 1 n Weextendthisdefinitiontorecursionschemesthroughfinite approximation of the computation tree: a recursion scheme is incrementally-bound just if every finite unfolding of the tree is incrementally-bound. (Or equivalently, if every finite tree obtained by pruning some branches of its computation tree is incrementally-bound.) 2.3 The safety restriction The safety restriction has appeared under different forms in the literature [10, 6,7,2,4]. We include here a reformulationofthe definition by Knapiket al. in the setting of recursion schemes [10]. Definition 2.10 (Type homogeneity). We say that a simple type A −→ 1 ··· −→ A −→ o with n ≥ 0 is homogeneous just if ordA ≥ ordA ≥ n 1 2 ···≥ordA , and each A , ..., A is homogeneous [10]. n 1 n Definition 2.11 (Safe recursion scheme). Let G be a higher-order recursion scheme where the non-terminals all have homogeneous types. We say that G is unsafe just if it has a production rule Fz ...z → e where e contains a 1 m subterm that: 7 1. occurs in operand position in e, 2. contains a parameter of order strictly less than its order. By “operand position” we mean “in the second position of some occurrence of the term application operator”. A recursion scheme is said to be safe if it is not unsafe. Theterm‘safety‘comesfromthefactthat,whenconvertedtolambda-terms, saferecursionschemescanbe evaluatedwithouteverhavingtogenerateafresh variable during substitution: β-redexes can be reduced using (simultaneous) capture-permitting substitution [2, 4, 1]. The safe subset of the simply-typed lambda calculus introduced in [4, 2] relates to the notion of safe higher-order recursion schemes in the following sense: Proposition 2.1 (Safe rewrite rules and lambda terms [2, Proposition 3.11]). Take a recursion scheme R = hΣ,N,R,Si. For every non-terminal N, the associated rewriting rule is safe if and only if the simply-type term Λ(N), with free variables in Σ∪N, is derivable with the typing judgment of the safe lambda calculus of [2] and all types involved in the typing derivation are homogeneous. Itwasshownthatincremental-bindingcharacterizessafesimply-typedlambda terms [2, Proposition 5.11]. We show here the equivalent result for recursion schemes. Withoutlossofgeneralitywewillconsiderrecursionschemeswith no dead rule such that for every production rule, there exists a derivation from the start non-terminal involving that rewrite rule. Proposition 2.2 (Binder characterization for HORS). A higher-order recur- sion scheme with no dead rule is safe (in the sense of [10]) if and only if it is homogeneous and incrementally-bound. Proof. The proof reduces to the setting of the lambda calculus where a similar result was shown for finite lambda terms [2]. Take a safe recursion scheme R=hΣ,N,R,Si. (=⇒) Observe that all the iterated unfoldings of Λ(S) are safe homoge- neous simply-typed terms. It’s true of Λ(S) itself by Proposition 2.1. And by the Substitution Lemma [2, 3.19], it is also true of each subsequent un- folding. Consequently, by the characterization result of the safe-simply typed lambda calculus [2, Proposition 5.11](i), every repeated unfolding of Λ(S) has an incrementally-bound computation tree. Hence R is incrementally-bound. (⇐=) Assume that R is not safe. Suppose that it’s homogeneously-typed, then the syntactic constraint of safety is not met for some production rule Nx ···x → e ∈ R and non-terminal N ∈ N. Since the scheme has no 1 n dead-rule, after performing |N| unfoldings of Λ(S) the non-terminal N must have been substituted at least once by Λ(N)=λx ···x .e, which is unsafe by 1 n Proposition2.1. HenceafterafinitenumberofunfoldingsofS weobtainaterm t′ containing the unsafe subterm Λ(N). Thus, by [2, Proposition 5.11](ii), the computation tree t′ is not incrementally-bound. 8 2.4 Equi-expressivity results Now that we have defined the notions of tree-generating higher-order recursion schemesandtree-generatinghigher-orderautomatawecanstatetwoimportant results about their relative expressivity: Theorem 2.1 (Safe HORS - PDA equi-expressivity [10]). A Σ-labelled tree is generated by a safe order-n recursion scheme if and only if it is accepted by an order-n pushdown automaton. Theorem 2.2 (HORS - CPDA equi-expressivity [9]). A Σ-labelled tree is gen- erated by an order-n recursion scheme if and only if it is accepted by an order-n collapsible pushdown automaton. The proof of the HORS-CPDA equi-expressivity result is constructive in both direction: given a higher-order recursion scheme R, one can construct a collapsible pushdown automaton denoted CPDA(G) that recognizes the same tree;andgivenacollapsiblepushdownautomatonAonecanconstructahigher- orderrecursionschemerecognizingthe same tree. Inwhatfollows,we willrefer to them as the HMOS constructions. The following result summarizes the contribution of the present paper: Theorem 2.3 (Homogeneity is not a restiction). A Σ-labelled tree is generated byan incrementally-boundorder-n recursion schemeif andonlyif itis accepted by an order-n pushdown automaton. Section 4 gives a constructive proof of the implication by showing that the collapsible pushdown automaton CPDA(G) from the HMOS construction can be turned into an equivalent pushdown automaton (Theorem 4.1). Section 5 proves the opposite direction. 3 From recursion scheme to collapsible push- down automaton In this section we recall some of the concepts from the HMOS constructions from Theorem2.2. Familiarity with the originalconstructioncan be helpful, in particular for the concept of traversals. We refer the reader to [9] for a more detailed introduction to those concepts. We fix a higher-order recursion scheme G=hΣ,N,R,Si of order n. Let N denotes the set of nodes of the computation tree of G; N denotes the set of @ application nodes; N the set of lambda nodes; Nprime the set of lambda nodes λ λ that are the first child of some @ nodes (also known as prime lambda nodes); and N denotes the set of variables nodes. var Presentation Definition 3.1 (CPDA of G). We consider the order n collapsible pushdown automaton, obtained from G by the HMOS transformation defined in [9] and denoted CPDA(G) [8, Definition 5.2]. Recall that: • The ranked-alphabet is Σ (the alphabet of G); 9 • The stack-alphabetΓ ofthe automatonis takenas the set ofnodes of the computation graph of G. Alternatively, this graph can be viewed as the computation tree of Λ(S) by replacing back-pointers in the computation graphwithpointerstonon-terminalsnodesinthecomputationtree. Thus Γ=N; • The transition function δ of the automaton is shown in Figure 1 using a more concise definition than the original one from [8]; • The initial configuration is defined as c = push λ ⊥ where λ refers to 0 1 n the root (dummy) lambda node of the computation graph of G. The automaton is well-defined in the sense that no collapse can occur at an element whose link is undefined: In particular collapse never occurs at non- lambda nodes. It is equivalent to G in the sense that they both generate the same tree [9]. The idea is that automaton CPDA(G) proceeds by inductively computing a set of traversals over the computation tree of G. The traversals are shown to correctly evaluates the production rules of the recursion scheme G, therefore the constructed automaton correctly accepts the same tree as the recursion scheme. (At this point, readers not familiar with the concept of traversals over the computation graph of a recursion scheme, O-view and P-view may want to lookup their definitions in [11].) Observe that one can easily modify CPDA(G) into an automaton that “printsout”thetraversalthatisbeingcomputed. Thiscanbedonebychanging the behaviour of the push operation to make it print out the input element 1 before pushing it onthe stack. The justification pointers can then be recovered inductively using the node labels: For a variable node, it is the only node- occurrence that binds it in the P-view at that point (which is computable by theinductionhypothesis);primelambdanodesalwayspointtotheirimmediate predecessor; and a non-prime lambda node λx is always justified by the prede- cessor of the justifier of the variable node preceding it (written ip(jp(t)) where t is the traversalending with λx). Remark 3.1. Our presentationof δ differs slightly from the originalone: In the case (A), when pushing the prime child of an application node @ on the stack, we assign it a link pointing to the preceding stack symbol in the top 1-stack (i.e., the @-nodeitself). Thismodificationavoidsthecaseanalysisonthevalue ofj—thechild-indexofu’sbinder—inthecases(V )and(V ),andthesequence 0 1 of instructions popp+1 can just be replaced by popp;collapse. 1 1 The stack of the current configuration alone does not suffice to reconstruct the traversalthat is being computed due to the use of the “destructive” opera- tions collapse in the CPDA. Nevertheless, two important pieces of information are recoverablefrom the configuration-stack: the O-view and the P-view of the traversal. Proposition 3.1 (Recovering views from a configuration of CPDA(G)). Let c be a configuration of CPDA(G). The long O-view, O-view and P-view of thetraversalcurrentlybeingsimulatedbytheconfigurationc,writtenrespectively ⌊c⌋, xcy and pcq, can be retrieved using the following stack operations: 10