Abstract This paper describes anti-unification algorithms for computing least general generalizations of two expressions in a functional programming language with recursive let. First, by exploring a semantic approach to the problem, we argue for an improvement of the technique used in previous papers which avoids infinite chains of properly descending generalizations. Second, we present a (non-deterministic) nominal general anti-unification algorithm applicable to general expressions, which is complete, terminating and requires polynomial time. Third, we propose a specialized anti-unification algorithm applicable to two or more garbage-free ground expressions that produces a single least general generalization in polynomial time, and which can also exploit further semantically correct equivalences. Our results have potential applications in finding clones in functional programs.

To support the understanding of declarative probabilistic programming languages, we introduce a lambda-calculus with a fair binary probabilistic choice that chooses between its arguments with equal probability. The reduction strategy of the calculus is a call-by-need strategy that performs lazy evaluation and implements sharing by recursive let-expressions. Expected convergence of expressions is the limit of the sum of all successful reduction outputs weighted by their probability. We use contextual equivalence as program semantics: two expressions are contextually equivalent if and only if the expected convergence of the expressions plugged into any program context is always the same. We develop and illustrate techniques to prove equivalences including a context lemma, two derived criteria to show equivalences and a syntactic diagram-based method. This finally enables us to show correctness of a large set of program transformations with respect to the contextual equivalence.

A sound and complete algorithm for nominal unification of higher-order expressions with a recursive let is described, and shown to run in nondeterministic polynomial time. We also explore specializations like nominal letrec-matching for expressions, for DAGs, and for garbage-free expressions and determine their complexity. We also provide a nominal unification algorithm for higher-order expressions with recursive let and atom-variables, where we show that it also runs in nondeterministic polynomial time. In addition we prove that there is a guessing strategy for nominal unification with letrec and atom-variable that is a trade-off between exponential growth and non-determinism. Nominal matching with variables representing partial letrec-environments is also shown to be in NP. Comment: 37 pages, 9 figures, This paper is an extended version of the conference publication: Manfred Schmidt-Schau{\ss} and Temur Kutsia and Jordi Levy and Mateu Villaret and Yunus Kutz, Nominal Unification of Higher Order Expressions with Recursive Let, LOPSTR-16, Lecture Notes in Computer Science 10184, Springer, p 328 -344, 2016. arXiv admin note: text overlap with arXiv:1608.03771

Abstract We consider matching, rewriting, critical pairs and the Knuth–Bendix confluence test on rewrite rules in a nominal setting extended by atom-variables. We utilize atom-variables instead of atoms to formulate and rewrite rules on constrained expressions, which is an improvement of expressiveness over previous approaches. Nominal unification and nominal matching are correspondingly extended. Rewriting is performed using nominal matching, and computing critical pairs is done using nominal unification. We determine the complexity of several problems in a quantified freshness logic. In particular we show that nominal matching is $$\prod _2^p$$ -complete. We prove that the adapted Knuth–Bendix confluence test is applicable to a nominal rewrite system with atom-variables, 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.

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 allowing declarative implementations of concurrent programs. 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 several further useful program transformations are sequential and parallel improvements.

We consider term rewriting under sharing in the form of compression by singleton tree grammars (STG), which is more general than the term dags. Algorithms for the subtasks of rewriting are analysed: finding a redex for rewriting by locating a position for a match, performing a rewrite step by constructing the compressed result and executing a sequence of rewrite steps. The first main result is that locating a match of a linear termsin another termtcan be performed in polynomial time ifs,tare both STG-compressed. This generalizes results on matching of STG-compressed terms, matching of straight-line-program-compressed strings with character-variables, where every variable occurs at most once, and on fully compressed matching of strings. Also, for the case wheresis directed-acyclic-graph (DAG)-compressed, it is shown that submatching can be performed in polynomial time. The general case of compressed submatching can be computed in non-deterministic polynomial time, and an algorithm is described that may be exponential in the worst case, its complexity isnO(k), wherekis the number of variables with double occurrences insandnis the size of the input. The second main result is that in case there is an oracle for the redex position, a sequence ofmparallel or single-step rewriting steps under STG-compression can be performed in polynomial time. This generalizes results on DAG-compressed rewriting sequences. Combining these results implies that for an STG-compressed term rewrite system with left-linear rules,mparallel or single-step term rewrite steps can be performed in polynomial time in the input sizenandm.

