Technical report Frank / Johann-Wolfgang-Goethe-Universität, Fachbereich Informatik und Mathematik, Institut für Informatik
Refine
Year of publication
Document Type
- Working Paper (95)
Language
- English (95)
Has Fulltext
- yes (95)
Is part of the Bibliography
- no (95)
Keywords
- Lambda-Kalkül (18)
- Formale Semantik (10)
- Operationale Semantik (8)
- Programmiersprache (7)
- lambda calculus (7)
- Nebenläufigkeit (6)
- functional programming (6)
- concurrency (5)
- pi-calculus (5)
- Logik (4)
Institute
- Informatik (95)
63
We consider matching, rewriting, critical pairs and the Knuth-Bendix confluence test on rewrite rules in a nominal setting extended by atom-variables. Computing critical pairs is done using nominal unification, and rewriting using nominal matching. We utilise atom-variables to formulate rewrite rules, which is an improvement over previous approaches, using usual nominal unification, nominal matching and nominal equivalence of expressions coupled with a freshness constraint. We determine the complexity of several problems in a quantified freshness logic. In particular we show that nominal matching is Πp2-complete. We prove that the adapted Knuth-Bendix confluence test is applicable to a nominal rewrite system with atom-variabes and thus, that there is a decidable test whether confluence of the ground instance of the abstract rewrite system holds. We apply the nominal Knuth Bendix confluence criterion to the theory of monads, and compute a convergent nominal rewrite system modulo alpha-equivalence.
62
A sound and complete algorithm for nominal unification of higher-order expressions with a recursive let is described, and shown to run in non-deterministic polynomial time. We also explore specializations like nominal letrec-matching for expressions, for DAGs, and for garbage-free expressions and determine their complexity. As extension a nominal unification algorithm for higher-order expressions with recursive let and atom-variables is constructed, where we show that it also runs in non-deterministic polynomial time.
61
The focus of this paper are space-improvements of programs, which are transformations that do not worsen the space requirement during evaluations. A realistic theoretical treatment must take garbage collection method into account. We investigate space improvements under the assumption of an optimal garbage collector. Such a garbage collector is not implementable, but there is an advantage: The investigations are independent of potential changes in an implementable garbage collector and our results show that the evaluation and other similar transformations are space-improvements.
60 [version 1.0]
The synchronous pi-calculus is translated into a core language of Concurrent Haskell extended by futures (CHF). The translation simulates the synchronous message-passing of the pi-calculus by sending messages and adding synchronization using Concurrent Haskell's mutable shared-memory locations (MVars). The semantic criterion is a contextual semantics of the pi-calculus and of CHF using may- and should-convergence as observations. The results are equivalence with respect to the observations, full abstraction of the translation of closed processes, and adequacy of the translation on open processes. The translation transports the semantics of the pi-calculus processes under rather strong criteria, since error-free programs are translated into error-free ones, and programs without non-deterministic error possibilities are also translated into programs without non-deterministic error-possibilities. This investigation shows that CHF embraces the expressive power and the concurrency capabilities of the pi-calculus.
60 [version 5.0]
Correctness of program transformations and translations in concurrent programming is the focus of our research. In this case study the relation of the synchronous pi-calculus and a core language of Concurrent Haskell (CH) with asynchronous communication is investigated. We show that CH embraces the synchronous pi-calculus. The formal foundations are contextual semantics in both languages, where may- as well as should-convergence are observed. We succeed in defining and proving smart properties of a particular translation mapping the synchronous pi-calculus into CH. This implies that pi-processes are error-free if and only if their translation is an error-free CH-program Our result shows that the chosen semantics is not only powerful, but can also be applied in concrete and technically complex situations. The developed translation uses private names. We also automatically check potentially correct translations that use global names instead of private names. As a complexity parameter we use the number of MVars introduced by the transformation, where MVars are synchronized 1-place buffers. The automated refutation of incorrect translations leads to a classification of potentially correct translations, and to the conjecture that one global MVar is insufficient.
60 [version 4.0]
Correctness of program transformations and translations in concurrent programming is the focus of our research. In this case study the relation of the synchronous pi-calculus and a core language of Concurrent Haskell (CH) with asynchronous communication is investigated. We show that CH embraces the synchronous pi-calculus. The formal foundations are contextual semantics in both languages, where may- as well as should-convergence are observed. We succeed in defining and proving smart properties of a particular translation mapping the synchronous pi-calculus into CH. This implies that pi-processes are error-free if and only if their translation is an error-free CH-program Our result shows that the chosen semantics is not only powerful, but can also be applied in concrete and technically complex situations. The developed translation uses private names. We also automatically check potentially correct translations that use global names instead of private names. As a complexity parameter we use the number of MVars introduced by the transformation, where MVars are synchronized 1-place buffers. The automated refutation of incorrect translations leads to a classification of potentially correct translations, and to the conjecture that one global MVar is insufficient.
60 [version 3.0]
Correctness of program transformations and translations in concurrent programming is the focus of our research. In this case study the relation of the synchronous pi-calculus and a core language of Concurrent Haskell (CH) with asynchronous communication is investigated. We show that CH embraces the synchronous pi-calculus. The formal foundations are contextual semantics in both languages, where may- as well as should-convergence are observed. We succeed in defining and proving smart properties of a particular translation mapping the synchronous pi-calculus into CH. This implies that pi-processes are error-free if and only if their translation is an error-free CH-program Our result shows that the chosen semantics is not only powerful, but can also be applied in concrete and technically complex situations. The developed translation uses private names. We also automatically check potentially correct translations that use global names instead of private names. As a complexity parameter we use the number of MVars introduced by the transformation, where MVars are synchronized 1-place buffers. The automated refutation of incorrect translations leads to a classification of potentially correct translations, and to the conjecture that one global MVar is insufficient.
60 [version 2.0]
We investigate translations from the synchronous pi-calculus
into a core language of Concurrent Haskell (CH). Synchronous messagepassing of the pi-calculus is encoded as sending messages and adding synchronization using Concurrent Haskell’s mutable shared-memory locations (MVars). Our correctness criterion for translations is invariance of may- and should-convergence. This embraces that all executions of a process are error-free if and only if this also holds for the translated program. We exhibit a particular correct translation that uses a fresh, private MVar per communication interaction and that is in addition adequate, and which is also fully abstract on closed expressions. A metaresult is that CH has the expressive power and the concurrency capabilities of the synchronous pi-calculus.
We also automatically check variants of translations of synchronous communication into an asynchronous calculus where only an a priori fixed number of MVars per channel (and not per communication interaction!) is available. We obtain non-correctness results for classes of small translations, and exemplary argue for the correctness (and adequacy) for two translations with a higher number of MVars. We introduce a classification of the potentially correct translations.
59
Automated deduction in higher-order program calculi, where properties of transformation rules are demanded, or confluence or other equational properties are requested, can often be done by syntactically computing overlaps (critical pairs) of reduction rules and transformation rules. Since higher-order calculi have alpha-equivalence as fundamental equivalence, the reasoning procedure must deal with it. We define ASD1-unification problems, which are higher-order equational unification problems employing variables for atoms, expressions and contexts, with additional distinct-variable constraints, and which have to be solved w.r.t. alpha-equivalence. Our proposal is to extend nominal unification to solve these unification problems. We succeeded in constructing the nominal unification algorithm NomUnifyASC. We show that NomUnifyASC is sound and complete for these problem class, and outputs a set of unifiers with constraints in nondeterministic polynomial time if the final constraints are satisfiable. We also show that solvability of the output constraints can be decided in NEXPTIME, and for a fixed number of context-variables in NP time. For terms without context-variables and atom-variables, NomUnifyASC runs in polynomial time, is unitary, and extends the classical problem by permitting distinct-variable constraints.
1998 ACM Subject Classification F.4.1 Mathematical Logic
58
We propose a model for measuring the runtime of concurrent programs by the minimal number of evaluation steps. The focus of this paper are improvements, which are program transformations that improve this number in every context, where we distinguish between sequential and parallel improvements, for one or more processors, respectively. We apply the methods to CHF, a model of Concurrent Haskell extended by futures. The language CHF is a typed higher-order functional language with concurrent threads, monadic IO and MVars as synchronizing variables. We show that all deterministic reduction rules and 15 further program transformations are sequential and parallel improvements. We also show that introduction of deterministic parallelism is a parallel improvement, and its inverse a sequential improvement, provided it is applicable. This is a step towards more automated precomputation of concurrent programs during compile time, which is also formally proven to be correctly optimizing.
57 [V3]
We explore space improvements in LRP, a polymorphically typed call-by-need functional core language. A relaxed space measure is chosen for the maximal size usage during an evaluation. It Abstracts from the details of the implementation via abstract machines, but it takes garbage collection into account and thus can be seen as a realistic approximation of space usage. The results are: a context lemma for space improving translations and for space equivalences; all but one reduction rule of the calculus are shown to be space improvements, and the exceptional one, the copy-rule, is shown to increase space only moderately.
Several further program transformations are shown to be space improvements or space equivalences, in particular the translation into machine expressions is a space equivalence. These results are a step Forward in making predictions about the change in runtime space behavior of optimizing transformations in callbyneed functional languages.
57 [V2]
We explore space improvements in LRP, a polymorphically typed call-by-need functional core language. A relaxed space measure is chosen for the maximal size usage during an evaluation. It Abstracts from the details of the implementation via abstract machines, but it takes garbage collection into account and thus can be seen as a realistic approximation of space usage. The results are: a context lemma for space improving translations and for space equivalences; all but one reduction rule of the calculus are shown to be space improvements, and the exceptional one, the copy-rule, is shown to increase space only moderately.
Several further program transformations are shown to be space improvements or space equivalences, in particular the translation into machine expressions is a space equivalence. These results are a step Forward in making predictions about the change in runtime space behavior of optimizing transformations in callbyneed functional languages.
57
We explore space improvements in LRP, a polymorphically typed call-by-need functional core language. A relaxed space measure is chosen for the maximal size usage during an evaluation. It Abstracts from the details of the implementation via abstract machines, but it takes garbage collection into account and thus can be seen as a realistic approximation of space usage. The results are: a context lemma for space improving translations and for space equivalences; all but one reduction rule of the calculus are shown to be space improvements, and the exceptional one, the copy-rule, is shown to increase space only moderately.
Several further program transformations are shown to be space improvements or space equivalences, in particular the translation into machine expressions is a space equivalence. These results are a step Forward in making predictions about the change in runtime space behavior of optimizing transformations in callbyneed functional languages.
56 [version 3.0]
The calculus LRP is a polymorphically typed call-by-need lambda calculus extended by data constructors, case-expressions, seq-expressions and type abstraction and type application. This report is devoted to the extension LRPw of LRP by scoped sharing decorations. The extension cannot be properly encoded into LRP if improvements are defined w.r.t. the number of lbeta, case, and seq-reductions, which makes it necessary to reconsider the claims and proofs of properties. We show correctness of improvement properties of reduction and transformation rules and also of computation rules for decorations in the extended calculus LRPw. We conjecture that conservativity of the embedding of LRP in LRPw holds.
56 [version 2.0]
The calculus LRP is a polymorphically typed call-by-need lambda calculus extended by data constructors, case-expressions, seq-expressions and type abstraction and type application. This report is devoted to the extension LRPw of LRP by scoped sharing decorations. The extension cannot be properly encoded into LRP if improvements are defined w.r.t. the number of lbeta, case, and seq-reductions, which makes it necessary to reconsider the claims and proofs of properties. We show correctness of improvement properties of reduction and transformation rules and also of computation rules for decorations in the extended calculus LRPw. We conjecture that conservativity of the embedding of LRP in LRPw holds.
56 [version 1.0]
This report documents the extension LRPw of LRP by sharing decorations. We show correctness of improvement properties of reduction and transformation rules and also of computation rules for decorations in the extended calculus LRPw. We conjecture that conservativity of the embedding of LRP in LRPw holds.
55 [version 3.0]
An improvement is a correct program transformation that optimizes the program, where the criterion is that the number of computation steps until a value is obtained is decreased. This paper investigates improvements in both { an untyped and a polymorphically typed { call-by-need lambda-calculus with letrec, case, constructors and seq. Besides showing that several local optimizations are improvements, the main result of the paper is a proof that common subexpression elimination is correct and an improvement, which proves a conjecture and thus closes a gap in Moran and Sands' improvement theory. We also prove that several different length measures used for improvement in Moran and Sands' call-by-need calculus and our calculus are equivalent.
55 [version 2.0]
An improvement is a correct program transformation that optimizes the program, where the criterion is that the number of computation steps until a value is obtained is decreased. This paper investigates improvements in both { an untyped and a polymorphically typed { call-by-need lambda-calculus with letrec, case, constructors and seq. Besides showing that several local optimizations are improvements, the main result of the paper is a proof that common subexpression elimination is correct and an improvement, which proves a conjecture and thus closes a gap in Moran and Sands' improvement theory. We also prove that several different length measures used for improvement in Moran and Sands' call-by-need calculus and our calculus are equivalent.
55 [version 1.0]
An improvement is a correct program transformation that optimizes the program, where the criterion is that the number of computation steps until a value is obtained is decreased. This paper investigates improvements in both { an untyped and a polymorphically typed { call-by-need lambda-calculus with letrec, case, constructors and seq. Besides showing that several local optimizations are improvements, the main result of the paper is a proof that common subexpression elimination is correct and an improvement, which proves a conjecture and thus closes a gap in Moran and Sands' improvement theory. We also prove that several different length measures used for improvement in Moran and Sands' call-by-need calculus and our calculus are equivalent.
54
Motivated by the question whether sound and expressive applicative similarities for program calculi with should-convergence exist, this paper investigates expressive applicative similarities for the untyped call-by-value lambda-calculus extended with McCarthy's ambiguous choice operator amb. Soundness of the applicative similarities w.r.t. contextual equivalence based on may-and should-convergence is proved by adapting Howe's method to should-convergence. As usual for nondeterministic calculi, similarity is not complete w.r.t. contextual equivalence which requires a rather complex counter example as a witness. Also the call-by-value lambda-calculus with the weaker nondeterministic construct erratic choice is analyzed and sound applicative similarities are provided. This justifies the expectation that also for more expressive and call-by-need higher-order calculi there are sound and powerful similarities for should-convergence.