Non-free data types are data types whose data have no canonical forms. For example, multisets are non-free data types because the multiset @math has two other equivalent but literally different forms @math and @math . Pattern matching is known to provide a handy tool set to treat such data types. Although many studies on pattern matching and implementations for practical programming languages have been proposed so far, we observe that none of these studies satisfy all the criteria of practical pattern matching, which are as follows: i) efficiency of the backtracking algorithm for non-linear patterns, ii) extensibility of matching process, and iii) polymorphism in patterns. This paper aims to design a new pattern-matching-oriented programming language that satisfies all the above three criteria. The proposed language features clean Scheme-like syntax and efficient and extensible pattern matching semantics. This programming language is especially useful for the processing of complex non-free data types that not only include multisets and sets but also graphs and symbolic mathematical expressions. We discuss the importance of our criteria of practical pattern matching and how our language design naturally arises from the criteria. The proposed language has been already implemented and open-sourced as the Egison programming language.
Functional logic programming @cite_4 is an approach towards this integration. It allows both of non-linear patterns and multiple pattern-matching results. The key difference between the functional logic programming and our approach is in the method for defining pattern-matching algorithms. In functional logic programming, we describe the pattern-matching algorithm for each pattern in the logic-programming style. A function that describes such an algorithm is called a . A pattern constructor takes decomposed values as its arguments and returns the target data. On the other hand, in our proposal, pattern constructors are defined in the functional-programming style: pattern constructors take a target datum as an argument and returns the decomposed values. This enables direct description of algorithms.
@cite_4
2127844749
Abstract We propose an approach to declarative programming which integrates the functional and relational paradigms by taking possibly non-deterministic lazy functions as the fundamental notion. Classical equational logic does not supply a suitable semantics in a natural way. Therefore, we suggest to view programs as theories in a constructor-based conditional rewriting logic. We present proof calculi and a model theory for this logic, and we prove the existence of free term models which provide an adequate intended semantics for programs. We develop a sound and strongly complete lazy narrowing calculus, which is able to support sharing without the technical overhead of graph rewriting and to identify safe cases for eager variable elimination. Moreover, we give some illustrative programming examples, and we discuss the implementability of our approach.