This paper presents an algorithm for unification of meta-expressions of higher-order lambda calculi with recursive bindings. The meta-language uses higher-order abstract syntax. Besides usual unification variables for expressions and term variables, there are context-variables for generalized shapes of contexts, environment variables for sets of bindings, and (flexible) chain-variables as they, for instance, occur in formal descriptions of the operational semantics of lazy functional programming languages with shared environments. To exclude solutions with unintended scoping, the algorithm takes advantage of so-called non-capture constraints. The expressiveness of the meta-language comprises reduction contexts to support reasoning on program evaluation under reduction strategies. The non-deterministic unification algorithm runs in polynomial time provided certain restrictions on the number of occurrences of unification variables hold. The deterministic version of the algorithm will output a finite and concise set of representatives of all solutions. Results on an implementation of the algorithm are presented. The experiments focus on computing critical pairs of equations from program calculi modeling lazy functional languages which support the reasoning on the correctness of program transformations.

One Context Unification (1CU) extends first-order unification by introducing a single context variable. This problem was recently shown to be in NP, but it is not known to be solvable in polynomial time. We show that the case of 1CU where the context variable occurs at most twice in the input (1CU2r) is solvable in polynomial time. Moreover, a polynomial representation of all solutions can also be computed in polynomial time. The 1CU2r problem is important as it is used as a subroutine in polynomial time algorithms for several more-general classes of 1CU problem. Our algorithm can be seen as an extension of the usual rules of first-order unification and can be used to solve related problems in polynomial time, such as first-order unification of two terms that tolerates one clash. All our results assume that the input terms are represented as Directed Acyclic Graphs.

One context unification extends first-order unification by introducing a single context variable, possibly with multiple occurrences. One context unification is known to be in NP, but it is not known to be solvable in polynomial time. In this paper, we present a polynomial time algorithm for certain interesting classes of the one context unification problem. Our algorithm is presented as an inference system that non-trivially extends the usual inference rules for first-order unification. The algorithm is of independent value as it can be used, with slight modifications, to solve other problems, such as the first-order unification problem that tolerates one clash.

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 not increased in any context. This paper investigates improvements an untyped call-by-need lambdacalculus 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 the improvement theory of Moran and Sands. We also prove that several different length measures used for improvement in the call-by-need calculus of Moran and Sands and our calculus are equivalent.

A concurrent implementation of software transactional memory in Concurrent Haskell using a call-by-need functional language with processes and futures is given. The description of the small-step operational semantics is precise and explicit, and employs an early abort of conflicting transactions. A proof of correctness of the implementation is given for a contextual semantics with may- and should-convergence. This implies that our implementation is a correct evaluator for an abstract specification equipped with a big-step semantics.

Our motivation is the question whether the lazy lambda calculus, a pure lambda calculus with the leftmost outermost rewriting strategy, considered under observational semantics, or extensions thereof, are an adequate model for semantic equivalences in real-world purely functional programming languages, in particular for a pure core language of Haskell. We explore several extensions of the lazy lambda calculus: addition of a seq-operator, addition of data constructors and case-expressions, and their combination, focusing on conservativity of these extensions. In addition to untyped calculi, we study their monomorphically and polymorphically typed versions. For most of the extensions we obtain non-conservativity which we prove by providing counterexamples. However, we prove conservativity of the extension by data constructors and case in the monomorphically typed scenario.

Equality of expressions in lambda-calculi, higher-order programming languages, higher-order programming calculi and process calculi is defined as alpha-equivalence. Permutability of bindings in let-constructs and structural congruence axioms extend alpha-equivalence. We analyse these extended alpha-equivalences and show that there are calculi with polynomial time algorithms, that a multiple-binding "let" may make alpha-equivalence as hard as finding graph-isomorphisms, and that the replication operator in the pi-calculus may lead to an EXPSPACE-hard alpha-equivalence problem.

The calculus CHF models Concurrent Haskell extended by concurrent, implicit futures. It is a lambda and process calculus with concurrent threads, monadic concurrent evaluation, and includes a pure functional lambda-calculus PF which comprises data constructors, case-expressions, letrec-expressions, and Haskell's seq. Our main result is conservativity of CHF as extension of PF. This allows us to argue that compiler optimizations and transformations from pure Haskell remain valid in Concurrent Haskell even if it is extended by futures. We also show that conservativity does no longer hold if the extension includes Concurrent Haskell and unsafe Interleave IO.

