Huet, G. and Lang, B. Proving and Applying Program Transformations Expressed with Second-Order Logic. Acta Informatica 11 (1978) 31--55.  @ NUS  Home/Search   Document Not in Database   Summary   Related Articles   Check

....used as the syntactic representation of binding operators. Theorem proving is undecidable, but it is unfortunate that each resolution step is undecidable. We can recover decidability by restricting unification. Limiting the search gives unpredictable results. Second order matching is decidable [18], though second order unification is not [11] Perhaps first order unification plus second order matching is a practical compromise. Ketonen s EKL proves theorems using first order unification plus higher order matching. Ketonen claims that higher order matching is decidable, without proof [20] ....

G. P. Huet, B. Lang, Proving and applying program transformations expressed with second-order patterns, Acta Informatica 11 (1978), pages 31--55.

.... known since the invention of typed # calculi (see for the special case of the quantifiers in [25] it was not before the late seventies that the overall importance of higherorder abstract syntax (a term coined by [28] for the representation of binding in logical rules and program transformations [29] and for implementations [28] was recognized. The term shallow embedding (invented in [30] extends higherorder abstract syntax (HOAS) to a semantic definition and is contrasted to deep embeddings . Moreover, throughout this paper, we will distinguish typed and untyped shallow embeddings. ....

G. Huet, B.L.: Proving and applying program transformations expressed with second order patterns. (Acta Informatica)

.... known since the invention of typed # calculi (see for the special case of the quantifiers in [25] it was not before the late seventies that the overall importance of higherorder abstract syntax (a term coined by [28] for the representation of binding in logical rules and program transformations [29] and for implementations [28] was recognized. The term shallow embedding (invented in [30] extends higherorder abstract syntax (HOAS) to a semantic definition and is contrasted to deep embeddings . Moreover, throughout this paper, we will distinguish typed and untyped shallow embeddings. ....

G. Huet, B.L.: Proving and applying program transformations expressed with second order patterns. (Acta Informatica)

....terms, the application of a substitution to a term and the computation of a matching substitution are rather simple operations. Thus, a rewriting step itself is a rather simple operation. This is not longer true in the second order world, i.e. if the terms contain second order variables; see [4] where Huet and Lang present an algorithm to compute all principal matches for the second order case. For second order variables, substitution application incorporates fi reduction, and consequently matching may involve fi expansion. The research reported here was partially supported by SERC ....

G'erard Huet and Bernard Lang. Proving and applying program transformations expressed with second-order patterns. Acta Informatica, 11:31--55, 1978.

....x of P , we can treat x as an arbitrary constant from now on. The subgoal may now be rewritten as #= Find : i(name x, id x, age x) name x, if age x 30 then id x else 0) 8 To make further progress, we need the concepts of imitation and projection from higher order matching theory [12], embodied in the following rules: Imitation Rule Given g : B 1 . B n # C To Find: f u = g(v 1 , v n ) Solution: f = # x g(h 1 x, h 2 x, h n x) #= Find: h i u = v i for 1 # i # n Projection Rule To Find: f(a 1 , a k ) a i Solution: f = # k i = # ....

G. Huet and B. Lang. Proving and applying program transformations expressed with second-order patterns. Acta informatica , 11:31--55, 1978.

....of their bound variable exactly once, are considered. A context may be viewed as a linear second order function with one argument, where the binder is left implicit and the hole is the single occurrence of the bound variable. An algorithm for general second order matching is given by Huet and Lang [15]. Curien, Qian and Shi [8] give an algorithm for second order matching that improves eciency for the case of right hand sides with many bound variables and few constants. Second order and third order matching are NP complete [7] while fourth order matching is decidable but NEXPTIME hard [26] For ....

