|
- Lambda Calculus with patterns
- The lambda phi-calculus is an extension of the lambda-calculus with a pattern matching facility. The form of the argument of a function can be specified and hence lambda phi-calculus is more convenient than ordinary lambda-calculus. We explore the basic theory of lambda-calculus, investigating properties such as confluence. In doing so, we find some requirements for patterns that guarantee confluence. Our work can be seen as giving some foundations for implementations of functional programming languages.
- Pure Pattern Calculus
- The pure pattern calculus generalises the pure lambda-cal- culus by basing computation on pattern-matching instead of beta-reduc- tion. The simplicity and power of the calculus derive from allowing any term to be a pattern. As well as supporting a uniform approach to func- tions, it supports a uniform approach to data structures which underpins two new forms of polymorphism. Path polymorphism supports searches or queries along all paths through an arbitrary data structure. Pattern polymorphism supports the dynamic creation and evaluation of patterns, so that queries can be customised in reaction to new information about the structures to be encountered. In combination, these features provide a natural account of tasks such as programming with XML paths. As the variables used in matching can now be eliminated by reduction it is necessary to separate them from the binding variables used to con- trol scope. Then standard techniques suffice to ensure that reduction
- Typed Pattern Calculi
- We present a typed pattern calculus with explicit pattern matching and explicit substitutions, where both the typing rules and the reduction rules are modeled on the same logical proof system, namely Gentzen sequent calculus for minimal logic. Our calculus is inspired by the Curry-Howard Isomorphism, in the sense that types, both for patterns and terms, correspond to propositions, terms correspond to proofs, and term reduction corresponds to sequent proof normalization performed by cut elimination. The calculus enjoys subject reduction, confluence, preservation of strong normalization w.r.t a system with meta-level substitutions and strong normalization for well-typed terms. As a consequence, it can be seen as an implementation calculus for functional formalisms defined with meta-level operations for pattern matching and substitutions.
- Basic Pattern Matching Calculi
- The pattern matching calculus is a refinement of lambda-calculus that integrates mechanisms appropriate for fine-grained modelling of non-strict pattern matching. In comparison with the functional rewriting strategy that is usually employed to define the operational semantics of pattern-matching in non-strict functional programming languages like Haskell or Clean, the pattern matching calculus allows simpler and more local definitions to achieve the same effects. The main device of the calculus is to further emphasise the clear distinction between matching failure and undefinedness already discussed in the literature by embedding into expressions the separate syntactic category of matchings. The language arising from that distinction turns out to naturally encompass the pattern guards of Peyton Jones and Erwig and conventional Boolean guards as special cases of the intermediate stages of matching reduction.
- Rewriting Logic
- Rewriting logic (RL) is a natural model of computation and an expressive semantic framework for concurrency, parallelism, communication and interaction. It can be used for specifying a wide range of systems and languages in various application fields. It also has good properties as a framework for representing logics. Several languages based on RL (ASF+SDF, CafeOBJ, ELAN, Maude, etc.) have been designed and implemented.