We consider the problem of finding an instance of a string-pattern s in a given string under compression by straight line programs (SLP). The variables of the string pattern can be instantiated by single characters. This is a generalisation of the fully compressed pattern match, which is the task of finding a compressed string in another compressed string, which is known to have a polynomial time algorithm. We mainly investigate patterns s that are linear in the variables, i.e. variables occur at most once in s, also known as partial words. We show that fully compressed pattern matching with linear patterns can be performed in polynomial time. A polynomial-sized representation of all matches and all substitutions is also computed. Also, a related algorithm is given that computes all periods of a compressed linear pattern in polynomial time. A technical key result on the structure of partial words shows that an overlap of h+2 copies of a partial word w with at most h holes implies that w is strongly periodic.

In this paper we analyze the semantics of a higher-order functional language with concurrent threads, monadic IO and synchronizing variables as in Concurrent Haskell. To assure declarativeness of concurrent programming we extend the language by implicit, monadic, and concurrent futures. As semantic model we introduce and analyze the process calculus CHF, which represents a typed core language of Concurrent Haskell extended by concurrent futures. Evaluation in CHF is defined by a small-step reduction relation. Using contextual equivalence based on may- and should-convergence as program equivalence, we show that various transformations preserve program equivalence. We establish a context lemma easing those correctness proofs. An important result is that call-by-need and call-by-name evaluation are equivalent in CHF, since they induce the same program equivalence. Finally we show that the monad laws hold in CHF under mild restrictions on Haskell's seq-operator, which for instance justifies the use of the do-notation.

Frontmatter, Table of Contents, Preface, Conference Organization

Term unification plays an important role in many areas of computer science, especially in those related to logic. The universal mechanism of grammar-based compression for terms, in particular the so-calledsingleton tree grammars (STGAs), have recently drawn considerable attention. Using STGs, terms of exponential size and height can be represented in linear space. Furthermore, the term representation by directed acyclic graphs (dags) can be efficiently simulated. The present article is the result of an investigation on term unification and matching when the terms given as input are represented using different compression mechanisms for terms such as dags and singleton tree grammars. We describe a polynomial time algorithm for context matching with dags, when the number of different context variables is fixed for the problem. For the same problem, NP-completeness is obtained when the terms are represented using the more general formalism of singleton tree grammars. For first-order unification and matching polynomial time algorithms are presented, each of them improving previous results for those problems.

This paper shows the equivalence of applicative similarity and contextual approximation, and hence also of bisimilarity and contextual equivalence, in the deterministic call-by-need lambda calculus with letrec. Bisimilarity simplifies equivalence proofs in the calculus and opens a way for more convenient correctness proofs for program transformations. Although this property may be a natural one to expect, to the best of our knowledge, this paper is the first one providing a proof. The proof technique is to transfer the contextual approximation into Abramsky's lazy lambda calculus by a fully abstract and surjective translation. This also shows that the natural embedding of Abramsky's lazy lambda calculus into the call-by-need lambda calculus with letrec is an isomorphism between the respective term-models. We show that the equivalence property proven in this paper transfers to a call-by-need letrec calculus developed by Ariola and Felleisen.

This paper is an investigation of the matching problem for term equations s = t where s contains context variables and first-order variables, and both terms s and t are given using some kind of compressed representation. The main result is a polynomial time algorithm for context matching with dags, when the number of different context variables is fixed for the problem. NP-completeness is obtained when the terms are represented using the more general formalism of singleton tree grammars. As an ingredient of this proof, we also show that the special case of first-order matching with singleton tree grammars is decidable in polynomial time.