....and want to avoid exponential behavior we may remove equations x t and X [ t[ where x or X occurs only once in the problem. It is interesting to compare the working of our rules to the rules Simpli cation, Imitation and Projection that are used in the more general higher order cases [9, 15]. Simpli cation is essentially a Decompose with respect to a function symbol, while Imitate and Project together correspond to Variable Split. Applied to context matching they would construct a context step by step, Imitation would add a function symbol at the bottom and Project would put in the ....

Gerard Huet and Bernard Lang. Proving and applying program transformations expressed with second-order patterns. Acta Informatica, 11:31-55, 1978.

....and verify that P satis es suitable conditions. The schemata approach determines much more concise program derivations than the rules strategies approach, but the schemata approach has its drawbacks: i) the matching task is not always easy and in some cases matching may even be undecidable [HuL78], and (ii) the choice of the right schema transformation one should apply, often requires a deep insight on the program behaviour and may be dicult to mechanize. We have not described our list introduction strategy in full detail. Nevertheless, the reader may realize that each individual ....

G. Huet and B. Lang. Proving and applying program transformations expressed with second-order patterns. Acta Informatica, 11:31-55, 1978.

....higher and not just second order means the code is complicated and not easy to understand. It proved difficult to work with and so I decided to write my own special purpose second order mapping. If more time had been available I would have modified the second order algorithm of Huet and Lang [Huet Lang 78] but given the time constraints, I implemented a restricted algorithm of my own. The algorithm considers various cases outlined in Figure 5 1. 1 The algorithm does not allow any variable (first or second order) to map to two different images. The main restriction is that first order ....

G Huet and B Lang. Proving and applying program transformations expressed with second-order patterns. Acta Information, 11:31-55, 1978.

....representing and reasoning about software development steps in QED: ffl by higher order functions, ffl by meta functions. 4.1 Representation of Steps by Higher Order Functions The formalization of transformations using higher order patterns has been considered by several researchers. In [19], for example, program transformations for recursion removal are expressed as second order patterns defined in the simply typed calculus [5] As opposed to this treatment we use the powerful framework of QED and demonstrate that it is possible to formalize and verify a large development step ....

G. Huet and B. Lang. Proving and applying program transformations expressed with second-order-patterns. Acta Informatica, 11:31--55, 1978.

....In this respect, the content language OpenProof (and for the same reason already OpenMath) is more problematic than traditional agent content languages. However, since we can restrict OpenProof to second order expressions, we only need second order matching, which is known to be decidable [ Huet and Lang, 1978 ] We are currently investigating whether more restrictive policies for addressing services via OpenProof can be captured with comparably more lightweight mechanisms. 5.3 A Categorisation of Mathematical Services In this section we brie y categorise mathematical services by their behaviour and ....

G. Huet and B. Lang. Proving and applying Program Transformations expressed with Second Order Logic. Acta Informatica, 11:31-55, 1978.

....etc. Transformations need to be aware of variables by means of extra conditions to avoid problems such as free variable capture during substitution and lifting variable occurrences out of bindings. Transparent handling of variable bindings is desirable. Higher order abstract syntax (hoas) [17, 29, 43] gives a solution to such problems by encoding variable bindings as lambda abstractions. In addition to dealing with the problem of variable capture, hoas provides higher order matching which synthesizes new functions for higher order variables. One of the problems of higher order matching is that ....

G. Huet and B. Lang. Proving and applying program transformations expressed with second-order patterns. Acta Informatica, 11:31-55, 1978.

....a rule s left hand side into a given application graph, limited to the case where the images of the rule tips are given, is decidable and finitary on finite graph, i.e. it has mostly finitely many solutions. 15 In several contexts, such as automatical reduction, one prefers a 15 On finite DAGs [11] gives this result. unitary matching problem, i.e. a matching problem with at most one solution. Under certain circumstances the matching is determined by the mapping of rule tips into the application graph. An example is the condition imposed on left hand rule sides in CRSs (see Def. 2.2.8) ....

G. P. Huet and B. Lang. Proving and applying program transformations expressed with second-order patterns. Acta Informatica, 11:31--55, 1978.

....= H also tries to imitate the rigid term but by building a term with which to instantiate the free variable in a single step. Beyond this the two algorithms differ substantially. The algorithm presented here is significantly restricted and is for matching, not unification. Huet and Lang [5] adapt Huet s original algorithm to the process of matching second order terms, which is known to be decidable. Their application area is program transformation which is close to the intended application of the algorithm presented here. Simon [12] also presents an algorithm for second order ....

G. Huet and B. Lang. Proving and applying program transformations expressed with 2nd order patterns. Acta Informatica, 11:31--55, 1978.

....Higher order matching was first studied by Lewis D. Baxter and Gerard Huet in the midseventies in their PhD theses [2, 11] Baxter [2] showed that second order matching is NP complete by reduction to the one in three SAT problem. At the same time this case was independently investigated by Huet [11, 12]. In 1975 Huet devised a semi decision algorithm for (undecidable even in the second order case) unification problem [10] Later an analysis of behavior (termination, running time, etc. of this algorithm and its modifications was a source of a couple of results about decidability and complexity ....

....e.g. the one introduced by Dale Miller [15] we would rather avoid it when speaking about unification of an arbitrary term with a closed (or ground) one. 1 ToMasz Wierzbicki: Complexity of the higher order matching order decidable lower bound upper bound 1 yes [18] NLOGSPACE [8] 2 yes [12] NP complete [2, 12, 5] 3 yes [6] NP complete [25, 5] 4 yes [16] NEXPTIME hard 2 NEXPTIME ( 5] # not elementary recursive [24] Table 1: Decidability and complexity of higher order matching also presented an algorithm for the fourth order case (the case shown to be decidable a year before ....

[Article contains additional citation context not shown here]

Gerard P. Huet, Bernard Lang, Proving and applying program transformations expressed with second order patterns, Acta Informatica, 11 (1978) 31--55.

....patterns [Mil90] Although we use a language with full higher order uni cation many of its uses are for higher order matching of a pattern to a sub term of a speci cation. Higher order matching appears in existing work on functional program transformation and synthesis, for example in [HL78] 3 Proof Planning A proof of a theorem can be attained by applying sound derivation rules to certain axioms until the theorem is reached. Alternatively, one can start with a theorem and back chain through the rules until axioms are reached. The search space of these rules, however, is too ....

G. Huet and B. Lang. Proving and applying program transformation expressed with second order patterns. Acta Informatica, 11:31-55, 1978. Logic Program Synthesis in a Higher-Order Setting 20th January 13

....higher order patterns [18] Although we use a language with full higher order uni cation many of its uses are for higher order matching of a pattern to a sub term of a speci cation. Higher order matching appears in existing work on functional program transformation and synthesis, for example in [11]. 3 Proof Planning A proof of a theorem can be attained by applying sound derivation rules to certain axioms until the theorem is reached. Alternatively, one can start with a theorem and back chain through the rules until axioms are reached. The search space de ned by these rules, however, is ....

G. Huet and B. Lang. Proving and applying program transformation expressed with second order patterns. Acta Informatica, 11:31-55, 1978.

....here in the decidable cases. Among them we can mention higher order pattern matching that is decidable and unitary as a consequence of the decidability of pattern uni cation [Mil91, DHKP96] higher order matching which is known to be decidable up to the fourth order [Pad96, Pad00, Dow94, HL78] the 9 decidability of the general case being still open) many rst order equational theories including associativity, commutativity, distributivity and most of their combinations [Nip89, Rin96] For example when T is empty, the syntactic matching substitution from t to t 0 , when it ....

G. Huet and B. Lang. Proving and applying program transformations expressed with secondorder patterns. Acta Informatica, 11:31-55, 1978.

....can not be used to define this notion of instance since that would produce a substitution replacing both p and q with the same variable. Matching must be used to solve the constraint A v = B. Since the object logic is first order, at most second order matching is needed, which remains decidable [9]. In case second order matching yields more than one matching substitution, the rule schema above remains valid for any substitution. WLG R can be thought of as a tactic that is applied backward (or goal directed) to the conclusion of the rule, yielding the premises as subgoals. The intuitive ....

G'erard Huet and Bernard Lang. Proving and applying program transformations expressed with second-order patterns. Acta Informatica, 11:31--55, 1978.

....a (g a e) where a = 1 d This paper is concerned with an algorithm for doing this. In previous work [6] we have given one such algorithm, known as the one step algorithm; this 3 algorithm represented an advance on the standard algorithm in the literature which was developed by Huet and Lang [9]; for example it allowed certain programming examples such as the well known fast reverse optimisation to be derived. However, this algorithm proves to be inadequate for more complicated problems such as this one, and therefore we now extend the ideas presented there to produce the (predictably ....

....terms in the images of the substitutions returned; a rst order term is a ground term such as 0, a second order term is a function which takes rst order terms as parameters, and so on. However, this approach does not sit well with our particular application; the standard Huet and Lang algorithm [9] returns only second order matches which are not enough to solve problems such as mindepth, and although a general algorithm for nding third order matches exists [5] the set of these can be in nite, and a matching algorithm that is not guaranteed to terminate is not useful in a practical program ....

G. Huet and B. Lang. Proving and applying program transformations expressed with second-order patterns. Acta Informatica, 11:31-55, 1978.

....parameters (fi conversion) We call such OE a match, which is a map from variables to expression objects: OE : Var Exp where Exp denotes all expression. Clearly it is undesirable that matching gives a potentially infinite set of matches in the context of automatic program transformation. In [22], Huet and Lang suggested restricting attention to matching of second order terms, and gave a matching algorithm which is both decidable and complete to compute a finite number of incomparable matches. Recently, de Moor and Sittampalam [13] extended the second order matching algorithm, and present ....

....x. We can simply code it as removeZero : Int Int removeZero = m 0 x : x : For readability, we often write the above as: removeZero 0 x = x : Two remarks are worth making. First, the expressions to be matched can have multiple occurrences of the same variable [22], i.e. the rules are not necessary to be left linear. So, sum2Double : Num a ) a a sum2Double = m x x : 2 3 x is a valid rule. Second, like programming in ordinary pattern matching, we can define calculation in a case by case E[j[e] j : Env [Val ] E[j[v] jae = ae ....

G. Huet and B. Lang. Proving and applying program transformations expressed with second-order pattersn. Acta Informatica, 11:31--55, 1978.

....the corresponding instances P 1 and P 2 are equivalent programs w.r.t. Sem. The transformation from a schema S 1 to a schema S 2 is correct w.r.t. Sem i S 1 and S 2 are equivalent w.r.t. Sem . Correctness of schema transformations has been studied within various formalisms (see, for instance, [87, 115, 151] for owchart programs and recursive schemata) Usually, we are interested in the correct transformation from a schema S 1 to a schema S 2 i each instance of S 2 is more e cient of the corresponding instance of S 1 . Given an initial program P 1 , the schemata approach to program transformation ....

G. Huet and B. Lang. Proving and applying program transformations expressed with second-order patterns. Acta Informatica, 11:3155, 1978.

....2(n 1) Gamma 1; n) for n 0. 2 5 Related Techniques for Program Development and Final Discussion Due to space limitations we are not able to present here some other program transformation techniques which have been proposed in the literature (see, for instance, Arsac Kodratoff 82, Berry 76, Huet Lang 78, Meertens 87, Pepper 84, Pepper 87, Wegbreit 76] In this section we would like to briefly indicate some techniques which have been developed in the fields of Theoretical Computer Science and Software Engineering and can also be used for assisting the programmer during the program ....

Huet, G., Lang, B.: Proving and Applying Program Transformation Expressed with Second-Order Patterns. Acta Informatica 11 (1978) 31--55

....In this respect, the content language OpenProof (and for the same reason already OpenMath) is more problematic than traditional agent content languages. However, since we can restrict OpenProof to second order expressions, we only need second order matching, which is known to be decidable [ Huet and Lang, 1978 ] We are currently investigating whether more restrictive policies for addressing services via OpenProof can be captured with comparably more lightweight mechanisms. 5.3 A Categorisation of Mathematical Services In this section we briefly categorise mathematical services by their behaviour ....

G. Huet and B. Lang. Proving and applying Program Transformations expressed with Second Order Logic. Acta Informatica, 11:31--55, 1978.

....programs and proofs can be represented and manipulated easily [6, 11, 31] In developing environments of this kind, programming languages that facilitate the representation and manipulation of these kinds of objects play a fundamental role. As is evident from the arguments provided elsewhere [16, 22, 30, 28], the representation of objects involving the notion of binding, i.e. objects such as formulas, programs and proofs, is best achieved through the use of a term language based on the calculus. The task of reasoning about such objects in turn places an emphasis on a programming paradigm that ....

Huet, G. and Lang, B. Proving and Applying Program Transformations Expressed with Second-Order Logic. Acta Informatica 11 (1978) 31--55.

....correlates with our methods of matching recursion schemes during the reconstruction of types for recursive sequences. Elliott adapted Huet s second order unification algorithm whereas we developed our matching algorithm by adapting a special case of Huet and Lang s second order matching algorithm [HL78] Some techniques of Elliott s algorithm might be applicable to our matching problem. We differ from Elliot s work primarily in our formulation of dependent product types using well founded recursion based on our specific object language. Elliott s work in LF, on the other hand, leaves the object ....

....The heart of the thesis lies in the unification and matching theorems for the recursive sequences of types comprising the dependent products. In developing the matching algorithm we worked with ad hoc methods, variations of second order unification [Hue75] and variations of second order matching [HL78] combined with first order unification. We believe there may be a more general framework for our unification and matching that could greatly simplify the presentation and clarify the results in much the same way that semi unification turned out to be a general framework for viewing ML style ....

[Article contains additional citation context not shown here]

G'erard Huet and Bernard Lang. Proving and applying program transformations expressed with second-order patterns. Acta Informatica, 11:31--55, 1978.

....r r r r r r r . r r r : r r r r , r r r r r r r. r r r r r r r , r r r r . r r r r r , r , r r r rr . x 1 Introduction Over the last few decades, a variety of methodologies for deductive software synthesis, transformation, and refinement from specification have been suggested, e.g. [4 , 7, 3, 6, 10]. Our research investigates general frameworks that support such program development formalisms. That is, how can a framework be used to embed calculi in correctness preserving ways, be applied to the construction of programs hand in hand with their correctness proofs (e.g. synthesis as opposed ....

G'erard Huet and Bernard Lang. Proving and applying program transformations expressed with second-order patterns. Acta Informatica, pages 31--55, 1978.

....[1] and Isabelle [20] both of which are based on higher order unification. A second application area is the representation of the abstract syntax of programming languages. The representation of variable bindings in programming languages using typed calculus was first advocated by Huet and Lang [6] and more recently by Pfenning and Elliott [21] and also by Miller [13] Subtypes arise naturally because some syntactic classes are contained in others, for example every identifier is an expression. This principle is exploited in systems like Centaur [8] and PSG [25] PSG is also based on ....

G. Huet and B. Lang. Proving and applying program transformations expressed with second-order patterns. Acta Informatica, 11:31--55, 1978.

....program matches the source scheme S 1 , and if the hypotheses are satisfied, then the output program is the result of replacing t by the instantiation of the output scheme S 2 . The matching process has to instantiate functions, therefore this is at least a second order matching as described in [9, 10, 7]. A way to avoid this is to use combinators, such as the composition operator, to express programs. If we use the composition, identity, pro ections and product to express programs, the axioms of the algebra of programs are those of categorical products. Then the matching process becomes ....

....we discuss below. A matching problem is a finite set of matching equations fs 1 = t 1 ; 1 1 1 ; s n = t n g seeking CS (s 1 ; t 1 ) 1 1 1 CS (s n ; t n ) e t eor rst or er ter lan ua e to re resent sc e es Let us consider one of the well known transformation rules for recursion removal. In [6, 10], this transformation rule is expressed by the rule S 1 S 2 ; H) where S 1 : f(x) if p(x) then g(x) else h(i(x) f(j(x) S 2 : f(x) if p(x) then g(x) else w(i(x) j(x) where w(x; y) if p(y) then h(x; g(y) else w(h(x; i(y) j(y) under the associativity of h: h(x; h(y; ....

[Article contains additional citation context not shown here]

G. Huet and B. Lang. Proving and Applying Program Transformations Expressed with Second-Order Patterns. Acta Informatica , 11, pages 31-55, Springer-Verlag, 1978.

.... such as formulas, programs and proofs [Bru80, CAB 86, CH88, GMW79, HHP93, MN87, Pau88, Pfe89] Lambda terms have been found to be useful as data structures because of their ability to represent naturally the notion of binding that is part of the syntax of several kinds of objects [Chu40, HL78, MN87, Pau87, PE88] Consider, for instance, the task of representing the quantified formula 8x( p x) q x) in which p and q are predicate names. Observing that a quantifier plays the dual role of determining a scope and of making a predication, this formula can be rendered fairly transparently ....

G'erard Huet and Bernard Lang. Proving and applying program transformations expressed with second-order patterns. Acta Informatica, 11:31--55, 1978.

....as arguments. Including this ability thus provides for aspects of higherorder programming. In a similar sense, the use of lambda terms results in data structures that permit syntactically complex objects like formulas, programs, proofs and types to be represented in a rather natural fashion [7, 18, 26, 36, 38]. Allowing these terms into our language and using the appropriate unification operation on these terms leads to novel metalanguage capabilities, and these have been explored in several places (e.g. see [13, 25, 26, 37] From an implementation perspective, the new problems posed by our language ....

G'erard Huet and Bernard Lang. Proving and applying program transformations expressed with second-order patterns. Acta Informatica, 11:31--55, 1978.

....are mixed and full unification is required, but in proof checking and semi automated theorem proving, these rules can be applied separately and thus pattern matching can be used instead of unification. Higher order matching is conjectured decidable in [6] and the problem is still open. In [5] 6] [7] Huet has given a semi decision algorithm and shown that in the particular case in which the variables occurring in the term a are at most second order this algorithm terminates, and thus that second order matching is decidable. In [10] Statman has reduced the conjecture to the definability ....

....x o : T:s : T T : s : s o) are solutions to this problem and they cannot be obtained as instances of a finite number of solutions. Remark In [6] 12] the similar examples (x z : T:z) a and (x z : T:z) b(a) are considered. So in contrast with second order matching [6] [7] there is no (always terminating) algorithm that enumerates a complete set of solutions to a third order matching problem. We consider now algorithms that take as an input a matching problem and either give one solution to the problem or fail if it does not have any. 3 A Bound on the Depth of ....

G. Huet, B. Lang, Proving and Applying Program Transformations Expressed with Second Order Patterns, Acta Informatica, 11, 1978, pp. 31-55.

....main abstraction in terms M 1 ; M k cannot contain variables from the main abstraction. 1 Preface The higher order matching problem for simply typed calculus has been considered since 1976 ( 5] There were proposed several partial solutions of the problem (second order matching [4]; correct, but without a proof of completeness, algorithm [7] third order matching [3] fourth order matching [6] In this paper, we present a special case of the higher order matching problem the linear interpolation problem. The problem consists in solving a collection of ....

B. Lang G. Huet. Proving and applying program transformations expressed with second order patterns. Acta Informatica, (11):31--55, 1978.

....PATH system: object language. The language which is being transformed, a subset of Haskell in our case (though we hope to eventually support full Haskell) transformation rules. Semantics preserving transformation rules for the object language; they are in the form of transformation templates [9], P 1 = P 2 if C , where P 1 and P 2 are program schemes and C is an applicability condition. meta language. The language that describes the application of a transformation rule at a point in a program. Specifically, it is the object language extended with annotations which describe some ....

G'erard Huet and Bernard Lang. Proving and applying program transformations expressed with second order patterns. Acta Informatica, 11:31--55, 1978.

....like 8n:8i n:P (#i) using ML syntax for projections where #1 = fst, #2 = snd) However, a meta language is now needed to express program laws. A simpler approach to transformation, the schematic approach, avoids the use of a meta language: program laws are of the form e 1 = e 2 ( e 3 = e 4 [HL78] (e 1 ; e 2 ; e 3 ; e 4 are programs in the language, all free variables are implicitly universally quanti ed, and the premise is optional) program derivations are developed by successively applying program laws: the law is instantiated, the premise is satis ed, then the conclusion is used to ....

Grard Huet and Bernard Lang. Proving and applying program transformations expressed with second order patterns. Acta Informatica, 11:3155, 1978.

....to express the above law in some metalanguage or meta logic where one could say something like 8n:8i n:P(#i) using ML syntax for projections where #1 = fst, #2 = snd) However, a meta language is now needed to express program laws. A simpler approach to transformation, the schematic approach [7], avoids the use of a metalanguage: program laws are of the form e 1 = e 2 ( e 3 = e 4 (e 1 ; e 2 ; e 3 ; e 4 are programs in the language, all free variables are implicitly universally quanti ed, and the premise is optional) program derivations are developed by successively applying program ....

Grard Huet and Bernard Lang. Proving and applying program transformations expressed with second order patterns. Acta Informatica, 11:3155, 1978.

....reduces to t iff (t,t ) Sem r l . We write t (r l) t for (r l) t) reduces to t . A transformation rule r l is applicable to t iff t . t (r l) t . Higher Order Matching Higher order matching as a basis for transformation is not a new idea (the use of second order terms is suggested in [HL 78] but is rarely used in practical systems. Higher order terms have been used informally for a long time (e.g. BW 82, CIP 85, HK 93] e.g. in the schema: X. f X = if B X then T X else D (f (H X) K X) Usually transformation rules including such higher order variables, e.g. B, T, D, H, K, ....

....This makes them less abstract and less reusable. Our goal is to obtain powerful elementary transformation rules (corresponding, in fact, to rule schemata in a more conventional view) by real second order matching with matching combinators (the decidability of second order matching is proved in [HL 78] Matching Combinators Theories considered so far in extended matching [JK91] are very specific, hard to combine and so far impractical for a transformational setting. In ( SW 94, Shi 94] we present a theoretical framework for a refined matching language for schematic transformation rules. ....

Huet, G., Lang, B. (eds.): Proving and Applying Program Transformations Expressed with Second-Order Patterns. Acta Informatik 11, 1978.

....elegant alternative to the explicit reference to the position of a term proposed in [13] 2.2 Schema Based Transformations Program transformations can be conveniently represented using the schemata above. This idea was originally pursued in [3] in the context of logic languages, and earlier in [5], for functional languages. Schemata can be used to describe typical, inecient programming constructs and how these should be changed in order to confer a better computational behaviour on those programs in which they are found. Using the de nitions above, we can formalise a particular class of ....

G. Huet and B. Lang. Proving and Applying Program Transformations Expressed with Second-Order Patterns. Acta Informatica, 11:31-55, 1978.

....pattern matching algorithm that handles a wide subclass of Hoffmann and O Donnell s Simple Patterns. 1. Introduction Pattern Matching in trees is fundamental to term rewriting systems [21] transformational programming systems [4, 15, 18, 26, 30, 35] program editing and development systems [10, 23, 32], code generator generators [14, 17, 19, 29] theorem provers [24] logic programming optimizers that attempt to replace unification with matching [27] and compilers for functional languages such as ML [34] and Haskell [22] that have equational function definitions. ################## 1. An ....

Huet, G. and Lang, B., "Proving and Applying Program Transformations Expressed with Second-Order Patterns, " Acta Informatica, vol. 11, pp. 31-55, 1978.

....improvements shown above can be represented in a generic way, by means of a transformation where the inefficient constructs are described as well as the changes that have to be made in order to confer a better performance on the programs in which they appear. This idea was originally presented in [5], for functional programming, and in [4] we see the same idea applied to logic programs. In [13] a completely automated approach is proposed for the analysis and transformation of logic programs incorporating this concept, and in [11] a more efficient method is proposed to perform the analysis ....

G. Huet and B. Lang. Proving and Applying Program Transformations Expressed with Second-Order Patterns. Acta Informatica, 11:31--55, 1978.

....following example: assume a goal x:c(F (x; t) x:c(x) with solution = fF 7 x; y:xg. Here, normalization of t does not change x:c(F (x; t) 7 An Example: Program Transformation The utility of higher order unification for program transformations has been shown nicely by Huet and Lang [14] and has been developed further in [26, 8] The following models an example for unfold fold program transformation in [5] We assume the following rules for lists: map(F; XjR] F (X)jmap(F; R) foldl(G; XjR] G(X; foldl(G; R) Now assume writing a function g(F; L) by g(F; L) foldl(x; ....

G'erard Huet and Bernard Lang. Proving and applying program transformations expressed with second-order patterns. Acta Informatica, 11:31--55, 1978.

....description of the enhanced schema language is presented in [VF95, VF96a] Schema based transformations are standard syntactic manipulations of portions of a given program. Such constructs can be seen as rewriting rules consisting of second order program schemas, similar to the work depicted in [HL78]. Program schemata are used to depict both input programs and their improved output versions. Two kinds of opportunities for program optimisation are formalised in [VF95, VF96a] one concerning individual procedures and how they can be improved singly, and the other concerning groups of ....

G. Huet and B. Lang. Proving and Applying Program Transformations Expressed with Second-Order Patterns. Acta Informatica, 11:31--55, 1978.

....But we are primarily interested here 4 in the decidable cases. Among them we can mention higher order pattern matching that is decidable and unitary as a consequence of pattern unification [Mil91, DHKP96] higher order matching which is known to be decidable up to the fourth order [Pad96, Dow92, HL78] the decidability of the general case being still open) many first order equational theories including associativity, commutativity, distributivity and most of their combinations [JK91] Indeed we restrict ourselves later in this paper to just considering syntactic matching. In this case we ....

G. Huet and B. Lang. Proving and applying program transformations expressed with secondorder patterns. Acta Informatica, 11:31--55, 1978.

No context found.

Huet, G. and Lang, B. Proving and Applying Program Transformations Expressed with Second-Order Logic. Acta Informatica 11 (1978) 31--55.

No context found.

G. P. Huet, B. Lang, Proving and applying program transformations expressed with second-order patterns, Acta Informatica 11 (1978) 31-55.

No context found.

Huet, G.P., Lang, B.: Proving and applying program transformations expressed with second-order patterns. Acta Informatica 11 (1978) 31-55

No context found.

Huet, G., Lang, B.: Proving and applying program transformations expressed with second-order patterns. Acta Informatica 11 (1978) 31--55

No context found.

Huet, G., and Lang, B. Proving and applying program transformations expressed with second-order patterns. Acta informatica 11 (1978), 31--55.

No context found.

G. P. Huet, B. Lang, Proving and applying program transformations expressed with second-order patterns, Acta Informatica 11 (1978), pages 31--55.

No context found.

G. P. Huet, B. Lang, Proving and applying program transformations expressed with second-order patterns, Acta Informatica 11 (1978), pages 31--55.

No context found.

G. P. Huet and B. Lang, Proving and applying program transformations expressed with second-order patterns, Acta Informatica 11 (1978), pages 31--55.

First 50 documents  Next 50

Online articles have much greater impact   More about CiteSeer.IST at NUS   Add search form to your site   Submit documents   Feedback  

CiteSeer.IST at NUS - Copyright Penn State and NEC. Hosted by the School of Computing, National University of Singapore.