Abstract This paper proves correctness of Nöcker's method of strictness analysis, implemented in the Clean compiler, which is an effective way for strictness analysis in lazy functional languages based on their operational semantics. We improve upon the work Clark, Hankin and Hunt did on the correctness of the abstract reduction rules in two aspects. Our correctness proof is based on a functional core language and a contextual semantics, thus proving a wider range of strictness-based optimizations as correct, and our method fully considers the cycle detection rules, which contribute to the strength of Nöcker's strictness analysis. Our algorithm SAL is a reformulation of Nöcker's strictness analysis algorithm in a functional core language LR. This is a higher order call-by-need lambda calculus with case , constructors, letrec , and seq , which is extended during strictness analysis by set constants like Top or Inf , denoting sets of expressions, which indicate different evaluation demands. It is also possible to define new set constants by recursive equations with a greatest fixpoint semantics. The operational semantics of LR is a small-step semantics. Equality of expressions is defined by a contextual semantics that observes termination of expressions. Basically, SAL is a nontermination checker. The proof of its correctness and hence of Nöcker's strictness analysis is based mainly on an exact analysis of the lengths of evaluations, i.e., normal-order reduction sequences to WHNF. The main measure being the number of “essential” reductions in evaluations. Our tools and results provide new insights into call-by-need lambda calculi, the role of sharing in functional programming languages, and into strictness analysis in general. The correctness result provides a foundation for Nöcker's strictness analysis in Clean, and also for its use in Haskell.

We present a higher-order call-by-need lambda calculus enriched with constructors,caseexpressions, recursiveletrecexpressions, aseqoperator for sequential evaluation and a non-deterministic operatorambthat is locally bottom-avoiding. We use a small-step operational semantics in the form of a single-step rewriting system that defines a (non-deterministic) normal-order reduction. This strategy can be made fair by adding resources for book-keeping. As equational theory, we use contextual equivalence (that is, terms are equal if, when plugged into any program context, their termination behaviour is the same), in which we use a combination of may- and must-convergence, which is appropriate for non-deterministic computations. We show that we can drop the fairness condition for equational reasoning, since the valid equations with respect to normal-order reduction are the same as for fair normal-order reduction. We develop a number of proof tools for proving correctness of program transformations. In particular, we prove a context lemma for both may- and must- convergence that restricts the number of contexts that need to be examined for proving contextual equivalence. Combining this with so-called complete sets of commuting and forking diagrams, we show that all the deterministic reduction rules and some additional transformations preserve contextual equivalence. We also prove a standardisation theorem for fair normal-order reduction. The structure of the ordering ≤cis also analysed, and we show that Ω is not a least element and ≤calready implies contextual equivalence with respect to may-convergence.

Monadic second-order unification is second-order unification where all function constants occurring in the equations are unary. Here we prove that the problem of deciding whether a set of monadic equations has a unifier is NP-complete, where we use the technique of compressing solutions using singleton context-free grammars. We prove that monadic second-order matching is also NP-complete.

Context unification is a variant of second‐order unification and also a generalization of string unification. Currently it is not known whether context unification is decidable. An expressive fragment of context unification is stratified context unification. Recently, it turned out that stratified context unification and one‐step rewrite constraints are equivalent. This paper contains a description of a decision algorithm SCU for stratified context unification together with a proof of its correctness, which shows decidability of stratified context unification as well as of satisfiability of one‐step rewrite constraints.

In this paper we present a non-deterministic call-by-need (untyped) lambda calculus X,d with a constant choice and a let-syntax that models sharing. Our main result is that Xnd has the nice operational properties of the standard lambda calculus: confluence on sets of expressions, and normal or-der reduction is sufficient to reach head normal form. Us-ing a strong contextual equivalence we show correctness of several program transformations. In particular of lambda-lifting using deterministic maximal free expressions. These results show that And is a new and also natural combination of non-determinism and lambda-calculus, which has a lot of opportunities for parallel evaluation. An intended application of And is as a foundation for compil-ing lazy functional programming languages with I/O based on direct calls. The set of correct program transformations can be rigorously distinguished from non-correct ones. All program transformations are permitted with the slight ex-ception that for transformations like common subexpression elimination and lambda-lifting with maximal free expres-sions the involved subexpressions have to be deterministic ones. 1

N ATURAL E XPERT is a product that allows users to build knowledge-based systems. It uses a lazy functional language, N ATURAL E XPERT L ANGUAGE , to implement backward chaining and provide a reliable knowledge processing environment in which development can take place. Customers from all over the world buy the system and have used it to handle a variety of problems, including applications such as airplane servicing and bank loan assessment. Some of these are used 10,000 times or more per month.

A complete unification algorithm is presented for the combination of two arbitrary equational theories E in T(F,X) and E/sup 1/ in T(F',X), where F and F' denote two disjoint sets of function symbols. The method adapts to unification of infinite trees. It is applied to two well-known open problems, when E is the theory of Boolean rings or the theory of Abelian groups, and E is the free theory. The interest to Boolean rings originates in VSLI verification.>