Pattern-Matching-Oriented Programming Language andComputer Algebra System as Its Application（パターンマッチ指向プログラミング言語とその応用としての数式処理システム）

bySatoshi Egi
江木聡志

A Doctor Thesis
博士論文

Submitted to
the Graduate School of the University of Tokyoon December 3, 2021
in Partial Fulﬁllment of the Requirements
for the Degree of Doctor of Information Science andTechnology
in Computer Science
Thesis Supervisor: Masami Hagiya 萩谷昌己
Professor of Computer ScienceABSTRACTA new programming language that widens the range of algorithms that we can concisely describe is important not only because it makes programming of the existing problems easy but also because it widens the scope of computer science by enabling us todeal with problems that we have avoided because programming has been diﬃcult. In thisthesis, we propose the Egison programming language with two independent new features:(i) a pattern-match facility for non-free data types; (ii) a facility for describing tensor
calculus in diﬀerential geometry in a form similar to mathematical formulae using index
notation.
Pattern matching of Egison features user-customizable non-linear pattern matchingwith backtracking. Several non-standard pattern constructs derive from this patternmatch facility: loop patterns and indexed pattern variables for representing the repetitions in a pattern; sequential patterns for controlling the order of pattern matching. In
the ﬁrst half of the thesis, we discuss the design and implementation of this patternmatch facility, classify programming techniques utilizing this pattern-match facility, andadvocates a new paradigm, called pattern-match-oriented programming. Then, we show
three applications of Egison pattern matching. First, we reimplement the basic list processing functions such as delete, concat, and unique and a SAT solver. We can simplify
their implementations by conﬁning explicit recursions for backtracking inside an intuitive pattern. Second, we show that Egison pattern matching provides a uniﬁed querylanguage that can be used for various kinds of databases. Egison pattern matching allows us to describe non-linear patterns for a set, tree, and graph that are executablewith a backtracking algorithm. Third, we show that Egison pattern matching makes theimplementation of a computer algebra system easy because it makes the implementation of a pattern-match engine for mathematical expressions compact. Egison patternmatching has two implementations: an interpreter in Haskell and a library implemented
using Haskell meta-programming. This Haskell library converts Egison pattern matching
to a Haskell program that uses a backtracking monad. We can execute Egison patternmatching as fast as Haskell because we convert Egison pattern matching to an equivalent
Haskell program. A computer algebra system is implemented in the Egison interpreterusing this Haskell library.
Tensor index notation that makes descriptions of tensor calculus in diﬀerential geometry is implemented in this computer algebra system. In the second half of the thesis,
we propose a method for importing tensor index notation into programming. First, we
propose a set of symbolic index reduction rules that allows us to deﬁne tensor operators
in diﬀerential geometry, such as tensor addition and multiplication, partial derivative,
and covariant derivative, without describing index rules that diﬀer for each operator. In
addition, we propose a set of index completion rules that allow us to concisely deﬁneoperators for diﬀerential forms, such as wedge product, exterior derivative, and Hodge
operator. A diﬀerential form is an important concept that allows us to describe formulae
in diﬀerential geometry in a coordinate independent way. It is known that a diﬀerential
form can be represented as an anti-symmetric tensor and expressed by omitting its indices in mathematical formulae. If we express diﬀerential forms as anti-symmetric tensors
with omitted indices in programs as we do in mathematical formulae, we can design a setof index completion rules that conforms to the above index reduction rules. Using thismethod, we can deﬁne operators for diﬀerential forms using tensor operators and index
notation. It makes deﬁnitions of operators for diﬀerential forms concise. In addition, theusers of this computer algebra system can translate mathematical formulae that containboth tensors and diﬀerential forms to programs because both tensor and diﬀerential forms
are represented as tensors and follow the same index rules. Programs of this computer
algebra system are close to a form of formulae in diﬀerential geometry. Therefore, it iseasy to use this computer algebra system even for researchers of mathematics who are
not used to programming.
Finally, we discuss a general method for creating a new language facility by reviewing
the processes of designing these two language facilities. To this end, we divide the processof creating a new language facility into three steps, classify our contributions for the two
language facilities into these three steps, and list commonalities.

論文要旨
簡潔に記述できるアルゴリズムの範囲を広げる新しいプログラミング言語は，既知のコンピュータ科学の問題のプログラミングを簡単にするだけでなく，従来プログラミングが難しいために敬遠されていた問題を扱いやすくし，コンピュータ科学の扱う範囲を広げる
ために重要である．本論文は，(i) 集合や，グラフ，数式のように 1 つの定まった標準形を持たないデータ型に対しても適用可能なパターンマッチと (ii) テンソルの添字記法を使って微分幾何の計算を数式に近い形で記述する機能の 2 つの独立した新しい言語機能をもつ
プログラミング言語 Egison を提案する．

Egison のパターンマッチは，ユーザーがパターンマッチ・アルゴリズムをカスタマイズ可能でかつ，バックトラッキング・アルゴリズムによって実行可能な非線形パターンをサポートするという特徴をもつ．このパターンマッチからは，パターン中の繰り返しを表現するためのループ・パターンと添字付きパターン変数や，パターンマッチの順序を制御するためのシーケンシャル・パターンという新しい種類のパターンが生まれる．本論文の前半では，このパターンマッチ機能をプログラミング言語に実装する手法を述べたあと，このパターンマッチを活かしたプログラミングテクニックをまとめ，パターンマッチ指向プ
ログラミングというパラダイムを提唱する．そして，このパターンマッチの 3 つの応用事
例を通してその有効性を実証する．1 つめに，従来は再帰を使って記述されていたバック
トラッキングのためのループをパターンの中に押し込めることにより，delete や concat，

unique のような基本的なリスト関数と SAT ソルバーを再実装する．2 つめに，集合・ツ
リー・グラフに対してバックトラッキング・アルゴリズムで実行可能な非線形パターンを記述できるために，さまざまな種類のデータベースに対して統一的な形のクエリー言語を提供できることをみせる．3 つめに，数式に対するパターンマッチ・エンジンをコンパクトに実装できるため，数式処理システムの実装が簡単になることをみせる．Egison のパター
ンマッチの実装には，Haskell によるインタプリタと，Haskell のメタプログラミング機能を用いて実装されたライブラリがある．Haskell によるライブラリ実装は，Egison パター
ンマッチをバックトラッキング・モナドを使った Haskell プログラムに変換する．同じ意
味の Haskell プログラムに変換するため，Egison パターンマッチが Haskell と同等の速度で実行できる．この Haskell ライブラリを利用して，Egison インタプリタには数式処理シ
ステムとしての機能が実装されている．
微分幾何に現れるテンソル計算の記述を簡潔にする添字記法は，この数式処理システムに実装されている．本論文の後半では，このテンソル計算を簡潔に表現するための手法を提案する．まず，微分幾何に現れる演算子（テンソルの足し算や掛け算，偏微分，共変微分など）の定義を簡潔にする添字の簡約ルールを提案する．添字の簡約ルールを適切に設計すると，演算子ごとに異なる添字のルールを記述することなしに微分幾何の演算子を定義できる．さらに，微分形式に対する演算子（ウェッジ積，外微分，ホッジ作用素など）の定義を簡潔にする添字の補完ルールを提案する．微分形式は，座標系の選択によらない微分幾何の数式の表現を可能にする重要な概念である．微分形式は歪対称テンソルとして表現できることが知られ，その添字を省略することによって数式の上で表現されることがある．これと同様に，添字が省略された歪対称テンソルとして微分形式をプログラム上で表現すると，上記のテンソルの添字の簡約ルールと適合する添字の補完ルールを設計できる．
この手法を使うと，微分形式の演算子の定義にテンソルの演算子と添字記法が使えるため，

それらの定義が簡潔になる．また，テンソルと微分形式の両方がテンソルとして表現され同一の添字の簡約ルールに従うため，この数式処理システムのユーザーは，テンソルと微分形式が混ざった数式もそのままプログラムに落とすことができる．この数式処理システ
ムのプログラムは微分幾何に現れる数式に近いため，あまりプログラミングに慣れていな
い数学の研究者にとってもこの数式処理システムは扱いやすく，実際の微分幾何の研究で現れる複雑な計量をもつ複素多様体の不変量の計算にこの数式処理システムは既に使われている．
最後に，これら 2 つの言語機能を設計した過程を振り返ることにより，新しい言語機能を作成するための一般的な手法について論じる．そのために，新しい言語機能作成の過程
を 3 つのステップにわけ，本論文で提案した 2 つの言語機能の作成のための貢献をこの 3
つのステップごとに分類し，共通点を列挙する．

Acknowledgements
First of all, I thank my supervisor Masami Hagiya, who provided me with
helpful advice and opportunities to meet and discuss with researchers outside theuniversity.
I thank Yoichi Hirai, Ibuki Kawamata, and Kentaro Honda, Hagiya laboratory
members when I was a graduate student in the Master’s course. They are theﬁrst real users of our language and gave me a lot of constructive feedback.
I thank Yuichi Nishiwaki, who is a current Hagiya laboratory member. Thanks
to collaboration with him, I succeeded in publishing the ﬁrst paper on the patternmatch system of our language.
I thank Ryo Tanaka, Takahisa Watanabe, Takuya Kuwahara, Yasuhiro Yamada, Mayuko Kori, Akira Kawata, Momoko Hattori, and Hiromi Ogawa for
their important contributions to develop our language.
I thank Hiroki Fukagawa, Yutaka Shikano, Takayuki Muranushi, Naoya Umezaki,
Yoshiaki Maeda, and Steven Rosenberg for intensive discussions about diﬀerential
geometry and physics. These discussions motivated me to import the advanced
notations from diﬀerential geometry into programming languages.
I thank Michal J. Gajda, Hiromi Hirano, Matthew Roberts, Kimio Kuramitsu,
Hidehiko Masuhara, Yasunori Harada, and Ikuo Takeuchi for their helpful feedback on our language and papers.
Finally, I thank my colleagues and supervisors in Rakuten, Inc. I especiallythank Yukihiro Matsumoto, Masaya Mori, Will Archer Arentz, Neil Primozich,
Pierre Imai, Yusaku Kaneta, Yu Hirate, Takuya Kitagawa, and Hiroshi Mikitani.
Thanks to their encouragement and support, I can continue my research.

Contents

1 Introduction
1.1 Motivation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
1.2 Pattern-Match-Oriented Programming . . . . . . . . . . . . . . . .
1.3 Importing Mathematical Notations from Tensor Calculus . . . . .
1.4 Outline . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

1
1
2
5
6

2 Design of Pattern-Matching System
2.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
2.2 Motivation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
2.2.1 Pattern Guards vs. Non-linear Patterns . . . . . . . . . . .
2.2.2 Extensible Pattern Matching . . . . . . . . . . . . . . . . .
2.2.3 Monomorphic Patterns vs Polymorphic Patterns . . . . . .
2.3 Proposal . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
2.3.1 The matchAll and match expressions . . . . . . . . . . . .
2.3.2 Eﬃcient Non-linear Pattern Matching with Backtracking .
2.3.3 Polymorphic Patterns . . . . . . . . . . . . . . . . . . . . .
2.3.4 Extensible Pattern Matching . . . . . . . . . . . . . . . . .
2.4 Algorithm . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
2.4.1 Execution Process of Non-linear Pattern Matching . . . . .
2.4.2 Pattern Matching with Inﬁnitely Many Results . . . . . . .
2.5 User-Deﬁned Matchers . . . . . . . . . . . . . . . . . . . . . . . . .
2.5.1 Matcher for Unordered Pairs . . . . . . . . . . . . . . . . .
2.5.2 Case Study: Matcher for Multisets . . . . . . . . . . . . . .
2.5.3 Matcher for Sorted Lists . . . . . . . . . . . . . . . . . . . .
2.6 Formal Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . .
2.7 Related Work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
2.7.1 1980s: Spread of Pattern Matching and Invention of Views
2.7.2 1990s and 2000s: Exploration for Expressive Patterns . . .
2.7.3 2010s: Toward a Uniﬁed Theory of Pattern-Match-Oriented
Programming . . . . . . . . . . . . . . . . . . . . . . . . . .
2.8 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

8
8
10
10
11
11
12
12
13
14
15
16
16
18
19
19
20
21
22
25
26
26

3 Pattern-Matching-Oriented Programming Style
3.1 Overview . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
3.2 Quick Tour of the Egison Pattern-Match-Oriented Language . . . .
3.2.1 Value Patterns and Predicate Patterns for Representing
Non-linear Patterns . . . . . . . . . . . . . . . . . . . . . .
3.2.2 Non-linear Pattern Matching with Backtracking . . . . . .
3.2.3 Ad-hoc Polymorphism of Patterns by Matchers . . . . . . .
3.2.4 matchAllDFS for Controlling the Order of Pattern-Matching
Process . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

28
28
28

vi

27
27

29
29
30
30

3.2.5

3.3

3.4

3.5

3.6

Logical Pattern Constructs: And-Patterns, Or-Patterns,
and Not-Patterns . . . . . . . . . . . . . . . . . . . . . . . .
3.2.6 Loop Patterns for Representing Repetition . . . . . . . . .
3.2.7 Sequential Patterns for Controlling the Order of PatternMatching Process . . . . . . . . . . . . . . . . . . . . . . . .
3.2.8 Matcher Compositions . . . . . . . . . . . . . . . . . . . . .
Pattern-Match-Oriented Programming Design Patterns . . . . . . .
3.3.1 Join-Cons Patterns for Lists — List Basic Functions . . . .
3.3.2 Cons Patterns for Multisets . . . . . . . . . . . . . . . . . .
3.3.3 Tuple Patterns with Sequential Not-Patterns for Comparing Collections . . . . . . . . . . . . . . . . . . . . . . . . .
3.3.4 Loop Patterns in Practice . . . . . . . . . . . . . . . . . . .
Pattern-Match-Oriented Programming in More Practical Situations
3.4.1 SAT Solver . . . . . . . . . . . . . . . . . . . . . . . . . . .
3.4.2 Graph Pattern Matching . . . . . . . . . . . . . . . . . . . .
3.4.3 Computer Algebra . . . . . . . . . . . . . . . . . . . . . . .
3.4.4 Database Query Languages . . . . . . . . . . . . . . . . . .
Related Work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
3.5.1 List Comprehensions . . . . . . . . . . . . . . . . . . . . . .
3.5.2 Comparison with Logic Programming . . . . . . . . . . . .
Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

31
31
32
33
34
34
36
37
37
39
39
41
43
44
45
45
46
47

4 Embedding Egison Pattern Matching into Haskell
4.1 Overview . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
4.1.1 Usage of Sweet Egison . . . . . . . . . . . . . . . . . . . . .
4.1.2 Compiling Method . . . . . . . . . . . . . . . . . . . . . . .
4.1.3 Organization of This Chapter . . . . . . . . . . . . . . . . .
4.2 Typing Rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
4.3 Implementation of Sweet Egison . . . . . . . . . . . . . . . . . . .
4.3.1 Backtracking Monads . . . . . . . . . . . . . . . . . . . . .
4.3.2 Control of Search Strategy . . . . . . . . . . . . . . . . . .
4.3.3 Translation Rules . . . . . . . . . . . . . . . . . . . . . . . .
4.3.4 Deﬁning Matchers . . . . . . . . . . . . . . . . . . . . . . .
4.3.5 Typing the Pattern-Match Expressions . . . . . . . . . . . .
4.3.6 Optimization . . . . . . . . . . . . . . . . . . . . . . . . . .
4.3.7 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . .
4.4 Related Work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
4.5 Performance . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
4.6 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

49
49
49
51
52
52
53
54
55
56
58
60
60
62
62
63
64

5 Computer Algebra System and Tensor Index Notation
5.1 Overview . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
5.2 Related Work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
5.2.1 Syntax-based Approach . . . . . . . . . . . . . . . . . . . .
5.2.2 Library-based Approach . . . . . . . . . . . . . . . . . . . .
5.2.3 Array-Oriented Programming . . . . . . . . . . . . . . . . .
5.2.4 Diﬀerential Forms . . . . . . . . . . . . . . . . . . . . . . .
5.2.5 Symbolic Tensor Calculus . . . . . . . . . . . . . . . . . . .
5.3 Index Reduction Rules for Importing Tensor Index Notation . . . .
5.3.1 Scalar and Tensor Parameters . . . . . . . . . . . . . . . . .
5.3.2 Reduction Rules for Tensors with Indices . . . . . . . . . .
5.3.3 Implementation of Scalar and Tensor Parameters . . . . . .

66
66
66
66
67
68
69
69
69
70
72
74

vii

5.3.4 Inverted Scalar Arguments . . . . . . . . . . . . . . . . . .
5.3.5 The withSymbols Expression . . . . . . . . . . . . . . . . . .
5.3.6 Tensor Declaration . . . . . . . . . . . . . . . . . . . . . . .
5.3.7 Declaring Symmetric and Antisymmetric Tensors . . . . . .
5.3.8 Pattern Matching for Tensor Indices . . . . . . . . . . . . .
Index Completion Rules for Tensors with Omitted Indices . . . . .
5.4.1 Representation of Diﬀerential Forms . . . . . . . . . . . . .
5.4.2 Index Completion Rules . . . . . . . . . . . . . . . . . . . .
Demonstration . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
Evaluation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

75
75
76
76
78
78
79
79
80
81
82

6 Conclusion
6.1 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
6.2 The Three Steps for Creating New Syntax Constructs . . . . . . .
6.2.1 Step 1: Discover a Gap between Our Recognition and Description of an Algorithm . . . . . . . . . . . . . . . . . . .
6.2.2 Step 2: Design New Syntax for Describing Algorithms in a
Form Close to Our Recognition . . . . . . . . . . . . . . . .
6.2.3 Step 3: Design a Method for Executing New Syntax . . . .
6.3 Contributions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
6.4 Future Work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
6.4.1 Increase Application of Pattern-Match-Oriented Programming . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
6.4.2 Implement the Proposed Pattern Matching in Other Programming Languages . . . . . . . . . . . . . . . . . . . . . .
6.4.3 Proof Writing Language . . . . . . . . . . . . . . . . . . . .
6.4.4 Pattern Matching for Wider Range of Data Types . . . . .
6.4.5 Import More Notations from Mathematics . . . . . . . . . .
6.4.6 Expressive Complexity . . . . . . . . . . . . . . . . . . . . .

84
84
84

References

91

5.4

5.5
5.6
5.7

viii

85
86
87
87
88
88
88
89
89
89
89

List of Figures
1.1
1.2
1.3

Pattern matching for poker hand . . . . . . . . . . . . . . . . . . .
Tensor calculus in our language . . . . . . . . . . . . . . . . . . . .
Sympliﬁed index rules . . . . . . . . . . . . . . . . . . . . . . . . .

2
3
7

2.1
2.2
2.3
2.4
2.5

Reduction path of matching states . . . . . . . . . . . . . . . . . .
Search tree . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
Binary reduction tree . . . . . . . . . . . . . . . . . . . . . . . . . .
Syntax of our language . . . . . . . . . . . . . . . . . . . . . . . . .
Formal semantics of our language . . . . . . . . . . . . . . . . . . .

17
19
19
22
23

3.1

Visualization of graphData. . . . . . . . . . . . . . . . . . . . . . . . 42

4.1
4.2
4.3
4.4

Pattern matching for poker hand in Sweet Egison . . . . . . . . . .
Typing rules for matchAll and patterns of Typed Egison . . . . . .
Translation rules of match clauses . . . . . . . . . . . . . . . . . .
Benchmark programs . . . . . . . . . . . . . . . . . . . . . . . . . .

51
53
57
64

5.1
5.2
5.3
5.4
5.5
5.6

Deﬁnition and application of min function . . . . . . . . . . . . . .
Deﬁnition and application of “.” function . . . . . . . . . . . . . .
Representations of Riemann curvature tensor formula . . . . . . .
Pseudo code of index reduction . . . . . . . . . . . . . . . . . . . .
Index rule for partial derivative . . . . . . . . . . . . . . . . . . . .
Program for diﬀerential geometry in our language . . . . . . . . . .

70
71
71
73
75
81

ix

List of Tables
1.1
1.2

Index rules in mathematics . . . . . . . . . . . . . . . . . . . . . .
Our simpliﬁed index rules . . . . . . . . . . . . . . . . . . . . . . .

2.1

Benchmarks of Curry (PAKCS version 2.0.1 and Curry2Prolog(swi7.6) compiler environment) and Egison (version 3.7.12) . . . . . . . 14

4.1
4.2

Execution time of comb2 and perm2 in seconds . . . . . . . . . . . . . 63
Execution time of SAT solvers in seconds . . . . . . . . . . . . . . 64

5.1

The number of lines for deﬁning operators for tensors and diﬀerential forms . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 82x66

Chapter 1
Introduction
1.1

Motivation

The advance of science is inextricably linked with the evolution of notation. New
scientiﬁc knowledge leads to the invention of new notations, and new notations
accelerate the advance of science. The evolution of numeric notation is an obvious example. The numeric notation has been evolved utilizing our knowledge ofarithmetic. The evolved numeric notation (e.g., decimal notation) allows us to
identify numbers with less eﬀort and plays an important role in deepening ourknowledge. New scientiﬁc knowledge does not only evolve the existing notation
but also expand the target area of notation. The invention of a programming language, a set of notations for describing algorithms, is an example. The inventionof computers leads us to use programming languages for describing algorithms
instead of natural languages. From the latter half of the twentieth century, many
notations have been invented in the ﬁeld of programming languages. Lexicalscoping [20], high-order functions [63, 52], and pattern matching [24] are features
speciﬁc to programming invented for describing algorithms.
In this thesis, we aim to develop a programming language that expands therange of algorithms that we can describe without translating our recognition of
the algorithms for computers. We propose the Egison programming languagewith two independent new features: (i) a pattern-match facility for non-free datatypes; (ii) a facility for describing tensor calculus in diﬀerential geometry in a form
similar to mathematical formulae using index notation. The proposed language
has already been implemented and is open-sourced.
Non-free data types are data types whose data have no canonical forms. For
example, multisets are non-free data types because the multiset {a, b, b} has twoother equivalent but literally diﬀerent forms {b, a, b} and {b, b, a}. We developed
the pattern-match facility for non-free data types. Pattern matching for poker
hands is a simple example of our pattern matching. In Figure 1.1, all poker hands
are described in a single pattern. When designing the syntax of our language,
we aimed to make this poker hand program as concise as possible. This concise
deﬁnition of poker hands is achieved by three features of our pattern match facility. First, in line 2 we specify that we pattern-match a list of playing cards
as a multiset of cards. For determining poker hand, we do not care about theorder of the cards. By pattern matching as a multiset, we can write a pattern
without taking care of the order of the cards. In our language, the pattern-match
method for multisets is not built-in. The users can deﬁne pattern-match methods
for each non-free data type including multisets in our language. Second, we use
non-linear patterns for describing each poker hand. Non-linear patterns allow
multiple occurrences of the same variables in a pattern. For example, we use

1

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19

def poker cs :=match cs as multiset card with
| [card $s $n, card #s #(n-1), card #s #(n-2), card #s #(n-3), card #s #(n-4)]-> "Straight flush"| [card _ $n, card _ #n, card _ #n, card _ #n, _]-> "Four of a kind"| [card _ $m, card _ #m, card _ #m, card _ $n, card _ #n]-> "Full house"| [card $s _, card #s _, card #s _, card #s _, card #s _]-> "Flush"| [card _ $n, card _ #(n-1), card _ #(n-2), card _ #(n-3), card _ #(n-4)]-> "Straight"| [card _ $n, card _ #n, card _ #n, _, _]-> "Three of a kind"| [card _ $m, card _ #m, card _ $n, card _ #n, _]-> "Two pair"| [card _ $n, card _ #n, _, _, _]-> "One pair"| [_, _, _, _, _] -> "Nothing"

Figure 1.1: Pattern matching for poker hand
non-linear patterns for describing that all cards have the same suit (the value
pattern #s matches the value bound to the pattern variable $s). For handling
non-linear patterns, we need to traverse the search trees for pattern matchingeﬃciently because non-free data have multiple decompositions. Our main technical challenge is to achieve both the customizability of pattern-match methods
and the expressive patterns simultaneously. In this thesis, we present how wedesigned such a language.
By importing the mathematical notations in tensor calculus into programming, we aim to make programs for tensor calculus concise. Figure 1.2a shows
the samples of formulae in tensor calculus. In Figure 1.2b, we express these formulae in our language. We can observe that each term in the formulae is directlytranslated into our language. Figure 1.2c shows the deﬁnition of tensor operatorsthat appear in Figure 1.2b. Each tensor operator is deﬁned in one line. Our mainachievement in tensor calculus is that we enable the direct translation of a formula that uses tensor index notation, keeping the deﬁnition of tensor operators
concise. For this purpose, we have reorganized the mathematical deﬁnition of
tensor notations because the semantics of some notations are vague and complex
to implement them as a part of programming languages.
There is great signiﬁcance in the study of notation itself. There are several
interesting problems: “Is there a general way to ﬁnd a new notation?”, “Is there
a formal method for measuring the superiority of multiple notations?” Getting
close to the answers to these questions is the underlying motivation of this work.

1.2

Pattern-Match-Oriented Programming

How do you answer the question, “What is the map function?” We believe mostpeople answer as follows:
1. “The map function takes a function and a list and returns a list of theresults of applying the function to all the elements of the list.”
Few people answer as follows:2

Rijkl =

∂Γijl

∂Γijk

∂x

∂xl

−
k

+ Γmjl Γimk − Γmjk Γiml

Ωij = dω ij + ω ik ∧ ω kj(a) Mathematical formulae in tensor calculus
def R~i_j_k_l := withSymbols [m]∂/∂ Γ~i_j_l x~k - ∂/∂ Γ~i_j_k x~l + Γ~m_j_l . Γ~i_m_k - Γ~m_j_k . Γ~i_m_l
def Ω~i_j := withSymbols [k]antisymmetrize (d ω~i_j + ω~i_k ∧ ω~k_j)(b) The above formulae in our languagedef (.) %t1 %t2 := contractWith (+) (t1 * t2)
def d %A := !(flip ∂/∂) coord A
def (∧) %A %B := A !. B(c) Deﬁnition of tensor operators in our language

Figure 1.2: Tensor calculus in our language
2. “The map function takes a function and a list and returns an empty list if
the argument list is empty. Otherwise, it returns a list whose head element
is the result of applying the function to the head element of the argument
list, and the tail part is the result of applying the map function recursively
to the tail part of the argument list.”
Obviously, there is a signiﬁcant gap between these two explanations. The
former explanation is simpler and more straightforward than the latter. However,the current functional deﬁnition of map is based on the latter.
map _ [] = []map f (x : xs) = (f x) : (map f xs)

Interestingly, this basic deﬁnition of map has been almost unchanged for 60 years
since McCarthy ﬁrst presented the deﬁnition of maplist in [62]. The only diﬀerenceis a way for describing conditional branches: McCarthy uses predicates, whereas
Haskell uses pattern matching.
maplist[x ;f] = [null[x] -> NIL; T -> cons[f[car[x]]; maplist[cdr[x]; f]]]Recursion used in the above deﬁnitions is a mathematically simple but powerful framework for representing computations and has been a very basic constructof functional programming for describing loops in programs. Recursion is heavily
used for deﬁnitions of many basic functions such as filter, concat, and unique andmost of them are also simple enough.
However, as mentioned earlier, there does exist a substantial cognitive distance
between the recursive deﬁnition and the simplest explanation of that deﬁnition.
To illustrate this gap, we deﬁne mapWithBothSides, a variation of map. We often meeta situation to deﬁne a variant of basic functions speciﬁc to a target algorithm.
Deﬁning these utility functions is one of the cumbersome tasks in programming.
Therefore, considering a comfortable method for deﬁning these utility functions
is important.
3

mapWithBothSides takes a function of three arguments and a list, and returns alist of applying the function for all three tuples consisting of an initial preﬁx, thenext element, and the remaining suﬃx. mapWithBothSides is used for generating
lists by rewriting the element of an input list. This function is useful for handling
logical formulae, for example. We deﬁne mapWithBothSides with a helper function
as follows.
mapWithBothSides f xs = mapWithBothSides' f [] xs
where
mapWithBothSides' f xs [] = []mapWithBothSides' f xs (y : ys) = (f xs y ys) : (mapWithBothSides' f (xs ++ [y]) ys)The explanation of map given at the beginning and the above explanation of
mapWithBothSides are similar, and their deﬁnitions should be similar to each other.
However, their deﬁnitions are very diﬀerent from each other. A hint for ﬁlling
the gap is hidden behind these diﬀerences.
The cause of these diﬀerences is the lack of a pattern like hs ++ ts that divides a target list into an initial preﬁx and the remaining suﬃx. For example,
the list [1,2] has multiple decompositions for the pattern hs ++ ts: [] ++ [1,2],[1] ++ [2], and [1,2] ++ []. We call this pattern a join pattern. Unlike traditional
pattern matching for algebraic data types, this pattern has multiple decompositions. Pattern matching that can handle multiple results is necessary for handlingjoin patterns.
In our language Egison whose distinguishing feature is non-linear patternmatching with backtracking [38], we can deﬁne map and mapWithBothSides concisely
and in a very similar way. In fact, the author got an idea of the language when
he implemented mapWithBothSides for implementing an automated theorem conjecturer.
def map f xs := matchAll xs as list something with _ ++ $x :: _ -> f x
def mapWithBothSides f xs := matchAll xs as list something with $hs ++ $x :: $ts-> f hs x ts

In the above program, the join pattern is eﬀectively used. matchAll is a key
built-in syntactic construct of Egison for handling multiple pattern-matching results. matchAll collects all the pattern-matching results and returns a collection
where the body expression has been evaluated for each result. matchAll takes one
additional argument matcher that is list something in the above cases. A matcher
is an Egison speciﬁc object that knows how to decompose the target following the
given pattern. The matcher is speciﬁed between as and with, which are reserved
words. list is a user-deﬁned function that takes a matcher for the elements andreturns a matcher for lists. list deﬁnes a method for interpreting the cons (::)
and join (++) pattern. something is the only built-in matcher in Egison. somethingcan be used for pattern-matching arbitrary objects but can handle only patternvariables and wildcards. As a result, list something is evaluated as a matcher
for pattern-matching a list of arbitrary objects. _ that appears in a pattern is a
wildcard. Pattern variables are prepended with $.
These deﬁnitions of the variations of map are close to the explanation of map
given at the beginning. We achieved this by hiding the recursions in the deﬁnition of list, which deﬁnes the pattern-matching algorithm for the join patterns.
We call this programming style that replaces explicit recursions with intuitive
patterns, pattern-match-oriented programming style.
In this thesis, we advocate pattern-match-oriented programming as a new programming paradigm. Pattern-match-oriented programming is a paradigm that4

makes descriptions of algorithms concise by replacing loops for traversal andenumeration that can be done by simple backtracking. These loops are mixed inprograms with loops that are essential for lowering the time complexity of algorithms and make programs complicated. Pattern-match-oriented programming
separates these two kinds of loops and allows programmers to concentrate on
describing the essential part of algorithms.
The above examples show just a part of the expressiveness of pattern-matchoriented programming. For example, non-linear patterns enable to describe more
popular list processing functions such as unique and intersect in pattern-matchoriented style. Furthermore, pattern matching for general non-free data types(e.g., multisets, sets, and mathematical expressions) diversiﬁes the applications ofpattern-match-oriented programming signiﬁcantly. This thesis introduces full features of the Egison pattern-match-oriented programming language and presents
all the techniques we discovered so far for replacing explicit recursions with an
intuitive pattern.

1.3

Importing Mathematical Notations from Tensor Calculus

Programming languages are evolved also by importing notations from mathematics. For example, decimal number system, function modularization, and inﬁx
notation for basic arithmetic operators have been imported in most programming languages [19]. Importing mathematical notations into programming issometimes diﬃcult. This is because the semantics of some mathematical notations are vague and complex to implement as a part of programming languages.
For example, tensor index notation invented by Ricci and Levi-Civita [71] for
dealing with high-order tensors is one such notation.
The latter part of this thesis discusses a method for importing tensor index notation into programming languages. Tensor calculus often appears in thevarious ﬁelds of computer science. Tensor calculus is an important applicationof symbolic computation [57]. Tensor calculus is heavily used in computational
physics [49] and computer visions [47]. Tensor calculus also appears in machinelearning to handle multidimensional data [50]. Importing tensor index notation
makes programming in these ﬁelds easy.
Importing tensor index notation into programming languages is diﬃcult because the symbolic index rules vary by operators, especially by tensor addition
and multiplication as shown in Table 1.1. We will show examples. Let u and v
be vectors:• the expression ui + vi returns a vector, but ui vi is an invalid expression;(The expression ui vi returns the inner product in Euclidean spaces where
we can switch a superscript and a subscript freely. But we do not take thisexception into account.)• the expression ui + vi is an invalid expression, but ui vi is valid and returns
the inner product;• the expression ui + vj is an invalid expression, but ui vj is valid and returns
the tensor product.
Thus, each tensor operator has diﬀerent symbolic index rules. Therefore, weneed to specify symbolic index rules for each function when deﬁning them. It
is a verbose task. Furthermore, we need to design a syntactic construct for
describing index rules. Such a new syntactic construct makes a programming
language complex.
5

Tensor addition
ui + vi returns a vector
ui + vj is invalid
ui + vi is invalid

Tensor multiplication
ui vi is invalidui vj returns a matrix
ui vi returns a scalar

Table 1.1: Index rules in mathematics
Tensor addition
ui + vi returns a vector
ui + vj returns a matrix
ui + vi returns a matrix

Tensor multiplication
ui vi is invalidui vj returns a matrix
ui vi returns a scalar

Table 1.2: Our simpliﬁed index rules
We propose simpliﬁed symbolic index rules shown in Table 1.2 to avoid thisproblem. Our simpliﬁed rules keep all the mathematically valid expressions valid.
However, some mathematically invalid expressions become valid. For example,
vi + vj is an invalid expression in mathematics but a valid expression in our rules.
Figure 1.3a shows our simpliﬁed index rules for tensor addition. By relaxing
the rules that way, we can regard many tensor operators as variations of tensor
addition. For example, tensor multiplication is regarded as an operation that has
an additional procedure, contraction, after multiplying each component of tensors
in the same way as tensor addition (ﬁgure 1.3b). Contraction is an operation tosum up the diagonal components of a tensor when the tensor has a superscript andsubscript with an identical symbol. This point of view reduces the descriptionsof symbolic index rules for deﬁning tensor operators. We show that various
operators in diﬀerential geometry can be deﬁned concisely.
Furthermore, we propose index completion rules for omitted tensor indices.
We show that our index completion rules enable us to deﬁne operators for differential forms such as the wedge product, exterior derivative, and Hodge star
operator.
In our language, we can describe a program whose form is close to formulae in diﬀerential geometry. Therefore, it is easy to use this computer algebra
system even for researchers of mathematics who are not used to programming.
Due to this advantage, our language already has been applied in the research ofmathematics [37].

1.4

Outline

The rest of thesis is organized as follows. Chapter 2 proposes a criteria thatshould be fulﬁlled for practical pattern matching for non-free data types and designs our programming language that satisﬁes the criteria. Chapter 3 discusses
how programming changes by utilizing our pattern-match system and proposes a
new programming paradigm called pattern-match-oriented programming. Chapter 4 presents our Haskell library that embeds our pattern-match system into
Haskell. For this purpose, we design a set of typing rules and develop a method
for transforming our pattern-match expression to a Haskell program that uses
backtracking monad. Chapter 5 presents the method for importing notations of
tensor calculus into programming languages. The ﬁnal chapter summarizes the

6

( )
( )
(
)
a
c
a+c
+
=
b i
d i
b+d i
( )
( )
(
a
c
a+c
+
=
b i
d j
b+c

a+d
b+d

( )
( )i (
a
c
a+c
+
=
b i
d
b+c

a+d
b+d

( ) ( )
( )
a
c
ac
=
b i d i
bd i
)
ij

)i
i

(a) Sympliﬁed index rules for addition( ) ( )(acac=b i d j
bc

ad
bd

)
ij

( ) ( )i
(
)i
a
c
ac ad
= contract= ac + bd
b i d
bc bd i(b) Sympliﬁed index rules for multiplication

Figure 1.3: Sympliﬁed index rules
thesis and discusses future work.

7

Chapter 2
Design of Pattern-Matching System
2.1

Introduction

Pattern matching is an important feature of programming languages featuring
data abstraction mechanisms. Data abstraction serves users with a simple method
for handling data structures that contain plenty of complex information. Using pattern matching, programs using data abstraction become concise, humanreadable, and maintainable. Most of the recent practical programming languages
allow users to extend data abstraction e.g. by deﬁning new types or classes, orby introducing new abstract interfaces. Therefore, a good programming languagewith pattern matching should allow users to extend its pattern-matching facility
akin to the extensibility of data abstraction.
Earlier, pattern-matching systems used to assume a one-to-one correspondence between patterns and data constructors. However, this assumption became
problematic when one handles data types whose data have multiple representations. To overcome this problem, Wadler proposed the pattern-matching system
views [92] that broke the symmetry between patterns and data constructors.
Views enabled users to pattern-match against data represented in many ways.
For example, a complex number may be represented either in polar or Cartesianform, and they are convertible to each other. Using views, one can pattern-matcha complex number internally represented in polar form with a pattern written in
Cartesian form, and vice versa， provided that mutual transformation functions
are properly deﬁned. Similarly, one can use the Cons pattern to perform patternmatching on lists with joins, where a list [1,2] can be either (Cons 1 (Cons 2 Nil))or (Join (Cons 1 Nil) (Cons 2 Nil)), if one deﬁnes a normalization function of lists
with join into a sequence of Cons.
However, views require data types to have a distinguished canonical form
among many possible forms. In the case of lists with join, one can pattern-matchwith Cons because any list with join is canonically reducible to a list with joinwith the Cons constructor at the head. On the other hand, for any list with join,
there is no such canonical form that has Join at the head. For example, the list
[1,2] may be decomposed with Join into three pairs: [] and [1,2], [1] and [2],and [1,2] and []. For that reason, views do not support pattern matching of lists
with join using the Join pattern.
Generally, data types without canonical forms are called non-free data types.
Mathematically speaking, a non-free data type can be regarded as a quotient ona free data type over an equivalence. An example of non-free data types is, ofcourse, a list with join: it may be viewed as a non-free data type composed of a(free) binary tree equipped with an equivalence between trees with the same leaf
nodes enumerated from left to right, such as (Join Nil (Cons 1 (Cons 2 Nil))) =8

(Join (Cons 1 Nil) (Cons 2 Nil)). Other typical examples include sets and multi-sets, as they are (free) lists with obvious identiﬁcations. Generally, as shown forlists with join, pattern matching on non-free data types yields multiple results. ∗For example, multiset {1,2,3} has three decompositions by the insert pattern:
insert(1,{2,3}), insert(2,{1,3}), and insert(3,{1,2}). Therefore, how tohandle multiple pattern-matching results is an extremely important issue when
we design a programming language that supports pattern matching for non-freedata types.
On the other hand, pattern guard is a commonly used technique for ﬁltering such multiple results from pattern matching. Basically, pattern guards areapplied after enumerating all pattern-matching results. Therefore, substantial
unnecessary enumerations often occur before the application of pattern guards.
One simple solution is to break a large pattern into nested patterns to apply pattern guards as early as possible. However, this solution complicates the programand makes it hard to maintain. It is also possible to statically transform the program in a similar manner at the compile time. However, it makes the compiler
implementation very complex. Non-linear pattern is an alternative method forpattern guard. Non-linear patterns are patterns that allow multiple occurrencesof the same variables in a pattern. Compared to pattern guards, they are not only
syntactically beautiful but also compiler-friendly. Non-linear patterns are easier
to analyze and hence can be implemented eﬃciently (Section 2.2.1 and 2.3.2).
However, it is not obvious how to extend a non-linear pattern-matching system
to allow users to deﬁne an algorithm to decompose non-free data types. We
introduce extensible pattern matching to remedy this issue (Section 2.2.2, 2.3.4,
and 2.5). Extensibility of pattern matching also enables us to deﬁne predicate patterns, which are typically implemented as a built-in feature (e.g. pattern guards)
in most pattern-matching systems. Additionally, we improve the usability of pattern matching for non-free data types by introducing a syntactic generalization
for the match expression, called polymorphic patterns (Section 2.2.3 and 2.3.3).
We also present a non-linear pattern-matching algorithm specialized for backtracking on inﬁnite search trees and supports pattern matching with inﬁnitely
many results in addition to keeping eﬃciency (Section 2.4).
In this chapter, we aim to design a programming language that is oriented
toward pattern matching for non-free data types. We summarize the above argument in the form of three criteria that must be fulﬁlled by a language in order
to be used in practice:
1. Eﬃciency of the backtracking algorithm for non-linear patterns,
2. Extensibility of pattern matching, and
3. Polymorphism in patterns.
We believe that the above requirements, called together criteria of practical pattern matching, are fundamental for languages with pattern matching. However,none of the existing languages and studies [5, 39, 89, 18] fulﬁll all of them. In
the rest of the chapter, we present a language that satisﬁes the criteria, together
with comparisons with other languages, several working examples, and formal
semantics. We emphasize that our proposal has been already implemented in
Haskell as the Egison programming language, and is open-sourced [30].
∗In fact, this phenomenon that “pattern matching against a single value yields multiple
results” does not occur for free data types. This is the unique characteristic of non-free datatypes.

9

The rest of the chapter is organized as follows. Section 2.2 analyzes the capabilities of the prior work for handling non-free data types and clariﬁes the
problems to be solved. Section 2.3 shows our design of pattern-match expressions that solves the problems introduced in Section 2.2. Section 2.4 explains theinternal algorithm for executing pattern-match expressions in Section 2.3. Section 2.5 explains how users customize the pattern-match method for each non-freedata type in our system. Section 2.6 shows the formal semantics of our language.
Section 2.7 introduces the prior work on pattern-match extensions. Section 2.8
concludes this chapter.

2.2

Motivation

In this section, we discuss the requirements for programming languages to establish practical pattern matching for non-free data types.
2.2.1

Pattern Guards vs. Non-linear Patterns

Compared to pattern guards, non-linear patterns are a compiler-friendly method
for ﬁltering multiple matching results eﬃciently. However, non-linear patternmatching is typically implemented by converting them to pattern guards. For
example, some implementations of functional logic programming languages convert non-linear patterns to pattern guards [18, 17, 44]. This method is ineﬃcientbecause it leads to enumerating unnecessary candidates. In the following program in Curry, seqN returns "Matched" if the argument list has a sequential N-tuple.
Otherwise, it returns "Not matched". insert is used as a pattern constructor fordecomposing data into an element and the rest ignoring the order of elements.
We will explain the deﬁnition of insert in Section 3.5.2.2.
seq2 (insert x (insert (x+1) _)) = "Matched"seq2 _ = "Not matched"seq3 (insert x (insert (x+1) (insert (x+2) _))) = "Matched"seq3 _ = "Not matched"seq4 (insert x (insert (x+1) (insert (x+2) (insert (x+3) _)))) = "Matched"seq4 _ = "Not matched"seq2 (take 10 (repeat 0)) -- returns "Not matched" in O(n^2) time
seq3 (take 10 (repeat 0)) -- returns "Not matched" in O(n^3) time
seq4 (take 10 (repeat 0)) -- returns "Not matched" in O(n^4) time

When we use a Curry compiler such as PAKCS [4] and KiCS2 [23], we see that“seq4 (take n (repeat 0))” takes more time than “seq3 (take n (repeat( 0))) ” benfollows.
Therefore,
seq4 enumerates 4 candicause seq3 is compiled to seq3' as( )dates, whereas seq3 enumerates n3 candidates before ﬁltering the results. If the
program uses non-linear patterns as in seq3, we easily ﬁnd( )that we can check nosequential triples or quadruples exist simply by checking n2 pairs. However, suchinformation is discarded during the program transformation into pattern guards.
seq3' (insert x (insert y (insert z _))) | y==x+1 && z==x+2 = "Matched"seq3' _ = "Not matched"

One way to make this program eﬃcient in Curry is to stop using non-linear
patterns and instead use a predicate explicitly in pattern guards. The following
illustrates such a program.
isSeq2 (x:y:rs) = y == x+1

10

isSeq3 (x:rs) = isSeq2 (x:rs) && isSeq2 rs
perm [] = []perm (x:xs) = insert x (perm xs)
seq3 xs | isSeq3 ys = "Matched" where ys = perm xs
seq3 _ = "Not matched"seq3 (take 10 (repeat 0))-- returns "Not matched" in O(n^2) time

isSeq2 and isSeq3 checks whether the elements of the head part of the argument

list are in sequence or not. perm returns all the permutations of the argument
list. In the program, because of laziness, only the head part of the list is evaluated. In addition, because of sharing [41], the common head part of the list ispattern-matched only once. Using this call-by-need-like strategy enables eﬃcientpattern matching on sequential n-tuples. However, this strategy sacriﬁces thereadability of programs and makes the program obviously redundant. Instead,we base our work on non-linear patterns and attempt to improve its usability
keeping it compiler-friendly and syntactically clean.
2.2.2

Extensible Pattern Matching

As a program gets more complicated, data structures involved in the program getcomplicated as well. A pattern-matching facility for such data structures (e.g.
graphs and mathematical expressions) should be extensible and customizable byusers because it is impractical to provide the data structures for these data types
as built-in data types in general-purpose languages.
In the studies of computer algebra systems, eﬃcient non-linear pattern-matchingalgorithms for mathematical expressions that avoid such unnecessary search havealready been proposed [2, 58]. Generally, users of such computer algebra systems
control the pattern-matching method for mathematical expressions by specifying
attributes for each operator. For example, the Orderless attribute of the Wolfram
language indicates that the order of the arguments of the operator is ignored [3].
However, the set of attributes available is ﬁxed and cannot be changed [1]. Thismeans that the pattern-matching algorithms in such computer algebra systems
are specialized only for some speciﬁc data types such as multisets. However, there
are a number of data types we want to pattern-match other than mathematicalexpressions, like unordered pairs, trees, and graphs.
Thus, extensible pattern matching for non-free data types is necessary forhandling complicated data types such as mathematical expressions. In this chapter, we design a language that allows users to implement eﬃcient backtracking
algorithms for general non-free data types by themselves. It provides users withthe equivalent power to add new attributes freely by themselves. We discuss this
topic again in Section 2.3.4.
2.2.3

Monomorphic Patterns vs Polymorphic Patterns

Polymorphism of patterns is useful for reducing the number of names used as
pattern constructors. If patterns are monomorphic, we need to use diﬀerent
names for pattern constructors with similar meanings. As such, monomorphic
patterns are error-prone.
For example, the pattern constructor that decomposes a collection into anelement and the rest ignoring the order of the elements is bound to the nameinsert in the sample code of Curry [18] as in Section 2.2.1. The same pattern11

constructor’s name is Add' in the sample program of Active Patterns [39]. However, these can be considered as a generalized cons pattern constructor for lists tomultisets, because they are the same at the point that both of them are a patternconstructor that decomposes a collection into an element and the rest.
Polymorphism is important, especially for value patterns. A value pattern isa pattern that matches when the value in the pattern is equal to the target. It
is an important pattern construct for expressing non-linear patterns. If patterns
are monomorphic, we need to prepare diﬀerent notations for value patterns ofdiﬀerent data types. For example, we need to have diﬀerent notations for value
patterns for lists and multisets. This is because the equivalence of objects as lists
and multisets are not equal although both lists and multisets are represented asa list.
pairsAsLists (insert x (insert x _)) = "Matched"pairsAsLists _ = "Not matched"pairsAsMultisets (insert x (insert y _)) | (multisetEq x y) = "Matched"pairsAsMultisets _ = "Not matched"pairsAsLists [[1,2],[2,1]]-- returns "Not matched"pairsAsMultisets [[1,2],[2,1]] -- returns "Matched"

2.3

ProposalIn this section, we introduce our pattern-matching system, which satisﬁes all
requirements shown in Section 2.2. Our language has Haskell-like syntax. It is
dynamically typed, and as well as Curry, based on lazy evaluation.
2.3.1

The matchAll and match expressions

We explain the matchAll expression. It is a primitive syntax of our language. It
supports pattern matching with multiple results.
We show a sample program using matchAll in the following. In this thesis, weshow the evaluation result of a program in the comment that follows the program.
“--” is the inline comment delimiter of the proposed language.
matchAll [1, 2, 3] as list integer with$xs ++ $ys -> (xs, ys)-- [([], [1, 2, 3]), ([1], [2, 3]), ([1, 2], [3]), ([1, 2, 3], [])]
matchAll is composed of an expression called target, matcher, and match clause,

which consists of a pattern and body expression. The matchAll expression evaluates
the body of the match clause for each pattern-matching result and returns a(lazy) collection that contains all results. In the above code, we pattern-matchthe target [1, 2, 3] as a list of integers using the pattern $xs ++ $ys. list integer
is a matcher to pattern-match the pattern and target as a list of integers. The
pattern is constructed using the join pattern constructor. $xs and $ys are called
pattern variables. We can use the result of pattern matching referring to them.
A matchAll expression ﬁrst consults the matcher on how to pattern-match thegiven target and the given pattern. Matchers know how to decompose the target
following the given pattern and enumerate the results, and matchAll then collects
the results returned by the matcher. In the sample program, given a join pattern,
list integer tries to divide a collection into two collections. The collection [1,2, 3] is thus divided into two collections in four ways.

12matchAll can handle pattern matching that may yield inﬁnitely many results.

For example, the following program extracts all twin primes from the inﬁnite listof prime numbers∗ . We will discuss this mechanism in Section 2.4.2.
def twinPrimes :=matchAll primes as list integer with
| _ ++ $p :: #(p + 2) :: _ -> (p, p + 2)
take 6 twinPrimes-- [(3, 5), (5, 7), (11, 13), (17, 19), (29, 31), (41, 43)]

There is another primitive syntax called match expression. While matchAll returns a collection of all matched results, match short-circuits the pattern matchingprocess and immediately returns if any result is found. Another diﬀerence frommatchAll is that it can take multiple match clauses. It tries pattern matching
starting from the head of the match clauses， and tries the next clause if it fails.
Therefore, match is useful when we write conditional branching.
However, match is inessential for our language. It is implementable in terms ofthe matchAll expression and macros. The reason is that the matchAll expression isevaluated lazily, and, therefore, we can extract the ﬁrst pattern-matching result
from matchAll without calculating other pattern-matching results simply by usingcar. We can implement match by combining the matchAll and if expressions using
macros. Furthermore, if is also implementable in terms of the matchAll andmatcher expression as follows. We will explain the matcher expression in Section 2.5.
For that reason, we only discuss the matchAll expression in the rest of the chapter.
defMacro if b e1 e2 :=head (matchAll b as matcher$ as something with
| True -> [e1]| False -> [e2]
| $x -> x)

2.3.2

Eﬃcient Non-linear Pattern Matching with Backtracking

We have designed our language to handle non-linear patterns eﬃciently. For
example, the calculation time of the following code does not depend on the patternlength. Both of the following examples take O(n2 ) time to return the result.
matchAll take n (repeat 0) as multiset integer with
| $x :: #(x + 1) :: _ -> x-- returns {} in O(n^2) time
matchAll take n (repeat 0) as multiset integer with
| $x :: #(x + 1) :: #(x + 2) :: _ -> x-- returns {} in O(n^2) time

In our proposal, a pattern is examined from left to right in order, and the binding
to a pattern variable can be referred to in the right side of the pattern. In theabove examples, the pattern variable $x is bound to any element of the collection
since the pattern constructor is insert. After that, the patterns “#(x + 1)” and“#(x + 2)” are examined. A pattern that begins with “#” is called a value pattern.
The expression following “#” can be any kind of expression. The value patterns
match with the target data if the target is equal to the content of the pattern.
∗

We will explain the meaning of the value pattern #(p + 2) and the cons pattern constructor
in Section 2.3.2 and 2.3.3, respectively.

13

Therefore, after successful pattern matching, $x is bound to an element thatappears multiple times.
We can more elaborately discuss the diﬀerence in the eﬃciency of non-linear
patterns and pattern guards in general cases. The time complexity involved inpattern guards is O(np+v ) when the pattern matching fails, whereas the timecomplexity involved in non-linear patterns is O(np+min(1,v) ), where n is the sizeof the target object∗ , p is the number of pattern variables, and v is the number ofvalue patterns. The diﬀerence between v and min(1, v) comes from the mechanism of non-linear pattern matching that backtracks at the ﬁrst mismatch of thevalue pattern.
Curry
seq2
seq3
seq4

n=15
1.18s
1.42s
3.37s

n=25
1.20s
2.10s
16.42s

n=30
1.29s
2.54s
34.19s

n=50
1.53s
7.40s
229.51s

Egison
seq2
seq3
seq4

n=15
0.26s
0.25s
0.25s

n=25
0.34s
0.34s
0.34s

n=30
0.43s
0.46s
0.42s

n=50
0.84s
0.82s
0.78s

n=100
2.54s
50.66s
3667.49s

n=100
2.72s
2.66s
2.47s

Table 2.1: Benchmarks of Curry (PAKCS version 2.0.1 and Curry2Prolog(swi7.6) compiler environment) and Egison (version 3.7.12)
Table 2.1 shows microbenchmark results of non-linear pattern matching forCurry and Egison. The table shows execution times of the Curry program presented in Section 2.2.1 and the corresponding Egison program as shown above.
The environment we used was Ubuntu on VirtualBox with 2 processors and 8GB
memory hosted on MacBook Pro (2017) with 2.3 GHz Intel Core i5 processor. We
can see that the execution times in two implementations follow the theoreticalcomputational complexities discussed above. We emphasize that these benchmark results do not mean Curry is slower than Egison. We can write the eﬃcient
programs for the same purpose in Curry if we do not persist in using non-linear
patterns. Let us also note that the current implementation of Egison is not tuned
up and comparing constant times in two implementations is nonsense.
Value patterns are not only eﬃcient but also easy to read once we are used
to them because it enables us to read patterns in the same order the execution
process of pattern matching goes. It also reduces the number of new variables
introduced in a pattern. We explain the mechanism of how the proposed system
executes the above pattern matching eﬃciently in Section 2.4.
2.3.3

Polymorphic Patterns

The characteristic of the proposed pattern-matching expression is that they takea matcher. This ingredient allows us to use the same pattern constructors fordiﬀerent data types.
For example, one may want to pattern-match a collection [1, 2, 3] sometimes as a list and other times as a multiset or a set. For these three types, we cannaturally deﬁne similar pattern-matching operations. One example is the cons
pattern, which is also called insert in Section 2.2.1 and 2.3.2. Given a collection,∗

Here, we suppose that the number of decompositions by each pattern constructor can beapproximated by the size of the target object.

14pattern $x :: $rs divides it into the “head” element and the rest. When we use
the cons pattern for lists, it either yields the result which is uniquely determinedby the constructor, or just fails when the list is empty. On the other hand, formultisets, it non-deterministically chooses an element from the given collection
and yields many results. By explicitly specifying which matcher is used in match
expressions, we can uniformly write such programs in our language:
matchAll [1, 2, 3] as list integer with
| $x :: $rs -> (x, rs)-- [(1, [2, 3])]matchAll [1, 2, 3] as multiset integer with
| $x :: $rs -> (x, rs)-- [(1, [2, 3]), (2, [1, 3]), (3, [1, 2])]
matchAll [1, 2, 3] as set integer with
| $x :: $rs -> (x, rs)-- [(1, [1, 2, 3]), (2, [1, 2, 3]), (3, [1, 2, 3])]In the case of lists, the head element $x is simply bound to the ﬁrst element of thecollection. On the other hand, in the case of multisets or sets, the head element
can be any element of the collection because we ignore the order of elements. In
the case of lists or multisets, the rest elements $rs are the collection that is madeby removing the “head” element from the original collection. However, in thecase of sets, the rest elements are the same as the original collection because weignore the redundant elements. If we interpret a set as a collection that contains
inﬁnitely many copies of each element, this speciﬁcation of cons for sets is natural.
This speciﬁcation is useful, for example, when we pattern-match a graph as a setof edges and enumerate all paths with some ﬁxed length including cycles without
redundancy.
Polymorphic patterns are useful especially when we use value patterns. As
well as other patterns, the behavior of value patterns is dependent on matchers.
For example, equality [1, 2, 3] = [2, 1, 3] between collections is false if we regard them as mere lists but true if we regard them as multisets. Still, thanks
to the polymorphism of patterns, we can use the same syntax for both of them.
This greatly improves the readability of the program and makes programmingwith non-free data types easy.
matchAll [1, 2, 3] as list integer with
| #[2, 1, 3] -> "Matched"-- []matchAll [1, 2, 3] as multiset integer with
| #[2, 1, 3] -> "Matched"-- {"Matched"}

We can pass matchers to a function because matchers are ﬁrst-class objects.
It enables us to utilize polymorphic patterns for deﬁning function. The following
is an example utilizing polymorphism of value patterns.
def elem/m m x xs :=match xs as list m with
| _ ++ #x :: _ -> True
| _ -> False

2.3.4

Extensible Pattern Matching

In the proposed language, users can describe methods for interpreting patterns
in the deﬁnition of matchers. Matchers appeared up to here are deﬁned in our
language. We show an example of a matcher deﬁnition. We will explain thedetails of this deﬁnition in Section 2.5.1.
15

def unorderedPair m :=matcher| ($, $) as (m, m) with| ($x, $y) -> [(x, y), (y, x)]| $ as (eq) with| $tgt -> [tgt]An unordered pair is a pair ignoring the order of the elements. For example,
the tuple (2, 5) is equivalent to (5, 2), if we regard them as unordered pairs.
Therefore, the tuple (2, 5) is successfully pattern-matched with pattern (#5, $x).
matchAll (2, 5) as unorderedPair integer| (#5, $x) -> x-- [2]

We can deﬁne matchers for more complicated data types. For example, Egi constructed a matcher for mathematical expressions for building a computer algebra
system on our language [31, 32]. His computer algebra system is implemented
as an application of the proposed pattern-matching system. The matcher formathematical expressions is used for implementing simpliﬁcation algorithms ofmathematical expressions. A program that converts a mathematical expression
object n cos2 (θ) + n sin2 (θ) to n can be implemented as follows. (Here, we introduced the mathExpr matcher and some syntactic sugar for patterns.)
def simplifyCosAndSinInPoly poly :=match poly as mathExpr with$n * (#cos $x)^#2 * $y + #n * (#sin #x)^#2 * #y + r ->simplifyCosAndSinInPoly (n * y + r)
_ -> poly

2.4

Algorithm

This section explains the pattern-matching algorithm of the proposed system.
The formal deﬁnition of the algorithm is given in Section 2.6. The method fordeﬁning matchers explained in Section 2.5 is deeply related to the algorithm.
2.4.1

Execution Process of Non-linear Pattern Matching

Let us show what happens when the system evaluates the following patternmatching expression.
matchAll [2, 8, 2] as multiset integer with| $m :: #m :: _ -> m-- [2, 2]

Figure 2.1 shows one of the execution paths that reaches a matching result. First,
the initial matching state is generated (step 1). A matching state is a datum that
represents an intermediate state of pattern matching. A matching state is acompound type consisting of a stack of matching atoms, an environment, andintermediate results of the pattern matching. A matching atom is a tuple ofa pattern, a matcher, and an expression called target. MState denotes the data
constructor for matching states. env is the environment when the evaluationenters the matchAll expression. A stack of matching atoms contains a single
matching atom whose pattern, target, and matcher are the arguments of thematchAll expression.
In our proposal, pattern matching is implemented as a reduction of matchingstates. In a reduction step, the top matching atom in the stack of matching16

1

MState [($m :: #m :: _, multiset integer, [2, 8, 2])] env []2

MState [($m, integer, 2), (#m :: _, multiset integer, [8, 2])] env []MState [($m, integer, 8), (#m :: _, multiset integer, [2, 2])] env []MState [($m, integer, 2), (#m :: _, multiset integer, [2, 8])] env []3

MState [($m, something, 2), (#m :: _, multiset integer, [8, 2])] env []4

MState [(#m :: _, multiset integer, [8, 2])] env [(m, 2)]5

MState [(#m, integer, 8), (_, multiset integer, [2])] env [(m, 2)]MState [(#m, integer, 2), (_, multiset integer, [8])] env [(m, 2)]

6

MState [(_, multiset integer, [8])] env [(m, 2)]

7

MState [(_, something, [8])] env [(m, 2)]8

MState [] env [(m, 2)]

Figure 2.1: Reduction path of matching states
atoms is popped out. This matching atom is passed to the procedure called
matching function. The matching function is a function that takes a matching
atom and returns a list of lists of matching atoms. The behavior of the matching
function is controlled by the matcher of the argument matching atom. We cancontrol the behavior of the matching function by deﬁning matchers properly. For
example, we obtain the following results by passing the matching atom of theinitial matching state to the matching function.
matchFunction ($m :: #m :: _, multiset integer, [2, 8, 2]) =[ [($m, integer, 2), (#m :: _, multiset integer, [8, 2])][($m, integer, 8), (#m :: _, multiset integer, [2, 2])][($m, integer, 2), (#m :: _, multiset integer, [2, 8])] ]Each list of matching atoms is prepended to the stack of the matching atoms.
As a result, the number of matching states increases to three (step 2). Our
pattern-matching system repeats this step until all the matching states vanish.
For simplicity, in the following, we only examine the reduction of the ﬁrst
matching state in step 2. This matching state is reduced to the matching state
shown in step 3. The matcher in the top matching atom in the stack is changed
to something from integer, by deﬁnition of integer matcher. something is the only
built-in matcher of our pattern-matching system. something can handle only wildcards or pattern variables, and is used to bind a value to a pattern variable. This
matching state is then reduced to the matching state shown in step 4. The top
matching atom in the stack is popped out, and a new binding (m, 2) is added tothe collection of intermediate results. Only something can append a new binding
to the result of pattern matching.
Similarly to the preceding steps, the matching state is then reduced as shownin step 5, and the number of matching states increases to 2. #m is pattern-matchedwith 8 and 2 by integer matcher in the next step. When we pattern-match witha value pattern, the intermediate results of the pattern matching is used as anenvironment to evaluate it. In this way, “m” is evaluated to 2. Therefore, theﬁrst matching state fails to pattern-match and vanishes. The second matchingstate succeeds in pattern matching and is reduced to the matching state shown17

in step 6. In step 7, the matcher is simply converted from multiset integer tosomething, by deﬁnition of multiset integer. Finally, the matching state is reduced
to the empty collection (step 8). No new binding is added because the pattern
is a wildcard. When the stack of matching atoms is empty, reduction ﬁnishes
and the matching patching succeeds for this reduction path. The matching result(m, 2) is added to the entire result of pattern matching.
We can check the pattern matching for sequential triples and quadruples arealso eﬃciently executed in this algorithm.
2.4.2

Pattern Matching with Inﬁnitely Many Results

The proposed pattern-matching system can eventually enumerate all successful
matching results when matching results are inﬁnitely many. It is performed by
reducing the matching states in proper order. Suppose the following program:take 8 (matchAll nats as set integer with $m :: $n :: _ -> (m, n))-- [(1, 1), (1, 2), (2, 1), (1, 3), (2, 2), (3, 1), (1, 4), (2, 3)]

Figure 2.2 shows the search tree of matching states when the system executes
the above pattern-matching expression. Rectangles represent matching states,
and circles represent ﬁnal matching states of successful pattern matching. The
rectangle at the upper left is the initial matching state. The rectangles in thesecond row are the matching states generated from the initial matching state one
step. Circles o8, r9, and s9 correspond to pattern-matching results [(m, 1), (n,1)], [(m, 1), (n, 2)], and [(m, 2), (n, 1)], respectively.
One issue on naively searching this search tree is that we cannot enumerate
all matching states either in depth-ﬁrst or breadth-ﬁrst manners. The reason isthat the widths and depths of the search tree can be inﬁnite. Widths can beinﬁnite because a matching state may generate inﬁnitely many matching states(e.g., the width of the second row is inﬁnite), and depths can be inﬁnite when we
extend the language with a notion such as recursively deﬁned patterns.
To resolve this issue, we reshape the search tree into a reduction tree as presented in Figure 2.3. A node of a reduction tree is a list of matching states, and anode has at most two child nodes, left of which is the matching states generated
from the head matching state of the parent, and the right of which is a copy of
the tail part of the parent matching states. At each reduction step, the system
has a list of nodes. Each row in Figure 2.3 denotes such a list. One reduction
step in our system proceeds in the following two steps. First, for each node, it
generates a node from the head matching state. Then, it constructs the nodes forthe next step by collecting the generated nodes and the copies of the tail partsof the nodes. The index of each node denotes the depth in the tree the node ischecked at. Since widths of the tree are at most 2n for some n at any depth, allnodes can be assigned some ﬁnite number, which means all nodes in the tree are
eventually checked after a ﬁnite number of reduction steps.
We adopt breadth-ﬁrst search strategy as the default traverse method because there are cases that breadth-ﬁrst traverse can successfully enumerate all
pattern-matching results while depth-ﬁrst traverse fails to do so when we handle pattern matching with inﬁnitely many results. However, of course, when
the size of the reduction tree is ﬁnite, the space complexity for depth-ﬁrst traverse is less expensive. Furthermore, there are cases that the time complexity for
depth-ﬁrst traverse is also less expensive when we extract only the ﬁrst several
successful matches. Therefore, to extend the range of algorithms we can express
concisely with pattern matching keeping eﬃciency, providing users with a method18

Figure 2.2: Search tree

Figure 2.3: Binary reduction tree

for switching search strategy of reduction trees is important. We leave the further
investigation of this direction as interesting future work.

2.5

User-Deﬁned Matchers

This section explains how to deﬁne matchers from scratch through examples.
2.5.1

Matcher for Unordered Pairs

We explain how the unorderedPair matcher shown in Section 2.3.4 works. unorderedPairis deﬁned as a function that takes and returns a matcher to specify how topattern-match against the elements of a pair. A matcher is deﬁned using thematcher expression. The matcher expression is a built-in syntax of Egison. matcher
takes a collection of matcher clauses. A matcher clause is a triple of a primitivepattern pattern, a next-matcher expression, and a next-target expression.
A matcher is a kind of function that takes a pattern and target, and returns
lists of the next matching atoms. A matching atom is a triple of a pattern, target,
and matcher. A primitive-pattern pattern matches a pattern. Patterns thatmatch with pattern holes ($ inside primitive-pattern patterns) are next patterns.
A next-matcher expression returns the next matchers. A next-target expression
is a function that takes a target and returns a list of the next targets. A matcher
generates a list of the next matching atoms by combining the next patterns,
the next matchers, and a list of next targets. The formal syntax of the matcher
expression is found in Figure 2.4 in Section 2.6.
unorderedPair has two matcher clauses. The primitive-pattern pattern of theﬁrst matcher clause is ($, $). This matcher clause deﬁnes the interpretation of thetuple pattern. This pattern contains two pattern holes $. It means that it interprets the ﬁrst and second elements of the tuple pattern by the matchers speciﬁedby the next-matcher expression. In this example, since the next-matcher expression is (m, m), both of the elements of the tuple pattern are pattern-matched using the matcher given by m. The primitive-data-match clause of the ﬁrst matcher
clause is ($x, $y) -> [(x, y), (y, x)]. The pattern ($x, $y) is pattern-matchedwith the target datum such as (2, 5), and $x and $y is matched with 2 and5, respectively. The primitive-data-match clause returns [(2, 5), (5, 2)]. A
primitive-data-match clause returns a collection of next-targets. This means thepatterns “#5” and $x are matched with the targets 2 and 5, or 5 and 2 using the
integer matcher in the next step, respectively. Pattern matching of primitivedata-patterns is similar to pattern matching against algebraic data types in ordinary functional programming languages. As a result, the ﬁrst matcher clause19

works in the matching function as follows.
matchFunction [($x, $y) (unorderedPair integer) (2, 5)] =[ [($x, integer, 2), ($y, integer, 5)] [($x, integer, 5), ($y, integer, 2)] ]The second matcher clause is rather simple; this matcher clause simply converts the matcher of the matching atom to the something matcher.
2.5.2

Case Study: Matcher for Multisets

As an example of how we can implement matchers for user-deﬁned non-free datatypes, we show the deﬁnition of multiset matcher. We can deﬁne it simply byusing the list matcher. multiset is deﬁned as a function that takes and returns
a matcher.
def multiset a :=matcher| [] as () with| [] -> [()]
| _ -> []| $ :: _ as a with| $tgt -> tgt| $ :: $ as (a, multiset a) with| $tgt ->matchAll tgt as list a with| $hs ++ $x :: $ts -> (x, hs ++ ts)| #$val as () with| $tgt ->match (val, tgt) as (list a, multiset a) with| ([], []) -> [()]| ($x :: $xs, #x :: #xs) -> [()]
| (_, _) -> []| $ as (something) with| $tgt -> [tgt]The multiset matcher has ﬁve matcher clauses. The ﬁrst matcher clause handles a nil pattern, and it checks whether the target is an empty collection ornot. The second and third matcher clauses handle a cons pattern. The fourthmatcher clause handles a value pattern. This matcher clause deﬁnes the equalityof multisets. The ﬁfth matcher clause handles the other patterns for multiset: apattern variable and wildcard.
First, we focus on the third matcher clause. The primitive-pattern patternof the second matcher clause is $ :: $, and the next matcher expression is (a,multiset a). It means two arguments of the cons pattern are next patterns andthey are pattern-matched using the a and multiset a matchers, respectively. a
is an argument of multiset and the matcher for inner elements of a multiset.
In the next target expression, a simple join-cons pattern is used to decompose
a target collection into an element and the rest collection. For example, when
the target is a collection [1,2,3], this next-target expression returns [(1,[2,3]),(2,[1,3]),(3,[1,2])]. Each tuple of the next targets is pattern-matched using
the next patterns and the next matchers recursively. For example, 1 and [2,3]are pattern-matched using the a and multiset a matcher with the ﬁrst and thesecond argument of the cons pattern, respectively.
Next, we focus on the second matcher clause. The primitive-pattern patternof the second matcher clause is $ :: _. This matcher clause handles a cons pattern
whose second argument is a wildcard. We omit the calculation of the next target.
In this case, we omit the calculation of the rest elements. The next matcher of thismatcher clause is a and the next target is [1,2,3] when the target is a collection20[1,2,3]. We call the optimization technique that omits the calculation of the next

target when a pattern contains wildcard wildcard optimization.
Next, we focus on the fourth matcher clause. The primitive-pattern pattern of
this matcher clause is #$val. It is called a value-pattern pattern. A value-patternpattern matches a value pattern. This matcher clause compares the content of avalue pattern (val) and a target (tgt) as multisets. The match expression is used
for this comparison. The target collection tgt is recursively pattern-matched as
multiset a.
The ﬁrst and the third match clauses of this match expression are simple. The
ﬁrst match clause states that it returns [()] when both val and tgt are empty.
This return value means pattern matching for the value pattern succeeded. The
third match clause states that it returns [] if pattern matching for the patternsof both the ﬁrst and the second match clause failed. This return value means
pattern matching for the value pattern failed.
The second match clause is the most technical part of this match expression.
The value pattern #xs is recursively pattern-matched using this matcher clauseitself. The collection xs is one element shorter than tgt. Therefore, this recursion
ﬁnally reaches the ﬁrst or the third match clause if val and tgt are ﬁnite.
Finally, let us also explain the ﬁfth matcher clause. This matcher clausecreates the next matching atom by just changing the matcher from multiset a tosomething.
2.5.3

Matcher for Sorted Lists

Modularization of pattern-matching algorithms by matchers not by patterns enables polymorphic patterns. However, its merit extends beyond polymorphic
patterns; matchers enable descriptions of more eﬃcient pattern matching keeping patterns concise. The reason is that pattern matching against patterns insidematcher deﬁnitions allows us to describe more detailed pattern-matching algorithms. This section shows such an example, a matcher for sorted lists.
The program that used a doubly-nested join-cons pattern for enumerating
pairs of prime numbers whose forms are (p, p + 6) gets slower when the numberof the enumerating prime pairs gets larger. The reason is that the program
enumerates all the combinations of prime numbers. For example, the program
tries to match all the pairs such as (3, 5), (3, 7), (3, 11), (3, 13), (3, 17), (3, 19), andso on. However, we should avoid enumerating the pairs after (3, 11), the ﬁrst pairwhose diﬀerence is more than 6. This is because it is obvious that the diﬀerences
between all the pairs after (3, 11) are more than 6.
take 10 (matchAll primes as sortedList integer with
| _ ++ $p :: (_ ++ #(p + 6) :: _) -> (p, p + 6))-- [(5,11),(7,13),(11,17),(13,19),(17,23),(23,29),(31,37),(37,43),(41,47),(47,53)]

We can avoid this unnecessary search by creating a new matcher that is specialized for sorted lists. We can deﬁne such a matcher by adding a matcher clausewith the primitive-pattern pattern $ ++ #$px :: $ to the list matcher as shown
below. This matcher clause improves the theoretical time complexity of the above
pattern from O(n2 ) to O(n).
def sortedList a := matcher| $ ++ #$px :: $ as (sortedList a, sortedList a) with
| \$tgt -> matchAll tgt as list a with| loop $i (1, $n)((?(\x -> x < px) & $h_i) :: ...)

21

Expressions

ValuesM ::= c | x | (λ(x, · · · )M ) | (M M )V ::= c | (V, · · · ) | (C V · · · )| (M, · · · ) | (C M · · · )| (Γ, λ(x, · · · )M )| letrec [(x, M ), · · · ] in M

| (Γ, [ϕ, · · · ])| matchAll M as M with p -> M

Values in weak head normal form

| something | matcher [ϕ, · · · ]p ::=v ::= • | c | hΓ, M i| $x | #M | (C p · · · )| (v, · · · ) | (C v · · · )ϕ ::= (pp as M with [dp -> M, · · · ])pp ::=| hΓ, λ(x, · · · )M i

| $ | #$x | (C pp · · · )dp ::= $x | (C dp · · · )| hΓ, [ϕ, · · · ]i
EnvironmentsΓ ::= ∅ | {x 7→ v} | Γ ∪ ΓFigure 2.4: Syntax of our language(#px :: $ts)-> (map (\i -> h_i) [1..n], ts)...

We call this optimization technique for nested patterns pattern fusion. In theabove matcher clause, a loop pattern is used. We will explain loop patterns
in Section 3.2.6. Note that pattern fusion is only applicable to Egison thatmodularizes pattern-matching methods for each matcher, not for each pattern.
The reason is that we need to match patterns whose form is _ ++ #x :: _ asmentioned above. If pattern-matching methods are modularized for each pattern,
we need to introduce a new pattern constructor joinCons ... ... that is equivalent
to _ ++ ... :: ... for this purpose.

2.6

Formal Semantics

In this section, we present the syntax and big-step semantics of our language (Figure 2.4 and 2.5). We use metavariables x, y, z, . . ., M, N, . . ., V, W, . . ., v, w, . . .,and p, . . . for variables, expressions, values, values in weak head normal form,
and patterns respectively. A value is in weak head normal form when only theoutermost part has been evaluated, whereas a normal value is fully evaluated.
We handle values in weak head normal form for achieving lazy evaluation. In
Figure 2.4, c denotes a constant expression and C denotes a data constructorname. X · · · in Figure 2.4 means a ﬁnite list of X. The syntax of our language
is similar to that of the Haskell programming language. As explained in Section 2.3.1, (M, · · · ) and (C M · · · ) denote tuples and data constructions. In thisformal language, lists are represented as an algebraic data type using constructors. ϕ, pp, and dp are called matcher clauses, primitive-pattern patterns, andprimitive-data patterns respectively. Γ, ∆, . . . denote variable assignments, i.e.,
partial functions from variables to values. • denotes the dummy object and isused to implement the recursive deﬁnitions by the letrec expressions.
In Figure 2.5, the following notations are used. We write [ai ]i to mean alazy list whose elements are evaluated to [a1 , a2 , . . .]. Similarly, [[aij ]j ]i denotes[[a11 , a12 , . . .], [a21 , a22 , . . .], . . .], but each list in the list may have diﬀerent length.
List of tuples [(a1 , b1 ), (a2 , b2 ), . . .] may be often written as [ai , bi ]i instead of[(ai , bi )]i for short. Concatenation of lists l1 , l2 are denoted by l1 + l2 , and a : ldenotes [a] + l (adding at the front). ϵ denotes the empty list. In general, ⃗x forsome metavariable x is a metavariable denoting a list of what x denotes. However,22

Deep Evaluation:

Γ, M ↓ (h∆, Ni i)i

Γ, M ↓ h∆, [ϕ, · · · ]i

Γ, M ↓ h∆, λ(x, · · · )M i

Γ, M ↓ c
D-ConstantΓ, M ⇓ c

D-Lambda

Γ, M ⇓ (∆, λ(x, · · · )M )∆, Ni ⇓ Vi (∀i)Γ, M ↓ (C h∆, Ni i)i
D-TupleΓ, M ⇓ (Vi )i

Γ, M ⇓ (∆, [ϕ, · · · ])D-Matcher∆, Ni ⇓ Vi (∀i)
D-ConsΓ, M ⇓ (C Vi )i

Core features as a functional language:Γ, c ↓ c

VariableTuple
Γ ∪ {x 7→ v} ∪ ∆, x ↓ v
Γ, (Mi )i ↓ (hΓ, Mi i)iCons
LambdaΓ, (C Mi )i ↓ (C hΓ, Mi i)iΓ, (λ(xi )i M ) ↓ (Γ, λ(xi )i M )Constant

Γ, M ↓ (∆, λ(xi )i M ′ )∆ ∪ {xi 7→ vi }i , M ′ ↓ w

Γ, N ↓ (vi )i

Application

Γ, (M N ) ↓ w
Γ ∪ {xi 7→ •i }i , Mj ↓ h∆, Mj i∆′ = update(∆, [•i ]i , [vi ]i )(∀j)∆′ , N ↓ w
LetrecΓ, letrec [(xi , Mi )]i in N ↓ w
Evaluation of matcher and matchAll:
Γ, matcher [ppi as Mi with [dpij -> Nij ]j ]i ↓ hΓ, [ppi , Mi , [dpij , Nij ]j ]⟩Γ, M ↓ v

Γ, N ↓ m[[[p ∼m v], Γ, ∅]] ⇛ [∆i ]iΓ ∪ ∆ i , L ↓ vi

Matcher(∀i)
MatchAllΓ, matchAll M as N with p -> L ↓ [vi ]i
Matching states:⃗⃗⃗⃗⃗s ⇒ ⃗Γ, s⃗′s⃗′ ⇛ ∆
MS-Bfs-Cons⃗s ⇛ ⃗⃗⃗
Γ+∆MS-Bfs-Nilϵ⇛ϵ⃗si → opt Γi , opt s⃗′ i , opt s⃗′′ i (∀i)
MS-Step∑∑∑[⃗si ]i ⇒ i (opt Γi ), i (opt s⃗′ i ) + i (opt s⃗′′ i )ϵ → none, none, none MS-Fail(ϵ, Γ, ∆) : ⃗s → (some ∆), none, (some ⃗s)p ∼Γ∪∆v ↓ [⃗ai ]i , ∆′m

MS-Top-MAtom((p ∼m v) : ⃗a, Γ, ∆) : ⃗s → none, (some[⃗ai + ⃗a, Γ, ∆ ∪ ∆′ ]i ), (some ⃗s)
Matching atoms:∼Γ
something v ↓ [ϵ], ∅MA-Something-WC$x ∼Γ
something v ↓ [ϵ], {x 7→ v}

pp ≈Γ p ↓ fail

p ∼Γ⃗

(ϕ,∆)

v ↓ ⃗a, Γ⃗((pp,M,⃗σ ):ϕ,∆)

pp ≈Γ p ↓ [p′i ]i , ∆′dp ≈ v ↓ fail

MA-PP-Fail

′

p ∼Γ

⃗
((pp,M,⃗σ ):ϕ,∆)⃗p ∼Γ

v ↓ ⃗a, Γ⃗((pp,M,(dp,N ):⃗σ ):ϕ,∆)

pp ≈Γ p ↓ [p′j ]j , ∆′dp ≈ v ↓ ∆′′MA-Something-PatVarv ↓⃗⃗a, Γ′⃗p ∼Γ

MS-Successv ↓⃗⃗a, Γ′
MA-DP-Fail

′

′ ] ]
∆ ∪ ∆′ ∪ ∆′′ , N ↓ [[vijj i∆, M ↓ [m′j ]jMA-Step′ ] ] ,∅v ↓ [[p′j ∼m′ vijj i⃗j((pp,M,(dp,N ):⃗σ ):ϕ,∆)p ∼Γ

Pattern matching on patterns:
Γ, M ↓ v≈Γ p ↓ [], ∅PPP-WC$ ≈Γ p ↓ [p], ∅PPP-PatHole

ppi ≈Γ pi ↓ p⃗i , Γi(∀i)∑(C pp1 . . . ppn ) ≈Γ (C p1 . . . pn ) ↓

⃗i ,
ip

∪

#$y ≈Γ #M ↓ ϵ, {y 7→ v}i Γi

PPP-ValPat

PPP-Constructor

Pattern matching on data:dpi ≈ vi ↓ Γi$z ≈ v ↓ {z 7→ v}

PDP-PatVar(∀i)(C dp1 . . . dpn ) ≈ (C v1 . . . vn ) ↓

∪

i Γi

Figure 2.5: Formal semantics of our language

23

PDP-Constructor

we do not mean by ⃗xi the i-th element of ⃗x; if we write [⃗xi ]i , we mean a list of alist of x.
Our language has some special primitive types: matching atoms a, . . ., matching states s, . . ., primitive-data-match clauses σ, . . ., and matchers m, . . .. A
matching atom consists of a pattern p, a matcher m, and a value v, and written asp ∼m v. A matching state is a tuple of a list of matching atoms and two variableassignments. A primitive-data-match clause is a tuple of a primitive-data pattern
and an expression, and a matcher clause is a tuple of a primitive-pattern pattern,
an expression, and a list of data-pattern clauses. A matcher is a pair containing alist of matcher clauses and a variable assignment. Note that matchers, matchingstates, etc. are all values.
The ﬁrst part of Figure 2.5 deﬁnes the semantics for evaluating values in weakhead normal form to the full-evaluated values. The judgment Γ, M ↓ v denotesthat the given expression M is evaluated to v, which is a value in weak headnormal form, under the environment Γ. The judgment Γ, M ⇓ V denotes that
M is evaluated to the full-evaluated value v under Γ. In the evaluation rules
D-Tuple and D-Cons, we can see that the subexpressions inside tuples andconstructor data are deeply evaluated using the judgment ∆, Ni ⇓ Vi recursively.
The second part of Figure 2.5 deﬁnes the semantics of the basic featuresof functional languages. The semantics for all the expressions in this part aredeﬁned in the common method. The ﬁrst judgment in the assumption of Letrec
evaluates each expression in bindings after assigning the variables in letrec todummy values. Then, the second judgment in the assumption of Letrec updates
the dummy values with these evaluated values. The function update(∆, [vi ]i , [wi ]i )returns the new environment ∆0 by updating the values that are stored at thepositions where each vi is located with wi .
In the ﬁgure, MatchAll and Matcher show the deﬁnition of evaluation ofmatcher and matchAll expressions, respectively. Evaluation results of expressions
are speciﬁed by the judgment Γ, e ↓ ⃗v , which denotes given a variable assignment
Γ and an expression e one gets a list of values ⃗v . The deﬁnition of matchAll relies
on another type of the judgment ⃗⃗s ⇛ ⃗Γ, which deﬁnes how the search space is
examined.
The rules that start with MS- in the second part of Figure 2.5 show thedeﬁnition of the judgment ⃗⃗s ⇛ ⃗Γ. The judgment ⃗⃗s ⇛ ⃗Γ takes a list of lists ofmatching states and returns pattern-match results. We handle a list of lists ofmatching states for traversing a search tree in breadth-ﬁrst order as explained in
Section 2.4.2. This list of lists of matching states represents the list of nodes at thesame depth level in the binary reduction tree in Figure 2.3. For example, ⃗⃗s is [[a1]]at the ﬁrst depth level, [[b2, c3, d4, · · · ]] at the second level, and [[e3], [c3, d4, · · · ]]at the third depth level in the binary reduction tree in Figure 2.3. MS-BfsNil and MS-Bfs-Cons deﬁne this breadth-ﬁrst search. In MS-Bfs-Cons, ⇛ is⃗inductively deﬁned using ⃗⃗s ⇒ ⃗Γ, s⃗0 , which is deﬁned by MS-Step. The judgment⃗0 takes a list of lists of matching states in the same depth level and⃗⃗s ⇒ ⃗Γ, s⃗returns the list of nodes in the next depth level. ⃗Γ represents the pattern-match⃗
results, and s⃗0 represents the list of nodes in the next depth level. For example,⃗
in the binary reduction tree in Figure 2.3, when ⃗⃗s is [[e3], [c3, d4, · · · ]], Γ and s⃗0are ∅ and [[f 4], [g4], [d4, · · · ]], respectively. MS-Fail, MS-Success, and MSTop-MAtom deﬁne the evaluation of the judgment ⃗s → opt Γ, opt s⃗0 , opt s⃗00 .
In these rules, we introduce notations for (meta-level) option types. none andsome x are the constructors of the option type, and opt x is a metavariable for an24

∑
optional value (possibly) containing what the metavariable x denotes. i (opt xi )creates a list by collecting all the valid (non-none) xi preserving the order. In
the judgment ⃗s → opt Γ, opt s⃗0 , opt s⃗00 , opt Γ represents a pattern-match result,opt s⃗0 represents next matching states, and opt s⃗00 represents the rest of matchingstates. This judgment takes a list of matching states (a node of the binary
reduction tree) and returns the next matching states. MS-Fail deﬁnes thatpattern matching fails when the next matching states of the previous matchingstate is empty. MS-Success deﬁnes that pattern matching succeeds when thestack of matching atoms becomes empty. MS-Top-MAtom expands the top
matching atom of the ﬁrst matching state by the method deﬁned in the matcherof the top matching atom.
The rules that start with MA- in the third part of Figure 2.5 show the deﬁnition of evaluation of a matching atom. The judgment p ∼Γm v ↓ ⃗⃗a, ∆ is a 6-ary
relation. One reads this judgment “performing pattern matching on v against p
using the matcher m under the variable assignment Γ yields the next matchingatoms ⃗⃗a and the variable assignment ∆.” ⃗⃗a being empty means the pattern matching failed. If [ϵ] is returned as ⃗⃗a, it means the pattern matching succeeded and nofurther search is necessary. These rules deﬁne the matching function explained in
Section 2.4.1. MA-Something-WC and MA-Something-PatVar deﬁne thepattern-match method for the only built-in matcher something. The something
matcher can handle only a wildcard or a pattern variable and always succeeds inpattern matching. When the pattern is a pattern variable, a new assignment is
added. MA-PP-Fail, MA-DP-Fail, MA-Step handle a user-deﬁned matcher.
As explained in Section 2.5, one needs to pattern-match patterns and data todeﬁne user-deﬁned matchers. Their formal deﬁnitions are given by judgments
pp ≈Γ p ↓ p⃗0 , ∆ and dp ≈ v ↓ Γ that are deﬁned in the fourth part and the lastpart of Figure 2.5. MA-PP-Fail deﬁnes that we try the next matcher clauses
when pattern matching for primitive-pattern pattern fails. MA-DP-Fail deﬁnesthat we try the next primitive-data-match clauses when pattern matching for
primitive-data pattern fails. MA-Step deﬁnes that we get the next matchingatoms by executing the body of the primitive-data match clause where patternmatching for the primitive-pattern pattern and the primitive-data pattern succeeds.
The rules that start with PPP- in the fourth part of Figure 2.5 show the definition of pattern matching for primitive-pattern patterns. One reads the judgment pp ≈Γ p ↓ p⃗0 , ∆ “performing pattern matching on the pattern p against theprimitive-pattern pattern pp under the environment Γ yields the next patternsp⃗0 and the variable assignment ∆”. PPP-WC, PPP-PatHole, PPP-ValPat,
and PPP-Constructor deﬁne primitive-pattern-match for a wildcard, a pattern hole, a primitive value pattern, a constructor pattern, respectively.
The rules that start with PDP- in the last part of Figure 2.5 show the deﬁnition of pattern matching for primitive-data patterns. One reads the judgment
dp ≈ v ↓ Γ “performing pattern matching on v against the primitive-data pattern
dp yields the variable assignment Γ”. PDP-PatVar and PDP-Constructor
deﬁne primitive-data-match for a pattern variable and a constructor pattern,
respectively.

2.7

Related WorkWhen pattern matching ﬁrst appeared, pattern matching could only be applied tothe speciﬁc types of algebraic data types [24]. Huge eﬀorts have been conducted
to remove this limitation [48, 25]. As a result, state-of-the-art work allows us
25

pattern matching for non-free data types. This section reviews this evolution byseeing what happened in each decade.
2.7.1

1980s: Spread of Pattern Matching and Invention of Views

From this decade, functional languages with user-deﬁned algebraic data types
and pattern matching for them became common. Miranda by Turner [90] andHaskell [48] were the most popular among these languages, and the ﬁrst patternmatch extensions for widening the target of pattern matching beyond algebraic
data types were designed on them.
Miranda’s laws [84, 85] and Wadler’s views [92, 65] are earlier such research.
They discarded the assumption that one-to-one correspondence should exist between patterns and data constructors. They enable pattern matching for datatypes whose data have multiple representation forms. For example, Wadler’s
paper on views [92] presents pattern matching for complex numbers that have
two diﬀerent representation forms: Cartesian and polar. However, their expressiveness is not enough for representing patterns for non-free data types. They
support neither non-linear patterns nor pattern matching with multiple results.
Views are supported as a GHC extension in Haskell [5]. Views are implemented
also in Racket [86].
At the same time, more expressive pattern matching is explored by Queinnec [70], who proposed expressive pattern matching for lists. Though this proposal is specialized to lists and not extensible, the proposed language supports
the cons and the join patterns, non-linear pattern matching with backtracking,matchAll, not-patterns, and recursive patterns. His proposal achieves almost perfect expressiveness for patterns of lists and allows the pattern-match-oriented
deﬁnition of the basic list processing functions. For example, the following member
deﬁnition is presented in Queinnec’s paper [70].
member ?x (??- ?x ??-) -> true
member ?x ?-> false

In Queinnec’s language, we represent a wildcard by -. Pattern variables areprepended by ? or ??. A pattern variable that starts with ?? appears only in alist pattern. This pattern variable matches a part of the target list.
2.7.2

1990s and 2000s: Exploration for Expressive Patterns

Following the pattern-match extensions in the previous decade, several new patternmatch extensions for extending the target range of pattern matching have been
proposed by several researchers. We review these proposals in this section.
Erwig’s active patterns [39, 80] are an attempt to extend the expressiveness ofpatterns beyond Wadler’s views. Active patterns also allow users to customize thepattern-matching algorithm for each pattern. An example of pattern matching
against graphs using matching function is also shown in [40]. Add' in the following
program is a pattern constructor of active patterns. Add' extracts an element that
is identical with the ﬁrst argument of Add' from the target collection.
pat Add' (x,_) = Add (y,s) => if x == y then Add (y,s) else let Add' (x,t) = s in
Add (x, Add (y, t)) end

Using the above Add', we can deﬁne the member function hiding the recursion as
follows.
fun member x (Add' (x,s)) = true| member x s = false

26However, the expressiveness of active patterns is still limited. Active patterns
do not support pattern matching with multiple results: Add' can take only a value
and cannot take a pattern variable as its ﬁrst argument. Non-linear patterns
exhibit their full ability when they are combined with pattern matching withbacktracking.
Tullsen’s ﬁrst-class patterns [89] are another extension of views. First-classpatterns support pattern matching with multiple results. In ﬁrst-class patterns,
we can deﬁne pattern constructors that have multiple decompositions. However,
the expressiveness of ﬁrst-class patterns is still limited because it does not support non-linear patterns. Non-linear pattern matching is a necessary feature fordescribing useful patterns for non-free data types.
2.7.3

2010s: Toward a Uniﬁed Theory of Pattern-Match-Oriented
Programming

In this decade, a uniﬁed theory for practical pattern matching for non-free datatypes has been pursued. Egison proposed in this thesis is such research. The
research listed and organized the properties for practical pattern matching fornon-free data types. We proposed three criteria. The criteria are as follows:(1) Eﬃciency of the backtracking algorithm for non-linear patterns; (2) Ad-hoc
polymorphism of patterns; (3) Extensibility of pattern matching.

2.8

Conclusion

We designed a user-customizable eﬃcient non-linear pattern-matching system byregarding pattern matching as reduction of matching states that have a stackof matching atoms and intermediate results of pattern matching. This systemenables us to concisely describe a wide range of programs, especially when nonfree data types are involved. For example, our pattern matching architecture isuseful to implement a computer algebra system because it enables us to directly
pattern-match mathematical expressions and rewrite them.
The major signiﬁcance of our pattern matching system is that it greatly improves the expressivity of the programming language by allowing programmers
to freely extend the process of pattern matching by themselves. Although we
consider that the current syntax of matcher deﬁnition is already clean enough,we leave further reﬁnement of the syntax of our surface language as future work.
We believe the direct and concise representation of algorithms enables us to
implement really new things that go beyond what was considered practical before.
We hope our work will lead to breakthroughs in various ﬁelds. ,27

Chapter 3
Pattern-Matching-Oriented Programming
Style
3.1

Overview

Throughout the history of functional programming, recursion has emerged as anatural method for describing loops in programs. However, there does often exist
a substantial cognitive distance between the recursive deﬁnition and the simplest
explanation of an algorithm even for the basic list processing functions such asmap, concat, or unique; when we explain these functions, we seldom use recursion
explicitly as we do in functional programming. For example, map is often explained
as follows: the map function takes a function and a list and returns a list of theresults of applying the function to all the elements of the list.
In this chapter, we advocate a new programming paradigm called patternmatch-oriented programming for ﬁlling this gap. An essential ingredient of our
method is utilizing pattern matching for non-free data types. Pattern matchingfor non-free data types features non-linear pattern matching with backtracking
and extensibility of pattern-matching algorithms. Several non-standard patternconstructs, such as not-patterns, loop patterns, and sequential patterns, are derived from this pattern-matching facility. Based on that result, we introduce
many programming techniques that replace explicit recursions with an intuitive
pattern by conﬁning recursions inside patterns. We classify these techniques as
pattern-match-oriented programming design patterns.
These programming techniques allow us to redeﬁne not only the most basic
functions for list processing such as map, concat, or unique more elegantly than the
traditional functional programming style, but also more practical mathematicalalgorithms and software such as a SAT solver, computer algebra system, anddatabase query language that we had not been able to implement concisely.
This chapter is organized as follows. Section 3.2 introduces Egison and various pattern constructs for non-free data types. These pattern constructs increase
the number of situations in which we can replace verbose recursions with more intuitive patterns. Section 3.3 catalogs pattern-match-oriented programming techniques utilizing the features introduced in Section 3.2. Section 3.4 explores theeﬀect of pattern-match-oriented programming in more practical situations. Section 3.5 reviews the related work. Finally, Section 3.6 concludes this chapter.

3.2

Quick Tour of the Egison Pattern-Match-Oriented Language

This section quickly introduces the pattern-matching facility of Egison.

28

3.2.1

Value Patterns and Predicate Patterns for Representing Nonlinear Patterns

matchAll gets even more powerful when combined with non-linear patterns. For

example, the following non-linear pattern matches when the target collection
contains a pair of identical elements.
matchAll [1, 2, 3, 2, 4, 3] as list integer with
| _ ++ $x :: _ ++ #x :: _ -> x-- [2, 3]

Value patterns play an important role in representing non-linear patterns.
A value pattern matches the target if the target is equal to the content of thevalue pattern. A value pattern is prepended with # and the expression after # isevaluated referring to the value bound to the pattern variables that appear on
the left side of the patterns. As a result, for example, $x :: #x :: _ is valid, but#x :: $x :: _ is invalid.
The variables inside a value pattern refer to a value bound outside the patternmatch expression when the corresponding pattern variables do not appear on theleft-side of a pattern. For example, the value pattern #x refers to the value boundby the ﬁrst argument of delete in the following sample.
def delete x xs :=match xs as list eq with| $hs ++ #x :: $ts -> hs ++ ts| _ -> xs
delete 2 [1, 2, 3, 4]-- [1, 3, 4]

Let us show pattern matching for twin primes as a sample of non-linear patterns. Twin primes are pairs of prime numbers whose forms are (p, p + 2). primes
is an inﬁnite list of prime numbers. This matchAll extracts all twin primes fromthis inﬁnite list of prime numbers in order.
def twinPrimes := matchAll primes as list integer with
| _ ++ $p :: #(p + 2) :: _ -> (p, p + 2)
take 8 twinPrimes-- [(3, 5), (5, 7), (11, 13), (17, 19), (29, 31), (41, 43), (59, 61), (71, 73)]

There are cases that we might want to use more general predicates in patterns
than equality. Predicate patterns are provided for such a purpose. A predicate
pattern matches the target if the predicate returns true for the target. A predicate
pattern is prepended with ?, and a predicate of one argument follows after ?.
def twinPrimes := matchAll primes as list integer with
| _ ++ $p :: ?(\q -> q = p + 2) :: _ -> (p, p + 2)

3.2.2

Non-linear Pattern Matching with Backtracking

The pattern-matching algorithm inside Egison includes the backtracking mechanism for eﬃcient non-linear pattern matching.
matchAll [1..n] as list integer with _ ++ $x :: _ ++ #x :: _ -> x-- returns [] in O(n^2) time
matchAll [1..n] as list integer with _ ++ $x :: _ ++ #x :: _ ++ #x :: _ -> x-- returns [] in O(n^2) time29

The above expressions match a collection that consists of integers from 1 ton as a list of integers for enumerating identical pairs and triples, respectively.
This target collection contains neither identical pairs nor triples. Therefore both
expressions return an empty collection.
When evaluating the second expression, Egison interpreter does not try pattern matching for the second #x because pattern matching for the ﬁrst #x always
fails. Therefore, the time complexities of the above expressions are identical. The
pattern-matching algorithm inside Egison is discussed in Section 2.4 in detail.
3.2.3

Ad-hoc Polymorphism of Patterns by Matchers

Another merit of matchers, in addition to the extensibility of pattern-matchingalgorithms, is the ad-hoc polymorphism of patterns. The ad-hoc polymorphismof patterns is important for non-free data types because some data are patternmatched as various non-free data types at the diﬀerent parts of a program. For
example, a collection is pattern-matched as a list, a multiset, and a set. Polymorphic patterns reduce the number of names for pattern constructors.
In the following sample, a list [1,2,3] is pattern-matched using diﬀerent
matchers with the same cons pattern. In the case of multisets, the cons pattern decomposes a collection into an element and the rest elements ignoring theorder of the elements. In the case of sets, the rest elements are the same as
the original collection because we ignore the redundant elements. If we regard
a set as a collection that contains inﬁnitely many copies of each element, thisspeciﬁcation of the cons pattern for sets is natural.
matchAll [1,2,3] as list something with $x :: $xs -> (x,xs)-- [(1,[2,3])]matchAll [1,2,3] as multiset something with $x :: $xs -> (x,xs)-- [(1,[2,3]),(2,[1,3]),(3,[1,2])]
matchAll [1,2,3] as set something with $x :: $xs -> (x,xs)-- [(1,[1,2,3]),(2,[1,2,3]),(3,[1,2,3])]Polymorphic patterns are useful especially for value patterns. As well as otherpatterns, the behavior of value patterns is dependent on matchers. For example,
an equality [1,2,3] == [2,1,3] between collections is false if we regard them as lists
but true if we regard them as multisets. Still, thanks to ad-hoc polymorphism ofpatterns, we can use the same syntax for both types. This dramatically improves
the readability of the program and makes programming with non-free data types
easy.
matchAll [1,2,3] as list integer with #[2,1,3] -> "Matched" -- []matchAll [1,2,3] as multiset integer with #[2,1,3] -> "Matched" -- ["Matched"]

3.2.4

matchAllDFS for Controlling the Order of Pattern-Matching Pro-cess
The matchAll expression is designed to enumerate all countably inﬁnite patternmatching results. For this purpose, users sometimes need to care about the orderof pattern-matching results.
Let us start by showing a representative sample. The matchAll expression
below enumerates all pairs of natural numbers. We extract the ﬁrst 8 elementswith the take function. matchAll traverses the reduction tree of pattern matchingin breadth-ﬁrst search to traverse all the nodes (Section 5.2 of [38]). As a result,the order of the pattern-matching results is as follows.

30

take 8 (matchAll [1..] as set something with
| $x :: $y :: _ -> (x,y))-- [(1,1),(1,2),(2,1),(1,3),(2,2),(3,1),(2,3),(3,2)]

The above order is preferable for traversing an inﬁnitely large reduction tree.
However, sometimes, this order is not preferable (see Section 3.3.1.2 and Section 3.3.4.1). matchAllDFS that traverses a reduction tree in depth-ﬁrst order isprovided for this reason.
take 8 (matchAllDFS [1..] as set something with
| $x :: $y :: _ -> (x,y))-- [(1,1),(1,2),(1,3),(1,4),(1,5),(1,6),(1,7),(1,8)]

3.2.5

Logical Pattern Constructs: And-Patterns, Or-Patterns, and
Not-Patterns

The situations where and-patterns and or-patterns are useful are similar to thoseof the existing languages, whereas not-patterns become useful when they are
combined with non-linear pattern matching with backtracking.
We start by showing pattern matching for prime triples as an example ofand-patterns and or-patterns. A prime triple is a triple of primes whose form is(p, p + 2, p + 6) or (p, p + 4, p + 6). The and-pattern is used as an as-pattern. The
or-pattern is used to match both of p + 2 and p + 4.
def primeTriples := matchAll primes as list integer with
| _ ++ $p :: ((#(p + 2) | #(p + 4)) & $m) :: #(p + 6) :: _-> (p, m, p + 6)
take 6 primeTriples -- [(5,7,11),(7,11,13),(11,13,17),(13,17,19),(17,19,23),(37,41,43)]

A not-pattern matches a target if the pattern does not match the target, as
its name implies. A not-pattern is prepended with !, and a pattern follows after!. The following matchAll enumerates sequential pairs of prime numbers that are
not twin primes.
take 10 (matchAll primes as list integer with
| _ ++ $p :: (!#(p + 2) & $q) :: _ -> (p, q))-- [(2,3),(7,11),(13,17),(19,23),(23,29),(31,37),(37,41),(43,47),(47,53),(53,59)]

3.2.6

Loop Patterns for Representing Repetition

A loop pattern is a pattern construct for representing a pattern that repeats
multiple times. It is an extension of Kleene star operator of regular expressions
for general non-free data types [33].
Let us start by considering pattern matching for enumerating all combinationsof two elements from a target collection. It can be written using matchAll as
follows.
def comb2 xs := matchAll xs as list something with
| _ ++ $x_1 :: _ ++ $x_2 :: _ -> [x_1, x_2]
comb2 [1,2,3,4] -- [[1,2],[1,3],[2,3],[1,4],[2,4],[3,4]]

Egison allows users to append indices to a pattern variable as $x_1 and $x_2
in the above sample. They are called indexed variables and represent x1 andx2 in mathematical expressions. The expression after _ must be evaluated to an
31integer and is called an index. We can append as many indices as we want like
x_i_j_k. When a value is bound to an indexed pattern variable $x_i, the system
initiates an abstract map consisting of key-value pairs if x is not bound to a map,and bind it to x. If x is already bound to a map, a new key-value pair is added
to this map.
Now, we generalize comb2. The loop patterns can be used for that purpose.
def comb n xs := matchAll xs as list something with| loop $i-- index variable(1, n)-- index range(_ ++ $x_i :: ...) -- repeat pattern_-- final pattern-> map (\i -> x_i) [1..n]comb 2 [1,2,3,4] -- [[1,2],[1,3],[2,3],[1,4],[2,4],[3,4]]
comb 3 [1,2,3,4] -- [[1,2,3],[1,2,4],[1,3,4],[2,3,4]]

The loop pattern takes an index variable, index range, repeat pattern, and ﬁnal
pattern as arguments. An index variable is a variable to hold the current repeat
count. An index range speciﬁes the range where the index variable moves. An
index range is a tuple of an initial number and ﬁnal number. A repeat pattern
is a pattern repeated when the index variable is in the index range. A ﬁnal
pattern is a pattern expanded when the index variable gets out of the index
range. Inside loop patterns, we can use the ellipsis pattern (...). The repeat
pattern or the ﬁnal pattern is expanded at the location of the ellipsis pattern.
The repeat pattern is expanded replacing the ellipsis pattern incrementing thevalue of the index variable. For example, when n = 3, the above loop pattern is
expanded as follows.
loop $i (1, 3) (_ ++ $x_i :: ...) _ -->_ ++ $x_1 :: (loop $i (2, 3) (_ ++ $x_i :: ...) _) -->_ ++ $x_1 :: _ ++ $x_2 :: (loop $i (3, 3) (_ ++ $x_i :: ...) _) -->_ ++ $x_1 :: _ ++ $x_2 :: _ ++ $x_3 :: (loop $i (4, 3) (_ ++ $x_i :: ...) _) -->_ ++ $x_1 :: _ ++ $x_2 :: _ ++ $x_3 :: _The repeat counts of the loop patterns in the above samples are constants.
However, we can also write a loop pattern whose repeat count varies dependingon the target by specifying a pattern instead of an integer as the ﬁnal number.
When the ﬁnal number is a pattern, the ellipsis pattern is replaced with both
the repeat pattern and the ﬁnal pattern, and the repeat count when the ellipsis
pattern is replaced with the ﬁnal pattern is pattern-matched with that pattern.
The following loop pattern enumerates all initial preﬁxes of the target collection.
matchAll [1,2,3,4] as list something with| loop $i (1, $n) ($x_i :: ...) _ -> map (\i -> x_i) [1..n]-- [[],[1],[1,2],[1,2,3],[1,2,3,4]]

Loop patterns are heavily used especially for trees and graphs. We work on
pattern matching for trees in Section 3.3.4.1. More formal speciﬁcation of syntax
and semantics of loop patterns is shown in the author’s previous paper [33].
3.2.7

Sequential Patterns for Controlling the Order of Pattern-Matching
Process

The pattern-matching system of Egison processes patterns from left to right inorder. However, there are cases where we want to change this order, for example,
to refer to the value bound to the right side of a pattern. Sequential patterns areprovided for such a purpose.
32Sequential patterns allow users to control the order of the pattern-matchingprocess. A sequential pattern is represented as a list of patterns. Pattern matching is executed for each pattern in order. In the following sample, the target list
is pattern-matched from the third, ﬁrst, and the second element in order.
matchAll [2,3,1,4,5] as list integer with
| {
@
::
@
:: $x :: _,(#(x + 1),@),#(x + 2)}-> "Matched" -- ["Matched"]@ that appears in a sequential pattern is called later pattern variable. The target

data bound to later pattern variables are pattern-matched in the next sequence.
When multiple later pattern variables appear, they are pattern-matched as atuple in the next sequence. It allows us to apply not-patterns for diﬀerent partsof a pattern at the same time as we will see in Section 3.3.3.
Some readers might wonder that a sequential pattern can be transformed intoa nested matchAll expression. There are at least two reasons why it is impossible.
First, a nested matchAll expression breaks breadth-ﬁrst search strategy: the innermatchAll for the second result of the outer matchAll is executed only after the innermatchAll for the ﬁrst result of the outer matchAll is ﬁnished. Second, a later patternvariable retains the information of not only a target but also a matcher. Thereare cases that the matcher of matchAll is a parameter passed as an argument of afunction, and a pattern is polymorphic. Therefore, it is impossible to determine
the matchers of inner matchAll expressions syntactically.
3.2.8

Matcher Compositions

Matchers are composable. We can deﬁne matchers for such as tuples of multisetsand multisets of multisets. Using this feature, we can deﬁne matchers for various
data types.
First, we can deﬁne a matcher for tuples by a tuple of matchers. A tuple
pattern is used for pattern matching using such a matcher. For example, we candeﬁne the intersect function using a matcher for tuples of two multisets. We
work on pattern matching for tuples of collections more in Section 3.3.3.
def intersect xs ys := matchAll (xs,ys) as (set eq, set eq) with| ($x :: _, #x :: _) -> x
eq is a user-deﬁned matcher for data types for which equality is deﬁned. Whenthe eq matcher is used, equality is checked for a value pattern.∗
By passing a tuple matcher to a function that takes and returns a matcher,we can deﬁne a matcher for various non-free data types. For example, we candeﬁne a matcher for a graph as a set of edges. In the following code, we assume
a node id is represented by an integer.
def graph := multiset (integer, integer)

A matcher for adjacency graphs also can be deﬁned. An adjacency graph isdeﬁned as a multiset of tuples of an integer and a multiset of integers.
def adjacencyGraph := multiset (integer, multiset integer)

Some readers might wonder about matchers for algebraic data types. Egison provides a special syntactic construct for deﬁning a matcher for an algebraic data type. For example, a matcher for binary trees can be deﬁned using
algebraicDataMatcher.
∗

A deﬁnition of the eq matcher is explained in Section 6.3 of [38].

33def binaryTree a := algebraicDataMatcher| bLeaf a| bNode a (binaryTree a) (binaryTree a)Matchers for algebraic data types and matchers for non-free data types also
can be combined. For example, we can deﬁne a matcher for trees whose nodes
have an arbitrary number of children whose order is ignorable. We show patternmatching for these trees in Section 3.3.4.1.
def tree a := algebraicDataMatcher| leaf a| node a (multiset (tree a))

3.3

Pattern-Match-Oriented Programming Design Patterns

This section introduces basic pattern-match-oriented programming techniquesthat replace explicit recursions with intuitive patterns. In the ﬁrst part of thissection, we rewrite many list processing functions such as map, filter, elem, delete, any, every, unique, concat, and difference, for which we expect most functional
programmers imagine the same deﬁnitions. In the latter part of this section, wemove our focus to descriptions of more mathematical algorithms that are notwell supported in the current functional programming languages. We proceedwith this section by listing patterns that frequently appear showing situations inwhich they are useful. The following table shows this list.

Name

Description

Explained and Used inJoin-cons pattern for list

Enumerate combinations of elements.

Cons pattern for multiset

Enumerate permutations of elements.

Tuple pattern for collections
Loop patternCompare multiple collections.
Describe repetitions inside patterns.

3.3.1
3.3.2, 3.3.3, 3.3.4,
3.4.1, 3.4.3, 3.4.4
3.3.3, 3.3.4, 3.4.1, 3.4.4
3.3.4

3.3.1

Join-Cons Patterns for Lists — List Basic Functions

Join patterns whose second argument is a cons pattern, such as _ ++ $x :: _, arefrequently used for lists. We call these patterns join-cons patterns. Many basic
list processing functions can be redeﬁned by simply using this pattern.
3.3.1.1

Single Join-Cons Patterns — The map Function and Its Family_ ++ $x :: _ matches each element of the target collection when the list matcher

is used. As a result, the matchAll expression below matches each element of xs, andreturns the results of applying f to each of them. As discussed in Introduction,
this map deﬁnition is very close to our natural explanation of map.
def map f xs := matchAll xs as list something with
| _ ++ $x :: _ -> f x

By modifying the above matchAll expression, we can deﬁne several functions.
For example, we can deﬁne filter by inserting a predicate pattern.
def filter pred xs := matchAll xs as list something with
| _ ++ (and ?pred $x) :: _ -> x

34

We can deﬁne elem by using a value pattern. elem is a predicate that determines
whether the ﬁrst argument element appears in the second argument list or not.
match is provided also in Egison. match is just an alias of head (matchAll ...)
because Egison evaluates matchAll lazily.∗def elem x xs := match xs as list eq with
| _ ++ #x :: _ -> True
| _-> False

We can deﬁne delete that removes the ﬁrst appearance of x from xs by modifying
elem.
def delete x xs := match xs as list eq with| $hs ++ #x :: $ts -> hs ++ ts
| _
-> xs

The predicate any and every [76] also can be concisely deﬁned with predicate
patterns using match. any is a predicate that determines whether any element of
the second argument list satisﬁes the ﬁrst argument predicate. every is a predicatethat determines whether all elements of the second argument list satisfy the ﬁrst
argument predicate.
def any pred xs := match xs as list something with
| _ ++ ?pred :: _ -> True
| _-> False
def every pred xs := match xs as list something with
| _ ++ !?pred :: _ -> False| _-> True

3.3.1.2

Nested Join-Cons Patterns — The unique and concat Function

By combining multiple join-cons patterns, we can describe more expressive patterns. One example is the unique function. The unique function is deﬁned in thepattern-match-oriented style as follows.
def unique xs := matchAllDFS xs as list eq with
| _ ++ $x :: !(_ ++ #x :: _) -> x

A not-pattern is used to describe that there is no more x after an occurrence ofx. Therefore, this pattern extracts only the last appearance of each element.
unique [1,2,3,2,4] -- [1,3,2,4]

We can deﬁne unique whose results consist of the ﬁrst appearance of eachelement by rewriting the above pattern using a predicate pattern with the elem
predicate. To match only the ﬁrst appearance of an element, we rewrite apattern that ensures that the same element does not appear before that element.
We cannot write such a pattern with a simple combination of the cons and join
patterns because they match a target list from left to right.
def unique xs := matchAllDFS xs as list eq with| $hs ++ (!?(\x -> member x hs) & $x) :: _ -> x
unique [1,2,3,2,4] -- [1,2,3,4]

Another more elegant solution is using a sequential pattern. We can describe
the same pattern by using the sequential pattern for the ﬁrst argument of join.
∗

matchAll also can handle multiple match clauses. matchAll t as m with c1 c2 ... is equivalent to matchAll t as m with c1 ++ matchAll t as m with c2 ++ ....

35

def unique xs := matchAllDFS xs as list eq with
| {@++ $x :: _,!(_ ++ #x :: _)}-> x

Another example of a nested join-cons pattern is concat. We can deﬁne concat
in the pattern-match-oriented style by combining a nested join-cons pattern andmatcher composition. Note that matchAllDFS is necessary for ordering the output
list properly.
def concat xss := matchAllDFS xss as list (list something) with
| _ ++ (_ ++ $x :: _) :: _ -> x

If we used matchAll instead of matchAllDFS for concat, it enumerates the elementsof the input list of lists alternately.
matchAll [[1..], (map negate [1..])] as list (list something) with
| _ ++ (_ ++ $x :: _) :: _ -> x-- [1, 2, -1, 3, -2, 4, -3, 5, -4, 6]

3.3.2

Cons Patterns for Multisets

Cons patterns for a multiset are useful when we want to treat a collection ignoring
the order of elements. We often meet such a situation, especially when describing
mathematical algorithms.
We start from a simple example. The lookup function for association lists canbe deﬁned using a single cons pattern for multiset. A single cons pattern for a
multiset can be replaced by a join-cons pattern for a list.
def lookup k ls := match ls as multiset (eq, something) with| (#k, $x) :: _ -> x

The usage of cons patterns for multisets diﬀers from that of join-cons patterns
when they are nested. Cons patterns for multisets can be used to enumeraten!
P (n, k) = (n−k)!
permutations of k elements, whereas join-cons patterns can ben!
used to enumerate C(n, k) = k!(n−k)!
combinations of k elements.

matchAll [1,2,3] as list integer with
| _ ++ $x :: _ ++ $y :: _ -> (x,y)-- [[1,2],[1,3],[2,3]]
matchAll [1,2,3] as multiset integer with
| $x :: $y :: _ -> (x,y)-- [(1,2),(1,3),(2,1),(2,3),(3,1),(3,2)]

The descriptions of algorithms for which nested cons patterns for multisets are
suitable become complicated in the traditional functional style. We can see thatby just comparing the descriptions of the above two matchAll in functional programming.
However, pattern matching for multisets often appears in mathematical algorithms. Besides that, a much wider variety of patterns exist for multisets thanlists. As a result, functions that correspond to patterns for multisets are not
implemented as library functions because naming all these patterns is not practical. In functional programming so far, they are deﬁned as a recursive function or
combining several functions by users each time. It makes functional descriptionsof mathematical algorithms complicated.
Thus, descriptions of these mathematical algorithms are the area where patternmatch-oriented programming demonstrates its full power. The rest of this chapter
36

discusses how we can describe this wide variety of patterns for multisets by justcombining pattern constructs introduced in Section 3.2.
3.3.3

Tuple Patterns with Sequential Not-Patterns for Comparing
Collections

When describing algorithms, we often meet a situation to compare multiple data.
A tuple pattern combined with not-patterns is especially useful for this purpose.
For example, we can deﬁne difference by inserting a not-pattern into the deﬁnitionof intersect in Section 3.2.8.
def difference xs ys := matchAll (xs, ys) as (set eq, set eq) with| ($x :: _, !(#x :: _)) -> x

By changing the position of the not-pattern as !($x :: _, #x :: _), we can also
describe a pattern that matches when no common element exists between thetwo collections.
We can write more complicated patterns by combining these patterns witha sequential pattern that allows us to apply a not-pattern to separate parts ofthe pattern simultaneously. For example, a pattern that matches when only
one common element exists between the two collections is described below. A
sequential pattern enables us to describe the pattern-matching process that ﬁrst
extracts one common element from the two collections, and after that checks
that no common element exists between the remainder of the two collections.
Sequential not-patterns often appear in mathematical algorithms, and we show
an example again in Section 3.4.1.
def singleCommonElem := match (xs, ys) as (multiset eq, multiset eq) with| [($x :: @, #x :: @),!($y :: _, #y :: _)] -> True
| _ -> False

We can combine a sequential pattern also with a loop pattern. For example, we can write a pattern that matches the common preﬁx of two lists with asequential loop pattern.
match (xs, ys) as (list eq, list eq) with| loop $i (1,$n)[($x_i :: @, #x_i :: @), [...]]!($y :: _, #y :: _)-> map (\i -> x_i) [1..n]3.3.4

Loop Patterns in Practice

Loop patterns are used for describing repetitions in a pattern. It is useful when
we construct a complicated pattern by combining simple pattern constructors(Section 3.3.4.1) and when the number of pattern variables that appear in apattern changes by parameters (Section 3.3.4.2). In such situations, very complicated recursion is necessary for describing algorithms. Loop patterns makethe descriptions of these algorithms intuitive by conﬁning recursion in a pattern.
This section introduces such examples.
3.3.4.1

Pattern Matching for Trees

This section demonstrates loop patterns by showing pattern matching for trees.
The nodes of the trees in this section have an arbitrary number of children as37

XML, and they are handled as a multiset. A matcher for such a tree is deﬁned
as tree in Section 3.2.8. We use this matcher in this section.
We describe patterns for a category tree of programming languages. treeDatadeﬁnes the category tree. For example, "Egison" belongs to the "pattern-matchoriented" category, and the "Dynamically typed" sub-category of the "Functional
programming" category.
def treeData :=Node "Programming language"[Node "pattern-match-oriented" [Leaf "Egison"],Node "Functional language"[Node "Strictly typed" [Leaf "OCaml", Leaf "Haskell", Leaf "Curry", Leaf "Coq"],
Node "Dynamically typed" [Leaf "Egison", Leaf "Lisp", Leaf "Scheme", Leaf
"Racket"]],Node "Logic programming" [Leaf "Prolog", Leaf "Curry"],
Node "Object oriented" [Leaf "C++", Leaf "Java", Leaf "Ruby", Leaf "Python",Leaf "OCaml"]]

The matchAll expression below enumerates all categories to which a speciﬁed
language belongs. A loop pattern is used to describe a pattern for this purpose
because leaves can appear at an arbitrary depth. The ellipsis pattern in this loop
pattern is not placed in the tail of the repeat pattern. The ability to choose theposition of expansion of a repeat pattern allows us to apply the loop patterns totrees.
def ancestors x t := matchAll t as tree string with| loop $i (1,$n)(node $c_i (... :: _))(leaf #x)-> map (\i -> c_i) [1..n]ancestors "Egison" treeData-- [["Programming language", "pattern-match-oriented"], ["Programming language","Functional language", "Dynamically typed"]]It is also possible to enumerate all languages that belong to a speciﬁc subcategory. We can use a doubly-nested loop pattern for this purpose because it
allows the sub-category to appear at an arbitrary depth. The following patternmatches all the languages that belong to a speciﬁed category. We used matchAllDFS
for this enumeration to make the order of the languages in the result the sameas the order with which they appear in the tree.
def descendants x t := matchAllDFS t as tree string with| loop _ (1,_)(node _ (... :: _))(node #x ((loop _ (1,_)(node _ (... :: _))(leaf $y)) :: _))-> ydescendants "Functional language" treeData-- ["OCaml", "Haskell", "Curry", "Coq", "Egison", "Lisp", "Scheme", "Racket"]

Egison is more elegant than XML path language [7] for handling trees because
we can describe the wide range of patterns by just combining a few simple patternconstructors and the loop patterns. In XML path, we would instead have to use
the built-in ancestor command to enumerate all ancestors of a node, for example.

38

3.3.4.2

N-Queen Problem

This section introduces a more tricky example of nested loop patterns by introducing an n-queen solver in Egison. The n-queen problem is the problem ofplacing n chess queens on an n × n board such that no queen can attack any of
the other queens. In chess, a queen can attack other chess pieces on the samerow, column, and diagonal.
Let us start by showing a program for solving the four queen problem. In thisprogram, we represent the positions of the four queens with a list. The numberof the n-th element represents the row number of the queen of the n-th line. The
solution must be a rearrangement of the list [1,2,3,4] because no two queens canbe in the same line or row. Therefore, we pattern-match a collection [1,2,3,4] asa multiset of integers. The requirement that all two queens must not share thesame diagonal is represented with conditions a1 ±1 ̸= a2 , a1 ±2 ̸= a3 , a2 ±1 ̸= a3 ,a1 ± 3 ̸= a4 , a2 ± 2 ̸= a4 , and a3 ± 1 ̸= a4 .
matchAll [1,2,3,4] as multiset integer with$a_1 ::(!#(a_1 - 1) & !#(a_1 + 1) & $a_2) ::(!#(a_1 - 2) & !#(a_1 + 2) & !#(a_2 - 1) & !#(a_2 + 1) & $a_3) ::(!#(a_1 - 3) & !#(a_1 + 3) & !#(a_2 - 2) & !#(a_2 + 2) & !#(a_3 - 1) & !#(a_3 + 1) & $a_4) ::[] -> [a_1,a_2,a_3,a_4]-- [[2,4,1,3],[3,1,4,2]]

We can use a doubly-nested loop pattern for generalizing this pattern for
the n-queen solver. The index pattern variable i of the outer loop is referred
to in the index range of the inner loop pattern for describing the diﬀerence ofthe repeat count of inner loop patterns. Also note that the values bound in
the previously repeated pattern are referred as a_j in #(a_j - (i - j)) and #(a_j + (i - j)). Non-linearity of indexed pattern variables is eﬀectively used for
representing this pattern.
def nQueens n :=matchAll [1..n] as multiset integer with
| $a_1 ::(loop $i (2,n)((loop $j (1, i - 1)(!#(a_j - (i - j)) & !#(a_j + (i - j)) & ...)$a_i) :: ...)[] -> map (\i -> a_i) [1..n]nQueens 4 -- [[2,4,1,3],[3,1,4,2]]

3.4

Pattern-Match-Oriented Programming in More Practical Situations

This section discusses how pattern-match-oriented programming changes the implementation of more practical algorithms and software.
3.4.1

SAT Solver

To see the eﬀect of pattern-match-oriented programming for implementing practical algorithms, we implement a SAT solver. A SAT solver determines whether
a given propositional logic formula has an assignment for which the formula evaluates to true. Input formulae for SAT solvers are often in conjunctive normal
form. A formula in conjunctive normal form is a conjunction of clauses, which39

are disjunctions of literals. A literal is a formula whose form is p or ¬p. For
example, (p ∨ q) ∧ (¬p ∨ r) ∧ (¬p ∨ ¬r) is a formula in conjunctive normal form
that has a solution; p = False, q = True, and r = True.
3.4.1.1

The Davis-Putnam Algorithm

In our implementation, propositional logic formulae in conjunctive normal form
are represented as a collection of collections of literals. We can pattern-matchthem as a multiset of multisets of literals because both ∧ and ∨ are commutative operators. Furthermore, we represent a literal as an integer. We represent
positive and negative literals as positive and negative integers respectively: forexample, p and ¬p are represented as 1 and −1, respectively. Therefore, thematcher for these formulae can be deﬁned by simply composing matchers as
multiset (multiset integer).
The program below shows the main part of our implementation of the DavisPutnam algorithm[46]. The dp function takes a list of propositional variables anda logical formula, and returns True if there is a solution, otherwise returns False.
def dp vars cnf :=match (vars, cnf) as (multiset integer, multiset (multiset integer)) with
| (_, []) -> True
| (_, [] :: _) -> False-- 1-literal rule
| (_, ($l :: []) :: _) -> dp (delete (abs l) vars) (assignTrue l cnf)-- pure literal rule (positive)| ($v :: $vs, !((#(neg v) :: _) :: _)) -> dp vs (assignTrue v cnf)-- pure literal rule (negative)| ($v :: $vs, !((#v :: _) :: _)) -> dp vs (assignTrue (neg v) cnf)-- otherwise| ($v :: $vs, _) ->dp vs((resolveOn v cnf) ++ (deleteClausesWith v (deleteClausesWith (neg v) cnf)))

The ﬁrst match clause states that the input formula has a solution when it
is empty. The second match clause states that there is no solution when clauses
include an empty clause. The third match clause represents 1-literal rule. Whenthe input formula includes a clause with a single literal, we can assign that literal
True at once. The fourth match clause states that if there is a propositionalvariable that appears only positively, we can set the value of this literal Trueand remove the propositional variable from the variable list and the clauses that
include this literal from the formula. For example, (p ∨ q) ∧ (¬p ∨ r) ∧ (¬p ∨ ¬r)contains a propositional variable q only positively, so we can assign q True andremove the ﬁrst clause from the next recursion. The ﬁfth match clause states
the opposite of the fourth match clause. It removes the clauses that include thisliteral if there is a propositional variable that appears only negatively (p in theabove sample is such propositional variable). The ﬁnal match clause applies theresolution principle. The resolveOn function collects all pairs of clauses p ∨ C and¬p ∨ D (let C and D be a disjunction of literals), and returns new clauses C ∨ D.
The above deﬁnition of dp describes all rules of the Davis-Putnam algorithm byfully utilizing pattern matching for multisets. In traditional functional languages,
we need to call several library functions and deﬁne several helper functions to
describe these conditional branches. We can compare this implementation withthe same algorithm implemented in OCaml in [46].

403.4.1.2

Pattern Matching for Resolution

We can elegantly deﬁne the resolveOn function using a sequential not-pattern.
First, let us show a naive implementation of resolveOn. The resolveOn function
is deﬁned with a single matchAll expression as follows.
def resolveOn v cnf := matchAll cnf as multiset (multiset integer) with| (#v :: $xs) :: (#(negate v) :: $ys) :: _-> unique (filter (\c -> not (tautology c)) (xs ++ ys))

The pattern for enumerating the pair of clauses p ∨ C and ¬p ∨ D is described
simply utilizing pattern-matching for a multiset of multisets. Note that the above
resolveOn removes tautological clauses by using the tautology predicate in the bodyof the match clause.
We can remove this use of the tautology predicate by using a sequential notpattern discussed in Section 3.3.3. The sequential pattern is eﬀectively used todescribe that the literal x appeared in xs does not appear negatively in ys.
def resolveOn v cnf :=matchAll cnf as multiset (multiset integer) with| {(#v :: (@ & $xs)) :: (#(neg v) :: (@ & $ys)) :: _,!($l :: _, #(neg l) :: _)}-> unique (xs ++ ys)

3.4.1.3

Separating Two Kinds of Loops

The SAT solver presented in this section is an important sample in the sensethat it is the only sample that contains a loop that we cannot remove by patternmatch-oriented programming. This unremovable loop is the recursion of the dp
function. This recursion is essential for narrowing the search tree. This narrowing
is impossible by simple backtracking. On the other hand, all the other loops thatcan be implemented in backtracking algorithms are pushed into the patterns.
In the traditional style, we usually describe the 1-literal rule and pure literalrules by combining several recursive functions such as find, partition, subtractand intersect [46]. Thus, pattern-match-oriented programming increases thereadability of practical algorithms.
3.4.2

Graph Pattern MatchingThis section demonstrates pattern matching for graphs as sets of edges and adjacency graphs, respectively.
3.4.2.1

Graphs as Sets of Edges

In this section, we pattern-match a graph as a set of edges. We can deﬁne amatcher and graph data as follows.
def graph := set edge
def edge := algebraicDataMatcher| edge integer integer
def graphData :=[ Edge 1 2, Edge 2 1, Edge 2 3, Edge 2 4, Edge 3 4, Edge 4 5, Edge 4 6, Edge 4
7, Edge 5 4, Edge 5 6, Edge 5 7, Edge 6 4, Edge 6 5, Edge 6 7, Edge 7 4, Edge 7
5, Edge 7 6, Edge 7 8, Edge 9 10, Edge 10 7 ]41

Figure 3.1: Visualization of graphData.
This sample graph is visualized in Section 3.1. This section lists several
pattern-matching examples against this graph. Various patterns for graphs canbe described using techniques introduced in this Chapter.
A pattern for listing all nodes that are accessible from s in two edges is
described as follows.
let s := 1 inmatchAll graphData as graph with| edge (#s & $x_1) $x_2 :: edge #x_2 $x_3 :: _-> x-- [1, 3, 4, 5, 6, 7]

A pattern for listing all nodes that possess an edge from s but not to s is
described utilizing a not-pattern eﬀectively.
let s := 1 inmatchAll graphData as graph with| edge #s $x :: !(edge #x #s :: _)-> x-- [4]A pattern for listing all routes from s to e is deﬁned with a loop pattern.
Egison allows users to use the let expression inside a pattern. The let expression
is used to bind s to $x_1. Thanks to this let, we can describe elegantly an initialcondition for $x_1 for the loop pattern.
let (s, e) := (1, 8) inmatchAll graphData as graph with| let x_1 := s inloop $i (2, $n)(edge #x_(i - 1) $x_i :: ...)
(edge #x_(n - 1) (#e & $x_n) :: _)-> map (\i -> x_i) [1..n]-- [[1, 4, 7, 8], ...]A pattern for ﬁnding all cliques whose size is n is given in the following way.
A double-nested loop pattern can be used for that purpose.
let n := 4 inmatchAll graphData2 as graph with| edge $x_1 $x_2 :: loop $i (3, n)(edge #x_1 $x_i :: loop $j (2, i - 1)(edge #x_j #x_i :: ...)...)_-> map (\i -> x_i) [1..n]-- [[4, 5, 6, 7], ...]

42

In this section, we demonstrated pattern matching only for a directed graph.
However, we can also deﬁne a matcher for undirected graphs using a matcher foredges that identiﬁes Edge a b and Edge b a. The matcher for undirected edges isdeﬁned as a user-deﬁned matcher, which we explained in Section 2.5.
3.4.2.2

Adjacency Graphs

This section demonstrates pattern matching for a weighted adjacency list. As
shown in the program below, a matcher for a weighted adjacency list can be
simply deﬁned by composing matchers. graphData in the program below represents
an airline network by a weighted adjacency list. The integers in graphData are thecosts of time by hours to move between two cities.
def graph := multiset (string, multiset (string, integer))def graphData :=[("Berlin", [("New York", 14), ("London", 2), ("Tokyo", 14), ("Vancouver", 13)]),("New York", [("Berlin", 14), ("London", 12), ("Tokyo", 18), ("Vancouver", 6)]),("London", [("Berlin", 2), ("New York", 12), ("Tokyo", 15), ("Vancouver", 10)]),("Tokyo", [("Berlin", 14), ("New York", 18), ("London", 15), ("Vancouver", 12)]),("Vancouver", [("Berlin", 13), ("New York", 6), ("London", 10), ("Tokyo", 12)])]-- List all routes that visit all cities exactly once and return to Berlin.
def trips :=let n := length graphData inmatchAll graphData as graph with| (#"Berlin", (($s_1,$p_1) :: _)) ::loop $i (2, n - 1)((#s_(i - 1), ($s_i, $p_i) :: _) :: ...)((#s_(n - 1), (#"Berlin" & $s_n, $p_n) :: _) :: [])-> sum (map (\i -> p_i) [1..n]), map (\i -> s_i) [1..n]head (sortBy (\(_, x), (_, y) -> compare x y)) trips)-- (["London", "New York", "Vancouver", "Tokyo"," Berlin"], 46)

The above matchAll expression lists all routes from Berlin that visit all the cities
exactly once and return to Berlin. This pattern can be used to solve the travelingsalesman problem. A non-linear loop pattern is used to represent the pattern.
There are several graph database query languages [66, 72, 6]. The advantageof Egison over these query languages is its generality. Egison does not focus
on pattern matching for graphs. Instead, Egison allows users to describe various
patterns by just combining non-linear loop patterns and a small number of simple
pattern constructors.
3.4.3

Computer Algebra

As an application of pattern-match-oriented programming, we have developed acomputer algebra system [31]. We can implement a pattern-matching engine formathematical expressions in a short program by deﬁning a matcher for mathematical expressions.
def mathExpr :=matcher| div $ $ as (mathExpr, mathExpr) with43

| Div $x $y -> [(x, y)]| $tgt -> [(tgt, 1)]| poly $ as multiset mathExpr with| $tgt -> [tgt]| term $ $ as (integer, multiset (mathExpr, integer)) with| Term $c $xs -> [(c, xs)]
| App $ $ as (mathExpr, list mathExpr) with| App $f $args -> [(f, args)]| sym $ as string with| Sym $name -> [name]| $ as something with| $tgt -> [tgt]The matcher for mathematical expressions is used for implementing programsfor simplifying mathematical expressions. For example, a function that simpliﬁes
a mathematical expression by reducing cos2 (θ) + sin2 (θ) to 1 can be implemented
as follows.
def simplifyCosAndSinInPoly poly :=match poly as mathExpr with
poly (term $n ((app (sym #"cos") [$x]), 2) :: $y) :: term #n ((app (sym #"sin") [#x], 2) :: #y) :: r) ->simplifyCosAndSinInPoly (n * (prod (map power y)) + (sum r))_ -> poly

The deﬁnition of a matcher for mathematical expressions is simple comparedwith the pattern-matching engines of the other computer algebra systems. As aresult, the implementation of the whole computer algebra system is also compact
and straightforward; therefore, this computer algebra system is easily extensible.
This extensibility allows us to experiment with new features easily.
This extensibility is a signiﬁcant advantage in the future of computer algebra
systems in the ﬁeld of which there are still notations that are popular among
researchers of mathematics but cannot be used in programs. There are many
possibilities of research for extending computer algebra systems to support thesenotations. The extensibility of computer algebra systems will help us advance
this research.
Such work has already been done by the author. We have developed a natural
method for importing tensor index notation into programming [32]. Thanks tothis work, Egison became an appropriate computer algebra system for describing
formulae of diﬀerential geometry. We will explain this feature in Chapter 5
3.4.4

Database Query Languages

Egison pattern matching can provide a uniﬁed query language for various kinds of
databases. For example, let us consider a database of social network services anda query to list all users who are followed by the user whose name is "Egison_Lang"but who do not follow this user. This query can be written with matchAll as
follows using Egison pattern matching. This query pattern-matches the tables ofa relational database as sets.
matchAll (users, follows, users) as (set user, set follow, set user) with((name #"Egison_Lang") & (id $uid) :: _,(fromID #uid) & (toID $fid) :: !((fromID #fid) & (toID #uid) :: _),(ID #fid) & (Name $fname) :: _) -> (fid, fname)

The above matchAll expression matches a tuple of the user table (users), the follow
table (follows), and the user table. Each table is pattern-matched as a set. The
second line pattern-matches the user table. Name and ID are pattern constructors
44

to access the column of a record. The pattern for the user table in the secondline matches the user whose name is "Egison_Lang" and $uid is bound to the user
ID of that user. The third line pattern-matches the follow table. FromID and ToID
are pattern constructors to match the IDs of follower and followee. The userof FromID follows the user of ToID. IDs of the users who do not follow back theuser whose ID is uid is pattern-matched using a not-pattern. The fourth line
pattern-matches the user table again to get the name of the user whose ID is fid
and returns the tuple (fid, fname).
The conciseness of the queries is an important advantage of Egison over
SQL [26]. For example, the same query described in SQL is more complicated.
We need to write all conditions in WHERE clauses instead of a non-linear pattern
and a sub-query instead of a not-pattern. A query in the pattern-match-oriented
style can be interpreted by reading it once from left to right in order, whereas
one in SQL cannot.
SELECT DISTINCT ON (user.name) user.name
FROM user AS user1, follow AS follow1, user AS user2
WHERE user1.name = 'Egison_Lang' AND follow1.from_id = user1.id AND user2.id =follow1.to_id
AND NOT EXISTS(SELECT '' FROM follow AS follow2
WHERE follow2.from_id = follow1.to_id AND follow2.to_id = user1.id)

List comprehensions also work as a sophisticated query language for relational
databases [88]. The above query can be simply expressed also by list comprehensions. The advantage of Egison to list comprehensions as a query language is its
generality. Egison can be used to express queries not only for relational databases
but also for XML and graph databases. XML path language [7] and graph querylanguages [66, 72, 6] only focus on handling their target data structures and have
many built-in functions to handle various patterns. On the other hand, Egison
pattern-matching system allows users to describe various patterns for various
data types in a uniﬁed manner with a small number of pattern constructors.

3.5

Related Work

This section compares our approach with list comprehensions (Section 3.5.1)
and logic programming (Section 3.5.2) as other approaches to remove explicit
recursions from programs.
3.5.1

List Comprehensions

List comprehensions [67] are another approach to hide explicit recursions. For
example, list comprehensions also allow us to deﬁne map without explicit recursion:
map f xs = [ f x | x <- xs ]However, list comprehensions are too specialized to enumerate elements of a list
and do not allow us to describe complex enumerations as concisely as patternmatch-oriented programming. We can summarize the advantages of patternmatch-oriented programming against list comprehensions as follows:
1. Pattern-match-oriented programming requires less local variables;
2. Pattern-match-oriented programming is more expressive thanks to ad-hoc
polymorphism of patterns and Egison speciﬁc pattern constructs such as
loop patterns and sequential pattern;45

3. Pattern matching can be used to describe conditional branches.
The second and third advantages are obvious. Therefore, in the rest of thissection, we focus on the ﬁrst advantage.
For illustrating the ﬁrst advantage, we write a program that enumerates all
the two combinations of elements in list comprehensions. We described the same
program in pattern-match-oriented programming style in Section 3.3.2. tails isa function that returns all the suﬃxes of the argument list.
comb2 xs = [ (x,y) | x:ys <- tails xs, y <- ys ]The variable ys is necessary for list comprehensions though it is unnecessary inpattern-match-oriented programming. Such variables that are necessary only inlist comprehensions appear when the pattern is nested. As a result, nested joincons patterns for lists (e.g. unique in Section 3.3.1.2) and nested cons patterns
for multisets (e.g. an N-queen solver in Section 3.3.4.2 and a SAT solver in
Section 3.4.1) cannot be described in list comprehensions as concisely as patternmatch-oriented programming.
3.5.2

Comparison with Logic Programming

Logic programming is a programming paradigm proposed with a similar motiveof simplifying the descriptions of backtracking. Logic programming describes
non-deterministic computations using uniﬁcation instead of pattern matching.
Uniﬁcation is a more general notion compared with pattern matching. But the
integration of non-determinism of logic programming and pattern matching is
not obvious. For example, the pattern-matching facility of Prolog is specialized
only for algebraic data types.
We can summarize the advantages of our approach against logic programming
as follows:
1. Our approach proposes syntax specialized for pattern matching of non-freedata types.
2. Our approach is compiler-friendly because our approach directly deﬁnes
methods for decomposing data.
3. Our approach modularizes non-free data types by matchers.
3.5.2.1

Special Syntax for Pattern Matching of Non-free Data Types

We can describe non-linear patterns and backtracking in functional logic programming as we have shown in Section 2.2.1. However, logic programming languages do not provide a special syntactic construct for handling multiple patternmatching results as the matchAll expression of our language. As a result, programsfor non-free data types in logic programming are not as concise as ones in our
approach. Curry [45] provides findall for handling multiple uniﬁcation results. If
we use findall for pattern matching, the program gets more complicated than thefunctional approach. For example, Curry program that deﬁnes the map functionin the pattern-match-oriented style is as follows.
map f xs = findall (\y -> let x free in (_ ++ (x : _)) =:= xs & f x =:= y)

The findall function takes a predicate (a function that returns a boolean value)
and returns a list of values that satisfy the predicate. The predicate passed to46

findall in the above code returns true when both (_ ++ (x : _)) =:= xs and f x =:=y return true. In Curry, & is a boolean operator and =:= represents an equational
constraint. We can represent pattern matching using equational constraints.
The equational constraint (_ ++ (x : _)) =:= xs binds the free variable x to anelement of xs. Then, the equational constraint f x =:= y binds the variable y tof x. Finally, findall returns all the values bound to y. As a result, the above
findall returns a list of results applying f to each element of xs.

3.5.2.2

Compiler-Friendly Pattern Deﬁnitions

The key diﬀerence between logic programming and our approach is in the methodfor deﬁning pattern-match algorithms. Logic programming deduces the methodfor decomposing data from a method for constructing data. For example, inCurry, the cons pattern for multisets, whose name is insert in Curry, is deﬁned
as follows (we demonstrated this pattern constructor in Section 2.2).
12

insert x [] = [x]insert x (y:ys) = x:y:ys ? y:(insert x ys)

The insert function is a non-deterministic function that returns the result of
inserting the ﬁrst argument to the second argument list. The inﬁx operator ? iscalled a non-deterministic operator. The ? operator returns its second argument
for example when the uniﬁcation for the ﬁrst argument fails. It is also possible
to enumerate all the results of a non-deterministic function by using findall
explained in Section 3.5.2.1. The ﬁrst line deﬁnes how to insert x to the empty
list. The second line deﬁnes how to insert x to a non-empty list. The ﬁrst
argument of the ? operator is x:y:ys that means x is inserted into the head of the
non-empty list. The second argument of the ? operator is y:(insert x ys). Thispart uses recursion for inserting the element x into the tail part of the argument
list. insert x ys returns the non-deterministic results of inserting x to ys.
On the other hand, in our proposal, we deﬁne pattern constructors by describing how to decompose data directly. Thanks to that, in our approach, it
is easy to control and optimize the execution process of the internal patternmatch process. For example, we can naturally deﬁne wildcard optimizations in
our approach (Section 2.5.2).
3.5.2.3

Abstraction of Non-free Data Types by Matchers

In our approach, we modularize pattern-match methods not for each pattern but
for each non-free data type using matchers. This abstraction of non-free datatypes improves the readability of programs by ad-hoc polymorphism of patterns
as we explained in Section 2.3.3. Not only that, this abstraction also enables
us to apply more complex optimization like pattern fusion that is explained in
Section 2.5.3

3.6

Conclusion

In this chapter, we have presented programming techniques that replace explicit
recursions for traversing search trees with intuitive patterns and allow programmers to concentrate on the description of the essential parts of algorithms that
reduce the computational complexities of the algorithms. We listed many algorithms that can be represented more elegantly in this way. These include many
very basic list processing functions to some larger more practical algorithms.
We believe the development of these programming techniques that enable the47more intuitive representation of algorithms extends the limit on the complexityof software that we can practically implement and has the potential to accelerate
research of computer science as a whole. We hope our work leads to the further
evolution of pattern matching and the future progress of data abstraction.

48

Chapter 4
Embedding Egison Pattern Matching into
HaskellIn this chapter, we discuss methods for embedding Egison pattern matching into
Haskell. There are three technical challenges for that: (1) we need to design
typing rules for Egison pattern matching; (2) we need to convert Egison patternmatch expressions to a Haskell program; (3) we need to make converted Haskell
programs type-inferable by GHC. In this chapter, we show our solution. We have
implemented our solution in the Haskell library, Sweet Egison. This library has
already been distributed via Hackage. Sweet Egison has three features that theoriginal Egison interpreter does not have: (1) type errors are detected staticallyby the compiler; (2) execution speed is much faster; (3) the users can customize
search strategies for pattern matching.

4.1
4.1.1

Overview
Usage of Sweet Egison

We start from the explanation of the matchAll expression of Sweet Egison. The
matchAll expression collects all the pattern-match results and returns a list of theresults evaluating the body expression for each pattern-match result. A matchclause is constructed using the quasi-quote [81] provided by Template Haskell [75].
The mc quasi-quoter is deﬁned in the proposed library to desugar a match clause.
The matchAll expression below pattern-matches the list [1, 2, 3] with the pattern$x : $xs as a list, and returns the collection of the tuple (x, xs). Patterns thatstart with $ ($x and $xs in this sample) are pattern variables. The evaluation resultof the matchAll expression contains only one element because the cons pattern fora list has only one decomposition.
matchAll dfs [1, 2, 3] (List Something)[[mc| $x : $xs -> (x, xs) |]]-- [(1, [2, 3])]The matchAll expression of Sweet Egison takes an additional argument as its
ﬁrst argument. We specify a search strategy by the ﬁrst argument. By default, we
can choose the depth-ﬁrst and breadth-ﬁrst search strategies. In Sweet Egison,users can deﬁne search strategies by deﬁning their own backtracking monads. It
is an important feature of Sweet Egison when compared to the original Egison
interpreter and Sweet Egison. We explain how to deﬁne backtracking monads in
Section 4.3.2.
take 10 (matchAll dfs [1..] (Set Something)[[mc| $x : $y : _ -> (x, y) |]])

49

-- [(1, 1), (1, 2), (1, 3), (1, 4), (1, 5), (1, 6), (1, 7), (1, 8), (1, 9), (1,10)]
take 10 (matchAll bfs [1..] (Set Something)[[mc| $x : $y : _ -> (x, y) |]])-- [(1, 1), (1, 2), (2, 1), (1, 3), (2, 2), (3, 1), (1, 4), (2, 3), (3, 2), (4,1)]

The matchAll expression takes a list of match clauses and can handle multiple
match clauses. When there are multiple match clauses, matchAll concatenates theresults for each match clause. “matchAll t m [c1 ,c2 ,...]” is equivalent to “matchAllt m [c1 ] ++ matchAll t m [c2 ] ++ ...”.
matchAll dfs [1, 2, 3] (List Something)[[mc| $x : $xs -> (x, xs) |],[mc| _ : $x : $xs -> (x, xs) |]]-- [(1, [2, 3]), (2, [3])]Matchers, the third argument of matchAll, play an important role in achieving
ad-hoc polymorphism of patterns as the original Egison language. The matcherof the program below is (Multiset Something). The cons pattern for a multiset isdeﬁned to decompose a target list into an arbitrary element and the rest elements.
Therefore, the pattern-match results change as follows.
matchAll dfs [1, 2, 3] (Multiset Something)[[mc| $x : $xs -> (x, xs) |]]-- [(1, [2, 3]), (2, [1, 3]), (3, [1,2])]The users can deﬁne matchers and pattern-match algorithms for each pattern ofeach matcher. We call this feature customizability of pattern-match algorithms.
Achieving both customizability and ad-hoc polymorphism of patterns together
is the ﬁrst main technical challenge for implementing this Haskell library. We
explain how to deﬁne matchers in Sweet Egison in Section 4.3.4.
Matching in Sweet Egison allows non-linear patterns as the original Egison
interpreter. The pattern that starts with # is a value pattern. An arbitrary
Haskell expression follows after #. A value pattern checks whether the target andthe content of the value pattern are equal or not. The Eql matcher is deﬁned touse == for checking the equality. The pattern below matches when there are pairsof sequential elements. There are two sequential pairs: (1, 2) and (4, 5). Value
patterns can refer to the values bound to the pattern variables that appear on
the left-side of patterns. For example, the pattern #(x + 1) : $x : _ is invalid.
This restriction makes patterns readable from left to right in order and makes
the internal pattern-match algorithm simple.
matchAll dfs [1, 5, 2, 4] (Multiset Eql)[[mc| $x : #(x + 1) : _ -> (x, x + 1) |]]-- [(1, 2), (4, 5)]

The type of an expression inside a value pattern is inferable by the GHC typechecker. Maintaining non-linear patterns in a static type system of Haskell is alsoa major technical challenge for implementing this Haskell library.
Sweet Egison also provides the match expression, which calculates only the ﬁrst
pattern-match result. The match expression is simply implemented as follows.
match s t m cs = head (matchAll s t m cs)

To keep the code simple, we made use of head to implement match. On failure ofpattern-match, this raises an uninformative exception, but it can be processedby an error handler.
50data Suit = Spade | Heart | Club | Diamond deriving (Eq)data Card = Card Suit Integer
poker :: [Card] -> String
poker cs = match dfs cs (Multiset CardM)[[mc| [card $s $n, card #s #(n-1), card #s #(n-2), card #s #(n-3), card #s #(n-4)] -> "Straight flush" |],[mc| [card _ $n, card _ #n, card _ #n, card _ #n, _] -> "Four of a kind" |],[mc| [card _ $m, card _ #m, card _ #m, card _ $n, card _ #n] -> "Full house"|],[mc| [card $s _, card #s _, card #s _, card #s _, card #s _] -> "Flush" |],[mc| [card _ $n, card _ #(n-1), card _ #(n-2), card _ #(n-3), card _ #(n-4)] ->"Straight" |],[mc| [card _ $n, card _ #n, card _ #n, _, _] -> "Three of a kind" |],[mc| [card _ $m, card _ #m, card _ $n, card _ #n, _] -> "Two pair" |],[mc| [card _ $n, card _ #n, _, _, _] -> "One pair" |],[mc| _ -> "Nothing" |]]Figure 4.1: Pattern matching for poker hand in Sweet Egison
We can use Sweet Egison for pattern matching of poker hand as shown in
Figure 4.1. We can represent each poker hand in a single pattern by patternmatching a list of cards as a multiset. The CardM matcher is a matcher for playing
cards. “[p1 , p2 , ..., pn ]” is syntactic sugar of a pattern whose form is “p1 : p2 :... : pn : []”.
There are two features not implemented in Sweet Egison. First, some nonstandard pattern constructs, such as loop patterns, indexed pattern variables,and sequential patterns, are not implemented in Sweet Egison. Loop patterns
and indexed pattern variables are used for representing the repetitions insidea pattern (Section 3.2.6). Sequential patterns are used to control the order ofpattern matching (Section 3.2.7). Second, the users of Sweet Egison cannot deﬁnepattern fusions. Sweet Egison cannot pattern-match patterns when deﬁning amatcher. This is because the users deﬁne each pattern as a function. We explain
this limitation in Section 4.3.6.
4.1.2

Compiling Method

Our key idea is to transform patterns into a program that uses backtracking
monads such as the standard list monad. For example, this matchAll expression
matchAll dfs [1, 2, 3] (Multiset Something) [[mc| $x : $xs -> (x, xs) |]]-- [(1, [2, 3]), (2, [1, 3]), (3, [1, 2])]is converted to the following Haskell program:(\ (matcher, target) -> do(x, xs) <- cons matcher target -- [(1, [2, 3]), (2, [1, 3]), (3, [1, 2])]let (_, _) = consM matcher target -- (Something, Multiset Something)return (x, xs))
(Multiset Something, [1, 2, 3]) -- [(1, [2, 3]), (2, [1, 3]), (3, [1, 2])]The cons (the alias of :) and consM functions are user-deﬁned functions that posses
the pattern-match method for the cons pattern. They are called next-target function and next-matcher function, respectively. The cons function takes a matcher
and a target and returns a list of results of decomposing the target. We need topass a matcher to next-target functions to make them polymorphic. For example,
the cons function for multisets returns all the pairs of an element and the rest of
the target list.
51

cons (Multiset Something) [1, 2, 3]-- [(1, [2, 3]), (2, [1, 3]), (3, [1, 2])]The consM function deﬁnes how these decomposed data are pattern-matched in
the next step.
consM (Multiset Something) [1, 2, 3]-- (Something, Multiset Something)

Each result of the cons function (e.g., 1 and [2, 3]) is pattern-matched as Something
and Multiset Something, respectively.
Next, we show the conversion of nested patterns. Patterns are transformedin sequence in the same do expression, therefore we can refer to the values thatare bound to the pattern variables in the left side of a pattern. For example, thefollowing non-linear pattern matching
matchAll dfs [1, 2, 3, 4] (Multiset Eql)[[mc| $x : #(x * 2) : _ -> (x, x * 2) |]]-- [(1, 2), (2, 4)]is converted as follows.
(\ (matcher, target) -> do(x, target') <- cons matcher target
let (_, matcher') = consM matcher target(target'', _) <- cons matcher' target'
let (matcher'', _) = consM matcher' target'
value (x * 2) matcher'' target''return (x, y))(Multiset Eql, [1, 2, 3, 4])

In the above program, value is a next-target function for handling value patterns.
The value function is user-deﬁned like the cons function. Users can deﬁne how tohandle value patterns for each non-free data type.
4.1.3

Organization of This Chapter

The rest of this chapter is organized as follows. Section 4.2 proposes a set of typing
rules for matchAll, matchers, patterns, and match clauses. Section 4.3 explains
the implementation of Sweet Egison. Section 4.5 shows the benchmarking results.
Section 4.6 concludes the chapter.

4.2

Typing Rules

This section shows a set of typing rules that we designed for Typed Egison [54],a variation of Egison with a static type system. As the original Egison is a
dynamically typed programming language, we need to devise typing rules for
Egison’s non-linear patterns with ad-hoc polymorphism.
Figure 4.2 shows the set of typing rules. In the rules, meta-variables x, e, p,
and C denotes a variable, expression, pattern, and pattern constructor, respectively. We write T and S to denote types, Γ and ∆ to denote type environmentsand ϵ to denote an empty type environment. We also write [T ] to denote a typeof a list of elements of type T . Matcher and Pattern are built-in type constructors: Matcher T is a type of a matcher for T ; Pattern T is a type of a pattern
for T .
The type judgement Γ ⊢ e : T states that e has the type T under the typeenvironment Γ. The other type judgment Γ; ∆ ⊢ p : T ; ∆0 states that the pattern52

A typing rule for matchAllΓ ⊢ e 1 : T1
Γ ⊢ e2 : Matcher T1
Γ; ϵ ⊢ p : Pattern T1 ; ∆Γ, ∆ ⊢ e3 : T3
T-MatchAll
Γ ⊢ matchAll e1 as e2 with p -> e3 : [T3 ]Typing rules for patterns

Γ; ∆ ⊢: Pattern T ; ∆TP-WC

Γ, ∆ ⊢ e : T
TP-ValueΓ; ∆ ⊢ #e : Pattern T ; ∆Γ; ∆ ⊢ $x : Pattern T ; ∆, (x : T )TP-VarΓ ⊢ C : (Pattern S1 , · · · , Pattern Sn ) → Pattern TΓ; ∆0 ⊢ p1 : Pattern S1 ; ∆1
Γ; ∆1 ⊢ p2 : Pattern S2 ; ∆2
· · · Γ; ∆n−1 ⊢ pn : Pattern Sn ; ∆n
TP-Constructor
Γ; ∆0 ⊢ (C p1 p2 ... pn ) : Pattern T ; ∆nFigure 4.2: Typing rules for matchAll and patterns of Typed Egisonp is to be matched against a value of type T under the type environment Γ; ∆,where the additional environment ∆ gives type assignment on pattern variables
that occur on the left of p.∗ This judgement denote that p has the type T
under the type environment Γ and ∆ updating ∆ to ∆0 . ∆ is an additional typeenvironment that describes the types of variables bound to the left of the patternp. The comma-separated pair Γ, ∆ concatenates the two type environments Γand ∆, where type assignments x in ∆ may override those in Γ.
We explain the typing rules for patterns, focusing on the type environments∆ for patterns. The type environment ∆ keeps track of types of pattern variables
in non-linear patterns. The rule (TP-Var) adds a type binding for each patternvariable. These assignments in ∆ are used to type-check the content of a value
pattern (TP-Value). The type environment ∆ is updated and passed in apattern in order from left to right (TP-Constructor).
In ﬁgure 4.2, we do not deﬁne the behavior for the case where a single pattern
has multiple occurrences of the same pattern variables. This is because we cannot
ﬁnd a useful example that contains such a pattern. Currently, we implementminiEgison to override the binding on variable x, if x ∈ dom(∆) in TP-Var.
A value pattern #x refers to the value matched by the closest preceding patternvariable $x.

4.3

Implementation of Sweet Egison

Sweet Egison embeds Egison pattern matching into Haskell by converting patterns to a program that uses backtracking monads by utilizing the meta-programming
facility of Haskell. There are three technical challenges for implementing Sweet
Egison.
1. Prepare backtracking monads for both depth-ﬁrst search and depth-ﬁrst
search.

∗We borrow this notation from [51].

532. Design a set of translation rules that convert Egison pattern-match expressions to Haskell programs that are type-inferable.
3. Enable the users to deﬁne their own patterns and matchers.
This section explains our solution. Section 4.3.1 implements the backtracking
monads for depth-ﬁrst search and breadth-ﬁrst search, and explains the methodfor deﬁning new backtracking monads. Section 4.3.2 explains how Sweet Egison
controls the search strategy for pattern matching utilizing these backtracking
monads. Section 4.3.3 explains how we convert a pattern-match expression toa Haskell program that uses the backtracking monads. Section 4.3.4 explains
how we deﬁne matchers in Sweet Egison. Section 4.3.5 explains the type of thepattern-match expressions in Sweet Egison. Section 4.3.6 explains the optimization techniques implemented in Sweet Egison.
4.3.1

Backtracking Monads

The goal of this section is to deﬁne backtracking monads that behave as follows.
toList (dox <- (fromList [1,2,3] :: DFS Integer)y <- fromList [1,2,3]
return (x, y))-- [(1,1),(1,2),(1,3),(2,1),(2,2),(2,3),(3,1),(3,2),(3,3)]
toList (dox <- (fromList [1,2,3] :: BFS Integer)y <- fromList [1,2,3]
return (x, y))-- [(1,1),(1,2),(2,1),(1,3),(2,2),(3,1),(2,3),(3,2),(3,3)]

The ﬁrst and second expressions use the DFS and BFS monads, respectively. We
switch a search strategy by changing the monad. The toList and fromList functions deﬁne the conversion between the value of these backtracking monads andlists. To make these conversion functions polymorphic, we deﬁne the MonadSearchtype class. The MonadSearch type class takes the type variable m as its argument.
This argument is used to represent two class methods, fromList and toList, arepolymorphic to m.
class MonadSearch m where
fromList :: [a] -> m a
toList:: m a -> [a]The implementation of the DFS monad is simple because we can use the list
monad as the DFS monad. We deﬁne the type constructor DFS as the alias of thetype constructor of lists.
type DFS = []Then we can use the id function for both fromList and toList.
instance MonadSearch [] where
fromList = id
toList = id

Our implementation of the BFS monad follows Spivey’s method [78]. It is
known by Spivey that we can implement a monadic interface also for breadth-ﬁrst
search. Spivey’s monad uses a list of lists as the data structure for a backtracking monad for breadth-ﬁrst search. Here is an implementation of a monad forbreadth-ﬁrst search.
54

newtype BFS a = BFS [[a]]instance MonadPlus BFS wheremzero = BFS []mplus (BFS xss) (BFS yss) = BFS (merge xss yss)wheremerge :: [[a]] -> [[a]] -> [[a]]merge [] [] = []merge xss [] = xss
merge [] yss = yss
merge (xs:xss) (ys:yss) = (xs ++ ys) : merge xss yss
instance Monad BFS wherereturn x = BFS [[x]]BFS [] >>= _ = BFS []BFS (xs:xss) >>= f = foldl mplus mzero (map f xs) mplus shift (BFS xss >>= f)
whereshift :: BFS a -> BFS ashift (BFS xss) = BFS ([] : xss)

In fact, the above program implements the identical algorithm that traverses
the binary reduction tree we discussed in Section 2.4.2. The list of lists in thisbacktracking monad represents the list of lists of matching states in the same
depth level in a binary reduction tree.
The conversion for a backtracking monad for breadth-ﬁrst search is deﬁned
as follows.
instance MonadSearch BFS where
fromList xs = BFS (map (\x -> [x]) xs)
toList (BFS xss) = concat xss

We can investigate how this BFS monad backtracks in breadth-ﬁrst order by
the following code (the negate function changes the sign of the given integer).
do x <- (fromList [1..] :: BFS Integer)y <- fromList (map negate [1..])
return (x, y))-- [[(1, -1)], [(1, -2), (2, -1)], [(1, -3), (2, -2), (3, -1)], ...]We have implemented the library that provides the above DFS and BFS monads.
We make this program open to public as a Hackage library [35]. Sweet Egison
uses this Haskell library.
4.3.2

Control of Search Strategy

For enabling the users to choose a search strategy, we transform pattern-match
expressions to do expressions that use the monads that are instances of theMonadSearch type class. For example, the pattern-match expression
matchAll strategy [1..] (Set Something) [[mc| $x : $y : _ -> (x, y) |]]is transformed as follows:
1
2
3
4
5
6
7
8

toList((\ (matcher, target) -> do(x, target') <- fromList (cons matcher target)
let (_, matcher') = consM matcher target(y, _) <- fromList (cons matcher' target')let (_, _) = consM matcher' target'
return (x, y))(strategy (Set Something, [1..])))

55

The fromList function is applied to the result of next-target functions. The toList
function is applied to the return value of the do expression. The strategy function,
the ﬁrst argument of matchAll, is used to initialize the monad value that is passed
to the do expression. The strategy function takes the tuple that consists of thematcher and the target of matchAll. As shown in Section 4.1.1, we pass dfs or bfs
to the ﬁrst argument of matchAll.
Now, we explain the implementation of dfs and bfs. The dfs and bfs functions
take a single value and return the monad value. The dfs strategy is deﬁned asfollows.
dfs :: a -> DFS a
dfs x = [x]The bfs strategy is deﬁned as follows.
bfs :: a -> BFS a
bfs x = fromList [x]We can use the fromList function for this purpose.
4.3.3

Translation Rules

Figure 4.3 shows the list of translation rules implemented in the mc quasi-quoter.
The mc quasi-quoter converts a match clause to a function that takes a tuple ofa matcher and target, and returns the results of evaluating the body for eachpattern-match result. In Figure 4.3, [mc| p → e |] is abbreviated to [| p → e |].
The rest of this section explains each translation rule by showing the speciﬁc
examples.
4.3.3.1

Converting Wildcards

We do nothing to pattern-match a wildcard because pattern-matching of a wildcard always succeeds.
[mc| _ -> body |]\ (_, _) -> return body

4.3.3.2

Converting Pattern Variables

The only diﬀerence from the translation rule of a wildcard is that we assign thetarget to the pattern variable. Pattern-matching of a pattern variable also always
succeeds.
[mc| $x -> body |]\ (_, target) -> do
let x = target
return body

4.3.3.3

Converting Value Patterns

A value pattern is converted to a program that calls the value next-target function.
The value function checks whether its ﬁrst and third arguments are equal or not.
If they are equal, the value function returns a non-empty list. Otherwise, it
returns the empty list.
56

wildcard[|→ e |] = \ ( , ) → return epattern variable[| $x → e |] = \ ( , t) → let x = t in return evalue pattern[| #v → e |] = \ (m, t) → f romList (value v m t) >> return eempty tuple pattern[| () → e |] = \ ((), ()) → return etuple pattern[| (p1 , · · · , pn ) → e |] = \ ((m1 , · · · , mn ), (t1 , · · · , tn )) →[| p1 → [| (p2 , · · · , pn ) → e |](m2 , · · · , mn ) (t2 , · · · , tn ) |] m1 t1
constructor pattern[| c p1 · · · pn → e |] = \ (m, t) → do {(t1 , · · · , tn ) ← f romList (c m t);let (m1 , · · · , mn ) = cM m t;[| (p1 , · · · , pn ) → e |] (m1 , · · · , mn ) (t1 , · · · , tn ) }Figure 4.3: Translation rules of match clauses[mc| #v -> body |]\ (matcher, target) -> do
fromList (value v matcher target)
return body

4.3.3.4

Converting Tuple Patterns

When the pattern is the empty-tuple pattern, the corresponding matcher andtarget must be the empty tuple. Otherwise, the pattern-match expression causesa type error at compile time.
[mc| () -> body |]\ ((), ()) -> return body

The elements of a non-empty tuple pattern are converted in sequence from thepattern of the ﬁrst element in order. We use recursion in the translation rule ofthe tuple pattern for implementing this sequential conversion.
[mc| ($x, $y) -> body |]\ ((m1, m2), (t1, t2)) -> do
let x = t1
do let y = t1
return body57

4.3.3.5

Converting Constructor Patterns

A constructor pattern is converted to a program that calls the corresponding nexttarget and next-matcher functions. The number of elements of the tuples returnedby these functions is the same as the number of the argument of constructor
patterns. We use the translation rules for tuple patterns for handling the next
targets and matchers.
[mc| cons $x $y -> body |]\ (matcher, target) -> do(t1, t2) <- fromList (cons matcher target)(m1, m2) <- consM matcher target
do let x = t1
do let y = t2
return body

4.3.4

Deﬁning Matchers

This section explains how we deﬁne user-deﬁned patterns and matchers.
The relationship between a matcher and its target datatype is represented
using a multi-parameter type class [48] that declares no class method. The type
constraint Matcher m t asserts that m is a matcher for t.
class Matcher m t

We can declare that data of some type are matchers for data of another typeby instance declaration for Matcher. The following instance declaration assertsthat Eql is a matcher for the type a that is an instance of Eq. Basically, a matcher
is deﬁned as a singleton type.
data Eql = Eql
instance Eq a => Matcher Eql a4.3.4.1

Matchers for Collections

This section explains how we deﬁne polymorphic patterns in Sweet Egison by
showing the deﬁnition of the cons pattern for a multiset.
The List m matcher is deﬁned as a data type whose type and data constructor
are identical.
data List m = List m

The List m matcher is an instance of the Matcher type class. This instance declaration asserts that List m is a matcher for a list of elements of the type t when mis a matcher for the type t.
instance Matcher m t => Matcher (List m) [t]The deﬁnition of the Multiset datatype is completely the same as that of List.
data Multiset m = Multiset m
instance Matcher m t => Matcher (Multiset m) [t]The patterns for collections are deﬁned as functions of the CollectionPat typeclass. In the following code, the deﬁnitions of the nil and join patterns areomitted.

58

class CollectionPattern m t wheretype ElemM mtype ElemT t
consM :: m -> t -> (ElemM m, m)cons :: m -> t -> (ElemT t, t)

Index type families (ElemM and ElemT) are used for extracting the matcher and typeof the elements of a target collection. The consM function takes a matcher andreturns the next matchers. The cons function takes a target datum and returns
the next targets. The pattern-match algorithm for the cons pattern is boundto cons because we implement the mc quasi-quoter to desugar “:” in patterns tothe cons pattern constructors. For example, the pattern $x : _ is desugared tocons $x _.
Then, the pattern-match algorithms for the cons pattern of List m and Multiset
m can be deﬁned as an instance of CollectionPat.
instance Matcher m t => CollectionPattern (List m) [t] wheretype ElemM (List m) = m
type ElemT [t] = t
consM (List m) _ = (m, List m)cons _[]= []cons (List _) (x : xs) = [(x, xs)]
instance Matcher m t => CollectionPattern (Multiset m) [t] wheretype ElemM (Multiset m) = m
type ElemT [t] = t
consM (Multiset m) _ = (m, Multiset m)cons (Multiset _) xs = matchAll dfs xs (List Something)[[mc| $hs ++ $x : $ts -> (x, hs ++ ts) |]]4.3.4.2

The Eql Matcher

This section explains how to deﬁne a pattern-match algorithm for value patterns.
First, we start from the deﬁnition of the Eql matcher. Eql is a matcher fordata types that belong the Eq type class.
data Eql = Eql
instance Eq a => Matcher Eql a

As we explained in Section 4.3.3, the value pattern is converted to the applicationof the value next-target function. The value next-target function is deﬁned as afunction of the ValuePattern type class to achieve ad-hoc polymorphism. The ﬁrst
argument of value is a value passed to the value pattern. The value function
compares this value with the target that is passed as the third argument. The
value function has the default deﬁnition that compares the value and the target
using ==.
class Eq t => ValuePattern m t where
value :: t -> m -> t -> [()]
default value :: Eq t => t -> m -> t -> [()]
value e _ v = if e == v then [()] else []We use the default deﬁnition of value for the Eql matcher. The Eql matcher uses== for pattern-matching value patterns.
instance Eq a => ValuePattern Eql a

Ad-hoc polymorphism of value allows us to deﬁne equality of non-free datatypes for which we cannot use ==. For example, we can deﬁne a pattern-match
method for a value pattern of a multiset as follows.
59

instance (Eq a, Matcher m a, ValuePattern m a)=> ValuePattern (Multiset m) [a] where
value e () (Multiset m) v = match dfs (xs, ys) (List m, Multiset m)[ [mc| ([], []) -> True |], [mc| ($x : $xs, #x : #xs) -> True |], [mc| _ -> False |] ]4.3.4.3

The Something Matcher

The deﬁnition of the Something matcher is simple in Sweet Egison. This is because
the pattern-match method for wildcards and pattern variables are already deﬁned
in our translation rules. In the following code, we just declare that we can use
the Something matcher for all the data types.
data Something = Something
instance Matcher Something a

4.3.5

Typing the Pattern-Match Expressions

This section explains the type of the matchAll expression of Sweet Egison. The
matchAll expression is deﬁned in Haskell as follows.
matchAll:: (Matcher m t, MonadSearch s)=> ((m, t) -> s (m, t))
-> t
-> m
-> [(m, t) -> s r]-> [r]
matchAll strategy target matcher =concatMap (\clause -> toList (strategy (matcher, target) >>= clause))

The type constraint Matcher m t states that m is a matcher for t. The ﬁrst argument is a search strategy whose type is ((m, t) -> s (m, t)). As we explainedin Section 4.3.2, a search strategy is a function that creates data of a type thatis an instance of the MonadSearch type class. The type of the forth argument is[(m, t) -> s r]. This represents the type of a list of converted match clauses. As
we explained in Section 4.3.3, a match clause is converted to a function that takes
a tuple of a matcher and target and returns the results evaluating the body foreach pattern-match result.
4.3.6

Optimization

We have implemented wildcard optimization and pattern fusion in Sweet Egison.
This section explains how we have implemented them.
4.3.6.1

Wildcard Optimization

Wildcard optimization omits the calculation of the target that matches wildcard(Section 2.5.2). For example, if the second argument of the cons pattern is a
wildcard, we do not need to calculate the rest.
matchAll dfs [1, 2, 3] (Multiset Something)[[mc| $x : $xs -> (x, xs) |]]-- [(1, [2, 3]), (2, [1, 3]), (3, [1, 2])]60

matchAll dfs [1, 2, 3] (Multiset Something)[[mc| $x : _ -> x |]]-- [1, 2, 3]

For wildcard optimization, we add an argument to the deﬁnition of patterns
to tell whether the argument pattern is wildcard or not. If an argument is a
wildcard, the pattern returns undefined as the next target. Thus, we omit thecalculation.
cons (GP, WC) (Multiset Something) [1, 2, 3]-- [(1, undefined), (2, undefined), (3, undefined)]cons (GP, GP) (Multiset Something) [1, 2, 3]-- [(1, [2, 3]), (2, [1, 3]), (3, [1, 2])]GP and WC are data constructors of PP and abbreviations of a general pattern andwildcard, respectively. PP is the abbreviation of a pattern for patterns.
data PP = WC | GP

Let us see how the deﬁnition of the cons pattern for multisets changes. The
cons function takes a pair of patterns for patterns as its ﬁrst argument because
the cons pattern takes two patterns as its argument.
class CollectionPattern m t where...
cons :: (PP, PP) -> m -> t -> (ElemT t, t)...

Here is a deﬁnition of the cons function. When the second argument of the cons
pattern is a wildcard, the cons function does not compute the rest elements.
instance Matcher m t => CollectionPattern (Multiset m) [t] where...
cons (_, WC) (Multiset _) xs = map (\x -> (x, undefined)) xs(Multiset _) xs = matchAll dfs xs (List Something)cons _[[mc| $hs ++ $x : $ts -> (x, hs ++ ts) |]]...

4.3.6.2

Pattern Fusions

Pattern fusion is invented for applying wildcard optimization for nested patterns(Section 2.5.3). For example, we can apply pattern fusion for a join pattern whose
second argument is a cons pattern.
matchAll dfs [1, 2, 3] (List Something)[[mc| _ ++ $x : _ -> x |]]-- [1, 2, 3]

If we handle join and cons separately, we calculate all the suﬃxes and get theﬁrst element of each suﬃx.
do (_, target') <- join (Wildcard, GeneralPat) target(x, _) <- cons (GeneralPat, Wildcard) target'
return x

On the contrary, if we handle join and cons at the same time and apply wildcard
optimization, we can omit the calculation of all the suﬃxes of the target list andjust enumerate its elements.
do (_, x, _) <- joinCons (Wildcard, GeneralPat, Wildcard) target
return x

61

We deﬁne the joinCons function as follow.
joinCons (WildCard, GeneralPat, Wildcard) (List Something) [1, 2, 3]-- [(undefined, 1, undefined), (undefined, 2, undefined), (undefined, 3,
undefined)]

Currently, Sweet Egison does not allow the users to deﬁne new pattern fusion.
The transformation from _ ++ $x : _ to joinCons _ $x _ is hard-coded in the implementation of the mc quasi-quoter that transforms patterns to do expressions.
On the other hand, the original Egison language has a user interface for deﬁning
pattern fusion. Pattern fusion is deﬁned by pattern-matching patterns. We may
borrow this user interface when we implement Sweet Egison as a GHC extension.
list a = matcher| _ ++ $ : _ as a with| tgt -> tgt| _ ++ $ as list a with| tgt -> tails tgt| $ ++ $ as (list a, list a) with
...

4.3.7

Summary

Sweet Egison transforms an Egison pattern-match expression to a Haskell program whose appearance is similar to a program that we manually write whendescribing backtracking. We summarize our method for this transformation as
follows.
1. The users can deﬁne their own search strategies by deﬁning a backtracking
monad (Section 4.3.1).
2. Sweet Egison transforms a match clause to a program that uses a backtracking monad by the quasi-quote of Template Haskell (Section 4.3.2 andSection 4.3.3).
3. Sweet Egison allows the users to deﬁne polymorphic patterns as the originalEgison interpreter (Section 4.3.4).
4. Both wildcard optimization and pattern fusion are implemented in Sweet
Egison (Section 4.3.6).

4.4

Related Work

Over the decades, several pattern-match extensions have been proposed and implemented in Haskell. Views [92] are an early such extension that provides users
with the user-customizable pattern matching facility. Views allow the users todeﬁne custom pattern-match algorithms for each pattern constructor. However,views support neither non-linear patterns nor pattern matching with backtracking. Active patterns [39] provides the user-customizable pattern matching facility
with non-linear patterns. However, active patterns do not support backtracking
and thus fail to fully utilize the expressiveness of non-linear patterns. First-classpatterns [89] provides the user-customizable pattern matching with backtracking.
However, ﬁrst-class patterns do not support non-linear patterns. The patternmatch system of Egison can be regarded as an extension that supports all thefeatures proposed above: user-customizable pattern-match algorithms; non-linear
patterns; pattern matching with multiple results. Implementations of some of the62

Functional styleminiEgison
Sweet Egison(w/o patternfusion)Sweet Egisoncomb2(n = 15, 000)
0.323
16.123comb2(n = 30, 000)
1.264
63.45

perm2
(n = 5, 000)
0.717
6.287

perm2
(n = 10, 000)
3.862
25.133

1.291

5.077

0.686

3.572

0.291

1.035

0.690

3.483

Table 4.1: Execution time of comb2 and perm2 in seconds
above pattern-match extensions are available as open-source and compilable withthe latest GHC. Views are implemented as a GHC extension. First-class patterns
are implemented as a Haskell library by Pope and Yorgey and distributed via
Hackage [69].
Sweet Egison is not the ﬁrst attempt to implement the Egison pattern-match
facility as a library of mainstream functional programming languages. Before
Sweet Egison, we developed miniEgison, a library that provides the Egison patternmatch facility, in Scheme [34] and Haskell.
We brieﬂy explain the approach taken by miniEgison. MiniEgison also transforms Egison pattern-match expressions to the Haskell programs. But the method
for this transformation is diﬀerent. MiniEgison embeds an interpreter for Egison pattern matching, whereas Sweet Egison embeds a compiler. MiniEgison
calls this interpreter via the patternMatch function that implements the internal pattern-match algorithm, reduction of matching states that have a stack ofmatching atoms, explained in Section 2.4. The patternMatch function takes a pattern, target, and matcher and returns pattern-match results. Here is an exampleof the conversion by MiniEgison.
matchAll [1, 2, 3] (Multiset Something)[mc| $x : $y : _ -> (x, y) |]map (\x, y) -> (x, y))(patternMatch [1, 2, 3] (Multiset Something) ($x : $y : _))In implementing miniEgison, we heavily reuse the ideas from the implementationof the ﬁrst-class patterns [69]: a pattern is deﬁned as a function that takes a target
and returns a pattern-match result, which is represented by a heterogeneous
list. The development of the conversion of miniEgison is not straightforward
because we need to make converted programs automatically type-inferable by
GHC. Especially, typing of matching states was challenging. GHC extensions
such as GADTs and existential types play essential roles for this purpose.

4.5

PerformanceThis section discusses the execution performance of Sweet Egison. First, we
compared the performance of programs that enumerate two combinations andpermutations of elements, namely comb2 and perm2, implemented in a traditional
functional style and pattern-match-oriented style in Haskell. Table 4.1 shows thebenchmark results. The deﬁnitions of the comb2 and perm2 functions are shown in
Figure 4.4. The comb2 function contains a join-cons pattern that we can apply
pattern fusion. Let us remind you that pattern fusion is not implemented inminiEgison.
63

EgisonminiEgison
Sweet Egison

CDCL(20 vars)
2.114
0.045
0.026

CDCL
(50 vars)
40.565
1.459
0.120

CDCL
(75 vars)
1175.28
15.9571.036

CDCL(100 vars)
n/a347.8227.471

Table 4.2: Execution time of SAT solvers in seconds
comb2 :: Int -> [(Int, Int)]comb2 n = matchAll dfs [1 .. n] (List Something)[[mc| _ ++ $x : _ ++ $y : _ -> (x, y) |]]comb2Native :: Int -> [(Int, Int)]comb2Native n = [ (x, y) | (x : ts) <- tails [1 .. n], y <- ts ]perm2 :: Int -> [(Int, Int)]
perm2 n = matchAll dfs [1 .. n] (Multiset Something)[[mc| $x : $y : _ -> (x, y) |]]perm2Native :: Int -> [(Int, Int)]
perm2Native n = go [1 .. n] [] []wherego [] _ acc = acc
go (x : xs) rest acc =[ (x, y) | y <- rest ++ xs ] ++ go xs (rest ++ [x]) acc

Figure 4.4: Benchmark programs
We also benchmarked our implementation of conﬂict-driven clause learning(CDCL), an algorithm for solving SAT, in a pattern-match-oriented programming style. Table 4.2 shows the benchmark results. The complete benchmarking
program is accessible on GitHub [56]. Our program for CDCL does not containa pattern that we can apply pattern fusion.
We compiled our benchmarks by the Glasgow Haskell Compiler (GHC) 8.10.7
and ran them on a 2.3GHz Dual-Core Intel Core i5 processor with 16GB of
RAM. We passed the options -O3 -threaded -rtsopts -with-rtsopts=-N to GHC forcompiling the above programs. The benchmark results show that:• Pattern-match-oriented style programs written in Sweet Egison are as fast
as traditional functional style programs in Haskell.
• Sweet Egison runs about 100 times faster than the original Egison interpreter.
• Sweet Egison runs about 10 times faster than miniEgison.
• Pattern fusion is important for improving execution performance.
The performance diﬀerence between miniEgison and Sweet Egison comes fromminiEgison’s internal pattern-match algorithm as a reduction of matching states,
which makes it hard to be optimized by GHC.

4.6

Conclusion

In this chapter, we showed that user-customizable non-linear pattern matchingwith backtracking implemented in the Egison programming language is implementable as a Haskell library. We showed that Egison pattern matching can be64statically typed. Thanks to the static type system, we can detect type errors atcompile time before executing programs. For this purpose, we proposed a new setof typing rules and a method for embedding these typing rules in Haskell utilizing
GHC extensions. These typing rules allow us to handle ad-hoc polymorphism ofpatterns and non-linear patterns.
The proposed library makes Egison pattern matching accessible from Haskell
users — a majority of functional programmers. Not only that, the proposed library is much faster than the original Egison interpreter and endures practicaluse. We have already utilized Sweet Egison for implementing the computer algebra system implemented in the Egison interpreter. We hope the proposed libraryincreases the number of Egison fans and leads to more inventions of practicalapplications of pattern-match-oriented programming.

65

Chapter 5
Computer Algebra System and Tensor Index
Notation
5.1

Overview

In mathematics, many notations have been invented for the concise representationof mathematical formulae. Tensor index notation is one of such notations and has
been playing a crucial role in describing formulae in mathematical physics. In thischapter, we show a programming language that can deal with symbolic tensor
indices by introducing a set of tensor index rules that is compatible with two
types of parameters, i.e., scalar and tensor parameters. When a tensor parameterobtains a tensor as an argument, the function treats the tensor argument as awhole. In contrast, when a scalar parameter obtains a tensor as an argument,
the function is applied to each component of the tensor. On a language withscalar and tensor parameters, we can design a set of index reduction rules thatallows users to use tensor index notation for arbitrary user-deﬁned functions
without requiring additional description. Furthermore, we can also design index
completion rules that allow users to deﬁne the operators concisely for diﬀerential
forms such as the wedge product, exterior derivative, and Hodge star operator.
In our proposal, all these tensor operators are user-deﬁned functions and can bepassed as arguments of high-order functions. We have implemented our proposal
in the computer algebra system that is implemented in the interpreter of ourlanguage using Sweet Egison.
This chapter is organized as follows. Section 5.2 introduces related work.
Section 5.3 proposes our symbolic index reduction rules for importing tensor index
notaion. Section 5.4 proposes our symbolic index completion rules for describing
formulae that handle diﬀerential forms. Section 5.5 demonstrates our computer
algebra system. Section 5.6 evaluates our proposal. Section 5.7 concludes thischapter.

5.2

Related Work

This section classiﬁes the existing method for handling tensor index notation inprograms.
5.2.1

Syntax-based Approach

The current major method for dealing with tensors is using a special syntax
for describing loops for generating multi-dimensional arrays. The Table [13] expression from the Wolfram language is such a syntax construct. Xij + Yij isrepresented as follows with the Table expression. The following program assumes

66that the length of each dimension corresponding to each index of the tensor area constant M.
Table[X[[i,j]] + Y[[i,j]],{i,M},{j,M}]

For contracting tensors, we use the Sum [12] expression inside Table. X ik Y kj isrepresented as follows.
Table[Sum[X[[i,k]] * Y[[k,j]],{k,M}],{i,M},{j,M}]

This method has the advantage that we can use an arbitrary function deﬁned for
scalar values for tensor operations. The following Wolfram program represents∂Xij /∂xk . D is the diﬀerential function in the Wolfram language.
Table[D[X[[i,j]],x[[k]]],{i,M},{j,M},{k,M}]

Due to this advantage, the Wolfram language has been used by mathematiciansin actual research [61, 60]. However, in this method, we cannot modularize tensor
operators such as tensor multiplication by functions. Due to this restriction, we
cannot syntactically distinguish applications of diﬀerent tensor operators, suchas tensor multiplication, wedge product, and Lie derivative, in programs. Thisis because we need to represent these tensor operators combining Table and Sum
every time when we use them. Modularization by functions is also importantfor combining index notation with high-order functions. If we can pass tensor
operators to high-order functions, we can represent a formula like “Xi1 Xi2 ...Xin ”(the number of tensors multiplied depends on the parameter n) by passing theoperator for tensor multiplication to the fold function [22]. There are otherexisting works that take the same approach with the Wolfram language. NumPy’s
einsum operator [11], Diderot’s EIN operator [55], and tensor comprehensions [91]are such work. Some of them provide a syntactic construct whose appearance issimilar to mathematical formulae. However, they have the same restriction on
function modularization. This restriction comes from the requirement that users
need to specify the indices of the result tensors (e.g., “ij ” of Aij = Xik Ykj ) for
determining whether to contract a pair of identical symbolic indices.
5.2.2

Library-based Approach

Another method for dealing with tensors is using library functions prepared forhandling symbolic tensor indices. Using this method enables index notation to
be directly represented in a program as the mathematical expressions. However,in this method, it is not easy for many users to deﬁne new tensor operators bythemselves. One of the reasons is that index rules diﬀer for each operator as
mentioned in Introduction. We need to describe the index rules for each tensor
operator when deﬁning them. For example, the program below is the deﬁnitionof tensor addition in SageMath [15].
def __add__(self, other):
permutation = list(range(other._tensor.tensor_rank()))
for other_index in range(other._tensor.tensor_type()[0]):if other._con[other_index] == self._con[other_index]:
permutation[other_index] = other_index
else:
permutation[other_index] = self._con.index(other._con[other_index])
for other_index in range(other._tensor.tensor_type()[1]):if other._cov[other_index] == self._cov[other_index]:
permutation[other._tensor.tensor_type()[0] + other_index]\67

= other._tensor.tensor_type()[0] + other_index
else:
permutation[other._tensor.tensor_type()[0] + other_index]\= other._tensor.tensor_type()[0] + self._cov.index(other._cov[
other_index])
result = self.__pos__()result._tensor = result._tensor + other.permute_indices(permutation)._tensor
return result

The C++ library by Åhlander [16], ITensor [42] library in Julia, and SageMath [15] also provides the tensor operators that can handle symbolic tensor
indices in a similar way.
We propose a method for reducing these additional descriptions for handlingsymbolic tensor indices for deﬁning tensor operators. By simplifying index rules,
we can unify index rules of many tensor operators. As a result, we can set thedefault index rules and omit the descriptions of index rules from the deﬁnitionsof tensor operators.
5.2.3

Array-Oriented Programming

Array-oriented programming languages, such as APL and J, take a completely
diﬀerent approach. They do not use tensor index notation for representing tensor
calculus. Instead, they invented a new notion, function rank [21]. Function rank
speciﬁes how to map the operators to the components of tensors. When thespeciﬁed function rank is 0 for an argument matrix, the operator is mapped toeach scalar component of the matrix (Ai +Bjk ). When the speciﬁed function rank
is 1 for an argument matrix, the operator is mapped to the rows of the matrix
by regarding the matrix as a vector of vectors (Aj + Bij ). When the speciﬁed
function rank is 2 for an argument matrix, the operator is applied to the matrix
directly (Ai + Bij ).
J> (2 $ 1 2) +"1 0 (2 2 $ 10 20
11 12
21 22
31 32
41 42
J> (2 $ 1 2) +"1 1 (2 2 $ 10 20
11 22
31 42
J> (2 $ 1 2) +"1 2 (2 2 $ 10 20
11 21
32 42

30 40)

30 40)

30 40)

Function ranks allow users to apply functions deﬁned for scalar values to tensors.
A similar idea to the function rank is also imported into various programming
languages and frameworks, including Wolfram [8] and NumPy [14]. However, thefunction rank has a limitation that it does not allow to represent an expressionthat requires transposition of an argument tensor: e.g., Aij + Bji (this expression
requires the transposition of the matrix B).
We show that our simpliﬁed index rules are compatible with scalar and tensor
parameters, which is a simpliﬁed notion of function rank. Our simpliﬁed index
rules allow us to set the default index rules. The combination of the default index
rules and function ranks allows us to apply functions deﬁned for scalar values totensors using index notation.

685.2.4Diﬀerential Forms

Diﬀerential forms are important concepts in diﬀerential geometry. Diﬀerential
forms are used to describe formulae in diﬀerential geometry in a coordinate independent way. By combining the operators for diﬀerential forms, such as thewedge product and exterior derivative, we can concisely describe various formulae in diﬀerential geometry. Diﬀerential forms can be represented as tensors andformulae that we can describe using diﬀerential forms include formulae in tensor
calculus [74].
There are numerous independent works [53, 79, 15] for programming diﬀerential forms. What makes programming of diﬀerential forms diﬃcult is that
diﬀerential forms are alternating multi-linear forms (e.g., dx ∧ dy = −dy ∧ dx)
and have many representation. These works prepare special data structures forrepresenting this property of diﬀerential forms. As a result, programming fortensor calculus and diﬀerential forms have been studied separately.
Our approach represents diﬀerential forms using multi-dimensional arrays as
we do for tensors. This approach allows us to use tensor index notation fordeﬁning the operators for diﬀerential forms. We show that our simpliﬁed index
rules are useful for deﬁning the operators not only for tensors but also diﬀerential
forms. By designing the index completion rules for omitted indices properly, we
become able to concisely deﬁne the operators for the diﬀerential forms. We
introduce our method for programming of diﬀerential forms in Section 5.4.
5.2.5

Symbolic Tensor Calculus

There are two types of approaches for manipulating tensors: the ﬁrst approachaims to compute each component of tensors and represents a tensor using somedata structures such as arrays; the second approach aims to simplify formulaethat contains tensors with symbolic indices and handles a tensor as a whole as asymbol. The existing methods that we introduced so far take the ﬁrst approachand aims to compute each component of tensors. We also takes the ﬁrst approach.
There are several libraries that implement the second approach. For example,
Ricci of the Wolfram language [59] and itensor of Maxima [9, 87, 77] are suchlibraries. These libraries implement rewrite rules, such as g ij Γjkl = Γi kl whereg ij is a metric tensor and d(ω ∧ η) = dω ∧ η + (−1)p ω ∧ dη where ω is a p-form,
for simplifying formulae that contains tensors with symbolic indices.
The behaviors and deﬁnitions of tensor operators in these two approach arecompletely diﬀerent. We focuse on the ﬁrst approach.

5.3

Index Reduction Rules for Importing Tensor Index Notation

This section presents a new method for importing tensor index notation into
programming languages. Brieﬂy, it is achieved by introducing two types of parameters, scalar parameters and tensor parameters, and simple index reduction
rules. First, we introduce scalar and tensor parameters. Second, we introduce
a set of index reduction rules that is compatible with them. The combinationof scalar and tensor parameters and the proposed index reduction rules enables
us to apply user-deﬁned functions to tensors using tensor index notation. We
demonstrate our proposal using the code in the Egison programming language.
Egison has a similar syntax to the Haskell programming language.

69

def min $x $y := if x < y then x else y    (a) Deﬁnition of the min function 1
10min(1, 10) min(1, 20) min(1, 30)
1 1min(2 , 20 ) = min(2, 10) min(2, 20) min(2, 30) = 2 2
3 i
30 j
min(3, 10) min(3, 20) min(3, 30) ij
3 3


1
2
3 ij

(b) Application of the min function to the vectors with diﬀerent indices   




1
10
min(1, 10) min(1, 20) min(1, 30)
min(1, 10)min(2 , 20 ) = min(2, 10) min(2, 20) min(2, 30) = min(2, 20) =3 i
30 i
min(3, 10) min(3, 20) min(3, 30) ii
min(3, 30) i
 
1
2
3 i
(c) Application of the min function to the vectors with identical indicesFigure 5.1: Deﬁnition and application of min function
5.3.1

Scalar and Tensor Parameters

Scalar and tensor parameters are a similar notion to the function rank [21]. Whena scalar parameter obtains a tensor as an argument, the function is applied toeach component of the tensor. In contrast, when a tensor parameter obtains atensor as an argument, the function treats the tensor argument as a whole. We
call a function that takes only scalar parameters scalar function and a functionthat takes only tensor parameters tensor function. For example, “+”, “-”, “*”,and “/” should be deﬁned as scalar functions; a function for multiplying tensors
and a function for matrix determinant should be deﬁned as tensor functions.
The diﬀerence between function rank and these two types of parameters is thatfunction rank allows users to control the level of mapping, whereas scalar andtensor parameters only allow users to specify whether we map the function to eachcomponent of the tensor or not. Instead, the proposed tensor index reduction
rules combined with scalar and tensor parameters allow users to control the levelof mapping.
Figure 5.1a shows the deﬁnition of the min function as an example of a scalarfunction. The min function takes two numbers as the arguments and returns
the smaller one. “$” is prepended to the beginning of the parameters of themin function. It means the parameters of the min function are scalar parameters.
When a scalar parameter obtains a tensor as an argument, the function is applied
to each component of the tensor like tensor product as ﬁgures 5.1b and 5.1c. As
Figure 5.1c, if the indices of the tensors given as arguments are identical, theresult matrix is reduced to the vector that consists of the diagonal components.
This reduction is deﬁned in the proposed tensor index reduction rules that will
be explained in the next section. Thus the min function can handle tensors eventhough it is deﬁned without considering tensors.
Figure 5.2a shows the deﬁnition of the “.” function as an example of a tensor
function. “.” is a function for multiplying tensors. “%” is prepended to thebeginning of the parameters of the “.” function. It means the parameters of
the “.” function are tensor parameters. As with ordinary functions, when atensor is provided to a tensor parameter, the function treats the tensor argument
as a whole maintaining its indices. “.” is deﬁned as an inﬁx operator. For
deﬁning an inﬁx operator, we enclose the name of a function with parenthesis.
70def (.) %t1 %t2 := contractWith (+) (t1 * t2)(a) Deﬁnition of the “.” function i  i
1
10
10 20 302 · 20 = contractW ith(+, 20 40 60 ) = 10 + 40 + 90 = 140
330 i
30 60 90 i   
 
 
1
10
10
10
2 · 20 = contractW ith(+, 40 ) = 40
3 i
30 i
90 i
90 i
   




1
10
10 20 30
10 20 302 · 20 = contractW ith(+, 20 40 60 ) = 20 40 60
3 i
30 j
30 60 90 ij
30 60 90 ij(b) Application of the “.” function

Figure 5.2: Deﬁnition and application of “.” function
Rijkl =

∂Γijl

∂Γijk

∂x

∂xl

−
k

+ Γmjl Γimk − Γmjk Γiml(a) Formula of Riemann curvature tensor
R=Table[D[Γ[[i,j,l]],x[[k]]] - D[Γ[[i,j,k]],x[[l]]]+Sum[Γ[[m,j,l]] Γ[[i,m,k]]- Γ[[m,j,k]] Γ[[i,m,l]],{m,M}],{i,M},{j,M},{k,M},{l,M}](b) Wolfram program that represents the formula in Figure 5.3a
def R~i_j_k_l := withSymbols [m]∂/∂ Γ~i_j_l x~k - ∂/∂ Γ~i_j_k x~l + Γ~m_j_l . Γ~i_m_k - Γ~m_j_k . Γ~i_m_l(c) A program by the proposed language that represents the formula in Figure 5.3aFigure 5.3: Representations of Riemann curvature tensor formula
In Figure 5.2a, “+” and “*” are scalar functions for addition and multiplication,
respectively. contractWith is a function to contract a tensor that has pairs of asuperscript and subscript with identical symbols. Figure 5.2b shows the example
for calculating the inner product of two vectors using the “.” function. We canuse the “.” function for any kind of tensor multiplication such as tensor productand matrix multiplication as well as inner product.
Let us show another example in diﬀerential geometry. When the mathematicalexpression in Fugure 5.3a is expressed in a standard way in the Wolfram language,
it becomes a program such as the one shown in Figure 5.3b. The same expression
can be expressed in our system as shown in Figure 5.3c. Our system supports
two types of indices, both superscripts and subscripts. A subscript is represented
by “_”. A superscript is represented by “~”. A double loop consisting of the Table
and Sum expressions appears in the program in the Wolfram language, whereas
the program in our system is ﬂat, similar to the mathematical expression. This isachieved by using tensor index notation in the program. In particular, the reason
that the loop structure by the Sum expression in the Wolfram language does notappear in our expression to express Γmjk Γiml − Γmjl Γimk is that the “.” function71can handle Einstein summation notation. It is emphisized that the program (∂/∂Γijk∂ Γ~i_j_k x~l) in this example expresses ∂xlin the ﬁrst term on the right-handside. In the Wolfram language, the diﬀerential function D is applied to each tensor
component, but our diﬀerential function ∂/∂ is applied directly to the tensors.
The diﬀerential function ∂/∂ is deﬁned in a program as a scalar function likethe min function. When a tensor is provided as an argument to a scalar function,
the function is applied automatically to each component of the tensor. Therefore, when deﬁning a scalar function, it is suﬃcient to consider only a scalar as
its argument. That is, in the deﬁnition of the ∂/∂ function, the programmers
need write the program only for the case in which the argument is a scalar value.
Despite that, the program ∂/∂ Γ~i_j_k x~l returns a fourth-order tensor. Thus,
we can import tensor index notation including Einstein notation into programming if we clearly distinguish between tensor functions such as “.” and scalarfunctions such as “+” and ∂/∂ .
5.3.2

Reduction Rules for Tensors with IndicesThis section presents a whole set of index reduction rules that are compatible
with the scalar and tensor parameters. Let us consider the reduction rules only
for a single tensor, and that is enough to deﬁne the set of the index reduction
rules. This is because the reduction rules are applied only after a scalar function
is applied to tensor arguments as seen in Figure 5.1.
5.3.2.1

Multiple Identical Symbolic IndicesTensors are reduced only when they have identical symbols as their indices. First,
let us discuss the cases that tensors have identical superscripts or subscripts.
When multiple indices of the same symbol appear, our system converts itto the tensor composed of diagonal components for these indices. After thisconversion, the leftmost index symbol remains. For example, the indices “ _i_j_i” convert to “_i_j”. In our system, unbound variables are treated as symbols.
These symbols can be used as indices of tensors. In our system, a tensor isexpressed by enclosing its components with “[|” and “|]”. We express a higherorder tensor by nesting this notation, as we do for an n-dimensional array. In thisthesis, we show the evaluation result of a program in the comment that follows
the program. “--” is the inline comment delimiter of our language.
[|[|11,12,13|],[|21,22,23|],[|31,32,33|]|]_i_j -[|[|11,12,13|],[|21,22,23|],[|31,32,33|]|]_i_j[|[|11,12,13|],[|21,22,23|],[|31,32,33|]|]_i_i -- [|11,22,33|]_i[|[|[|1,2|],[|3,4|]|],[|[|5,6|],[|7,8|]|]|]_i_j_i -- [|[|1,3|],[|6,8|]|]_i_j

When three or more subscripts of the same symbol appear, our system converts
it to the tensor composed of diagonal components for all these indices.
[|[|[|1,2|],[|3,4|]|],[|[|5,6|],[|7,8|]|]|]_i_i_i -- [|1,8|]_iSuperscripts and subscripts behave symmetrically. When only superscripts areused, they behave in exactly the same manner as when only subscripts are used.
[|[|[|1,2|],[|3,4|]|],[|[|5,6|],[|7,8|]|]|]~i~j~i -- [|[|1,3|],[|6,8|]|]~i~j72

E({A, xs}) =if e(xs) = [] then{A, xs})elsif e(xs) = [{k,j}, . . . ] & p(k,xs) = p(j,xs) thenE({diag(k, j, A), remove(j, xs))
elsif e(xs) = [{k,j}, . . . ] & p(k,xs) != p(j,xs) thenE({diag(k, j, A), update(k, 0, remove(j, xs)))

Figure 5.4: Pseudo code of index reduction
5.3.2.2

Superscripts and Subscripts with Identical Symbols

Next, let us consider a case in which the same symbols are used for a superscript
and a subscript. In this case, some existing work [16] automatically contracts
the tensor using “+”. In contrast, our system just converts it to the tensor
composed of diagonal components, as in the above case. However, in this case,the summarized indices become a supersubscript, which is represented by “~_”.
[|[|11,12,13|],[|21,22,23|],[|31,32,33|]|]~i_i -- [|11,22,33|]~_i

Even when three or more indices of the same symbol appear that contain bothsuperscripts and subscripts, our system converts it to the tensor composed of
diagonal components for all these indices.
[|[|[|1,2|],[|3,4|]|],[|[|5,6|],[|7,8|]|]|]~i~i_i -- [|1,8|]~_i

The reason not to contract it immediately is to parameterize an operator forcontraction. The components of supersubscripts can be contracted by using thecontractWith function. The contractWith function receives a function to be used
for contraction as the ﬁrst argument, and a target tensor as the second argument.
This feature allows us to implement a tensor multiplication function.
contractWith (+) [|11,22,33|]~_i -- 66

In the above program, the “+” function is passed to contractWith as a preﬁx
operator. When an inﬁx operator is enclosed with parenthesis, it becomes an
preﬁx operator.
The contractWith function is deﬁned using the contract built-in function. The
contract function takes a tensor and returns the list that consists of diagonalcomponents.
contract [|11,22,33|]~_i -- [11,22,33]

5.3.2.3

Pseudo Code for Index Reduction

Figure 5.4 shows the pseudo-code of index reduction explained in the above.
E(A,xs) is a function for reducing a tensor with indices, where A is an array thatconsists of tensor components and xs is a list of indices appended to A. For
example, E(A,xs) works as follows with the tensor whose indices are “~i_j_i”.
We use 1, -1, and 0 to represent a superscript, subscript, and supersubscript,
respectively.
E({[|[|[|1,2|],[|3,4|]|],[|[|5,6|],[|7,8|]|]|],[{i,1}, {j,-1}, {i,-1}]}) ={[|[|1,3|],[|6,8|]|], [{i,0}, {j,-1}]}

73

Let us explain the helper functions used in Figure 5.4: e(xs) is a function forﬁnding pairs of identical indices from xs; diag(k, j, A) is a function for creating
the tensor that consists of diagonal components of A for the k-th and j-th order;
remove(k, xs) is a function for removing the k-th element from xs; p(k, xs) is afunction for obtaining the value of the k-th element of the assoc list xs; update(k, p, xs) is a function for updating the value of the k-th element of the assoc list
xs to p. These functions work as follows.
e([{i, 1}, {j, -1}, {i, -1}])= [{1,3}]diag(1, 2, [|[|11,12|],[|21,22|]|]) = [|11,22|]p(2, [{i, 1}, {j, -1}])= -1
remove(2, [{i, 1}, {j, -1}])= [{i, 1}]
update(2, 0, [{i, 1}, {j, -1}])= [{i, 1}, {j, 0}]

5.3.3

Implementation of Scalar and Tensor Parameters

Let us explain how to implement scalar and tensor parameters. The implementation of tensor parameters is the same with the ordinary parameters because thefunction treats the argument tensor as it is. In contrast, a function with scalarparameters is converted to a function only with tensor parameters by using thetensorMap function as follows.
\ $x $y -> ...
-- => \ %x %y ->-tensorMap (\ %x -> tensorMap (\ %y -> ...) y))-x

As the name implies, the tensorMap function applies the function of the ﬁrst argument to each component of the tensor provided as the second argument. Whenthe result of applying the function of the ﬁrst argument to each component of
the tensor provided as the second argument is a tensor with indices, it moves
those indices to the end of the tensor that is the result of evaluating the tensorMap
function.
Let us review the min function deﬁned in Figure 5.1a as an example. This min
function can handle tensors as arguments as follows.
min [|1,2,3|]_i [|10,20,30|]_j -- [|[|1,1,1|],[|2,2,2|],[|3,3,3|]|]_i_jmin [|1,2,3|]_i [|10,20,30|]_i -- [|1,2,3|]_i

Note that the tensor indices of the ﬁrst evaluated result are “_i_j”. If the tensorMap
function simply applies the function to each component of the tensor, the result of
this program is [|[|1 1 1|]_j [|2 2 2|]_j [|3 3 3|]_j|]_i. However, as explained
above, if the results of applying the function to each component of the tensor are
tensors with indices, it moves those indices to the end of the tensor that is theresult of evaluating the tensorMap function. This is the reason that the indicesof the evaluated result are “_i_j”. This mechanism enables us to directly apply
scalar functions to tensor arguments using index notation as the above example.
Next, let us review the “.” function deﬁned in Figure 5.2a as an example of atensor function. When a tensor with indices is given as an argument of a tensor
function, it is passed to the tensor function maintaining its indices. It allows us
to directly apply tensor functions to tensor arguments using index notation as in
the following example.
[|1,2,3|]~i . [|10,20,30|]_i -- 140[|1,2,3|]_i . [|10,20,30|]_j -- [|[|10,20,30|],[|20,40,60|],[|30,60,90|]|]_i_j[|1,2,3|]_i . [|10,20,30|]_i -- [|10,40,90|]_i

74


∂f
( ) ( )j
 ∂x
x
f
=
∂/∂
 ∂g
g i y
∂x


∂f
∂y 

∂g 
∂y ij

Figure 5.5: Index rule for partial derivative
Tensor parameters are rarely used compared with scalar parameters becausea tensor parameter is used only when deﬁning a function that contracts tensors.
5.3.4

Inverted Scalar Arguments

The ∂/∂ function, the derivative operator, in Figure 5.3c is a scalar function.
However, ∂/∂ is not a normal scalar function. The ∂/∂ function is a scalar function that inverts indices of the tensor given as its second argument as shown in
Figure 5.5. For example, the program (∂/∂ Γ~i_j_k x~l) returns the fourth-ordertensor with the indices “~i_j_k_l”.
To deﬁne scalar functions such as ∂/∂ , we use inverted scalar parameters. Inverted scalar parameters are represented by “*$”. A program that uses inverted
scalar parameters is transformed as follows. The flipIndices function is a primitive function for inverting the indices of a tensor provided as an argument upside
down. Supersubscripts remain as supersubscripts even if they are inverted.
def ∂/∂ $f *$x := ...
-- => def ∂/∂ %f %x := tensorMap (\ %f -> tensorMap (\ %x -> ...) (flipIndices x))-f

In the following example, we apply ∂/∂ to tensors.
∂/∂ [|(r * (sin θ)),(r * (cos θ))|]_i [|r,θ|]_j-- [|[|(sin θ),(r * (cos θ))|],[|(cos θ),(-1 * r * (sin θ))|]|]_i~j∂/∂ [|(r * (sin θ)),(r * (cos θ))|]_i [|r,θ|]_i-- [|(sin θ),(-1 * r * (sin θ))|]~_i

5.3.5

The withSymbols Expression

The withSymbols expression is syntax for generating new local symbols as the
Module [10] expression in the Wolfram language. One-character symbols that areoften used as indices of tensors such as i, j, and k are often used in another partof a program. Generating local symbols using withSymbols expressions enables us
to avoid variable conﬂicts for such symbols.
The withSymbols expression takes a list of symbols as its ﬁrst argument. Thesesymbols are valid only in the expression given in the second argument of the
withSymbols expression.
withSymbols [i] contractWith (+) ([|1,2,3|]~i * [|10,20,30|]_i) -- 60

It acts in a special way when the evaluation result of the body of the withSymbols
expression contains the symbols generated by the withSymbols expressions. In
that case, the result tensor is transposed to shift those symbols backward andremove them. In the following evaluation result, the matrix is transposed because
j is shifted backward before it removed. This mechanism is useful to handle
diﬀerential forms that will be discussed in the next section.
75

withSymbols [j] [|[|1,2|],[|3,4|]|]_j_i) -- [|[|1,3|],[|2,4|]|]_i

5.3.6

Tensor Declaration

In our system, when binding a tensor to a variable, we can specify the type ofindices in the variable name. For example, we can bind diﬀerent tensors to g__, g~~, R____, and R~___. This feature is also implemented in Maxima [9] and simpliﬁesvariable names. In Figure 5.3c, we bind a tensor to the variable with symbolic
indices R~i_j_k_l. It is automatically desugared as follows.
def R~i_j_k_l := ...
-- => def R~___ := withSymbols [i,j,k,l]-(transpose [i,j,k,l] ...)

This syntactic sugar renders a program closer to the mathematical expression.
The transpose function is a built-in function for transposing the tensor in thesecond argument as speciﬁed in the ﬁrst argument.
5.3.7

Declaring Symmetric and Antisymmetric Tensors

Symmetric and anti-symmetric tensors often appear in diﬀerential geometry.
We can use symmetry to skip descriptions and calculation of symmetric components. This section designs a syntax construct for declaring symmetry andanti-symmetry of a tensor.
There is no special notation for declaring symmetry of tensors. For example,
the symmetries of Riemann curvature tensors are declared using equations asfollows.
Rabcd = −Rbacd
Rabcd = −Rabdc
Rabcd = Rcdab
We thought that it is redundant to declare tensor symmetries using the above
equation in a program. First, we need a complicated program to determine
which parts of the tensor are symmetric from the above equations. Second, thesymmetry declaration independent of the deﬁnition of a tensor itself makes the
speciﬁcation of programming languages complex.
For these reasons, we want to deﬁne a tensor and declare its symmetries atthe same time. We found a hint in the mathematical notation for the commutator. This notation is used to represent the sum and diﬀerence between values
combining two elements enclosed by parenthesis.
[a, b] = ab − ba{a, b} = ab + ba
This notation is also used in tensor indices.
R{ab}cd = Rabcd + Rbacd
R[ab]cd = Rabcd − Rbacd
Using this notation, we can describe the ﬁrst two above symmetries of Riemanncurvature tensor as follows.
R{ab}cd = 076Rab{cd} = 0
By extending this notation, we can also describe the third symmetry.
R[(ab)(cd)] = 0
We noticed that by borrowing this notation we can merge the tensor deﬁnitionand symmetry declaration in a single expression. We show an example using thedeﬁnition of Rabcd .
Rabcd = gai Ribcd
We declare symmetries of Rabcd by adding parenthesis in the list of symbolic
indices in the left-side of equation.
R[{ab}{cd}] = gai Ribcd
We explain how we implemented this notation. We desugar the following
tensor declaration
def X{_i_j} := ...

as follows.
def X_i_j :=let tmpX_i_j := ... ingenerateTensor(\i j -> if i > j then tmpX_j_i
else
tmpX_i_j)(tensorShape tmpX_#_#)The desugared program uses the generateTensor expression. Thanks to the callby-need strategy, we do not compute all the components of tmpX. We can apply
the same method for anti-symmetric tensors.
def X[_i_j] := ...

The above tensor declaration is transformed as follows.
def X_i_j :=let tmpX_i_j := ... ingenerateTensor(\i j -> if i > j then -tmpX_j_i
else if i = j then 0
else
tmpX_i_j)(tensorShape tmpX_#_#)

Finally, we show a case that symmetry declaration reduces the description ofa program. We found this case when writing a program for actual research of
diﬀerential geometry. We deﬁne a tensor R̄abcd that possesses the same symmetry
as Riemann curvature tensor. The tensor R̄abcd is deﬁned as follows.
R̄00cd = 0, R̄0b0d = −p2 gbd , R̄0bcd = −p∇b Jcd ,R̄abcd = Rabcd − p2 Jbc Jad + p2 Jac Jbd + 2p2 Jab Jcd
This tensor is deﬁned using the generateTensor expression as follow.
def R'_i_j_k_l :=generateTensor(\is -> match is as list integer with| [#1, #1, _, _] -> 0
| [_, _, #1, #1] -> 0
| [#1, $b, #1, $d] -> -1 * p^2 * g_(b - 1)_(d - 1)77

| [$a, #1, #1, $d] ->p^2 * g_(a - 1)_(d - 1)
| [#1, $b, $c, #1] ->p^2 * g_(b - 1)_(c - 1)
| [$a, #1, $c, #1] -> -1 * p^2 * g_(a - 1)_(c - 1)
| [#1, $b, $c, $d] -> -1 * p * ∇J_(b - 1)_(c - 1)_(d - 1)
| [$a, #1, $c, $d] ->p * ∇J_(a - 1)_(c - 1)_(d - 1)
| [$a, $b, #1, $d] -> -1 * p * ∇J_(d - 1)_(a - 1)_(b - 1)
| [$a, $b, $c, #1] ->p * ∇J_(c - 1)_(a - 1)_(b - 1)
| [$a, $b, $c, $d] -> R_(a - 1)_(b - 1)_(c - 1)_(d - 1)
+ -1 * p^2 * J_(b - 1)_(c - 1) * J_(a - 1)_(d - 1)+p^2 * J_(a - 1)_(c - 1) * J_(b - 1)_(d - 1)
+ 2 * p^2 * J_(a - 1)_(b - 1) * J_(c - 1)_(d - 1))[5, 5, 5, 5]

By using our notation for declaring symmetry, we can reduce the number ofbranches in the generateTensor.
def R'{[_i_j][_k_l]} :=generateTensor(\is -> match is as list integer with| [#1, #1, _, _] -> 0
| [#1, $b, #1, $d] -> -1 * p^2 * g_(b - 1)_(d - 1)
| [#1, $b, $c, $d] -> -1 * p * ∇J_(b - 1)_(c - 1)_(d - 1)
| [$a, $b, $c, $d] -> R_(a - 1)_(b - 1)_(c - 1)_(d - 1)
+ -1 * p^2 * J_(b - 1)_(c - 1) * J_(a - 1)_(d - 1)+p^2 * J_(a - 1)_(c - 1) * J_(b - 1)_(d - 1)
+ 2 * p^2 * J_(a - 1)_(b - 1) * J_(c - 1)_(d - 1))[5, 5, 5, 5]

5.3.8

Pattern Matching for Tensor Indices

For deﬁning a tensor operator, we sometimes need to rearrange symbolic tensor
indices of the argument tensors. For example, here is a mathematical formulaethat deﬁnes the covariant derivative operator.
∂ a1 ···arT
b1 ···bk∂xc
a1 ···ar−1 da1
da2 ···arar+ Γ dc T
b1 ···bk
b1 ···bk + · · · + Γ dc T

∇c T a1 ···arb1 ···bk =− Γda1 c T a1 ···ardb2 ···bk − · · · − Γdbk c T a1 ···arb1 ···bk−1 d
The symbolic tensor indices appended to the tensor T in left-side and right-sideof the equation are diﬀerent.
In order to deﬁne such an operator, we allow to pattern-match symbolic tensor
indices of the argument tensors.
def ∇_c T~(a_1)...~(a_r)_(b_1)..._(b_k) :=∂/∂ T~(a_1)...~(a_r)_(b_1)..._(b_k) x~c+ sum (map (\i -> Γ~(a_i)_d_c .
T~(a_1)...~(a_(i-1))~d~(a_(i+1))...~(a_r)_(b_1)..._(b_k))[1..r])- sum (map (\i -> Γ~d_(b_i)_c .
T~(a_1)...~(a_r)_(b_1)..._(b_(i-1))_d_(b_(i+1))..._(b_k))[1..k])We allow to use “...” as we do in mathematical formulae. A pattern for tensor
indices that contains “...” matches the logest possible part.

5.4

Index Completion Rules for Tensors with Omitted Indices

By designing the index completion rules for omitted indices properly, we can
extend the proposed method explained so far to express a calculation handling78the diﬀerential forms.
5.4.1

Representation of Diﬀerential Forms

This section explains how we represent diﬀerential forms in programs. In our
method, n-forms are represented by rank-n tensors. Let us show examples in
3-dimensional
space.
One-forms
dx, dy, and dz are represented as() ( Euclidean)()
1 0 0 , 0 1 0 , and 0 0 1 , respectively. Two-forms dx∧dy and dz ∧dx(0 0 0)(0 1 0)are represented as 0 0 0 and 0 0 0 , respectively.
100000
In mathematics, n-forms can be regarded as a function that takes n tangent
vectors and returns a value. This return value is the result of multiplying thetensor that represents the diﬀerential form and the tangent vectors. Especially,
the result of applying the tangent vector v to the one-form ω is inner product:
ω(v) = ⌊ω⌋i v iwhere ⌊ω⌋ is the tensor representation of ω. Generally, the result of applying
the tangent vectors v1 , · · · , vn to the n-form ω is determined by the following
formula.
()
1 ∑ω(v1 , · · · , vn ) =sgn(σ)⌊ω⌋iσ1 ···iσn (v1 )i1 · · · (vn )in
n!
σ∈Sn

1
We call n!

∑sgn(σ)⌊ω⌋iσ1 ···iσn the normal representation of the diﬀerential formσ∈Snω. We use the antisymmetrize function for calculating the normal representation of
diﬀerential forms. For example, the normal representation of dx∧dy is calculated
as follows.
antisymmetrize [| [| 0, 1, 0 |], [| 0, 0, 0 |], [| 0, 0, 0 |] |]-- [| [| 0, 1 / 2, 0 |], [| -1 / 2, 0, 0 |], [| 0, 0, 0 |] |]5.4.2

Index Completion Rules

We distinguish diﬀerential forms from the other tensors in programs by omitting indices. In mathematics, we denote a p-form by appending only (n − p)indices to an n-th order tensor. For example, the third order tensor ω i j denotes amatrix-valued one-form. We can use this notation for representing tensor-valued
diﬀerential forms in programs.
This section shows the design of index completion rules for omitted indicesthat allows us to concisely deﬁne the operators for diﬀerential forms. Let A and B
be scalar-valued 2-forms. For general scalar functions, we complement the same
indices to each argument tensor as follows.
A + B -- => A_t1_t2 + B_t1_t2

We know that the above completion is natural from the following example.
⌊dx ∧ dy + dy ∧ dz⌋t1 t2 = ⌊dx ∧ dy⌋t1 t2 + ⌊dy ∧ dz⌋t1 t2
In most of the cases, if we complement indices as above, we can represent
the operation for diﬀerential forms. However, this completion is not suitable forfunctions specially deﬁned for diﬀerential forms such as the wedge product andexterior derivative. In the case of the wedge product, we would like to append
the diﬀerent indices to each argument as follows.
79A ∧ B -- => A_t1_t2 . B_t3_t4

For example, the following formula holds in four-dimensional Euclidean space.
⌊(dx ∧ dy) ∧ (dz ∧ dw)⌋t1 t2 t3 t4 = ⌊dx ∧ dy⌋t1 t2 ⌊dz ∧ dw⌋t3 t4
We introduce the “!” operator for this purpose. If the “!” operator is prepended
to function application, the omitted indices are complemented by the lattermethod. With this method, the function for calculating the wedge product isdeﬁned in one line as follows.
def (∧) %A %B := A !. B

We can also deﬁne the exterior derivative in one line as follows.
def d %A := !(flip ∂/∂) coord A

The flip function swaps the arguments of a two-argument function. It is used
to transpose the result. We set the symbols for representing the coordinates tocoord. We can use the wedge product and exterior derivative deﬁned above as
follows.
def coord := [| x, y, z |]d x -- [| 1, 0, 0 |]d x ∧ d y -- [| [| 0, 1, 0 |], [| 0, 0, 0 |], [| 0, 0, 0 |] |]d z ∧ d x -- [| [| 0, 0, 0 |], [| 0, 0, 0 |], [| 1, 0, 0 |] |]Next, we deﬁne Hodge star operator. We use the following mathematicalformula for Hodge star operator [73].
√∗A = det |g| · ϵi1 ...in · Aj1 ...jk · g i1 j1 · · · g ik jk · eik+1 ∧ ... ∧ ein(5.1)
We can directly translate the above formula as follows.
def hodge %A :=let k := dfOrder A in
withSymbols [i, j](sqrt (abs (det g_#_#))) * (foldl (.) ((ϵ N k)_(i_1)..._(i_N) . A..._(j_1)..._(j_k))(map (\t -> g~(i_t)~(j_t)) [1..k]))In the above program, the dfOrder function returns p when it obtains an p-form;
the det function returns the determinant of the argument matrix; ϵ is the LeviCivita symbols; “#” used in the indices as g_#_# represents a dummy symbol. All
instances of “#” are treated as diﬀerent symbols. In a program that deals withhigh-order tensors, the number of symbols used for indices increases. A dummy
symbol suppresses that. This mechanism makes it easier to distinguish indices,
thereby also improves the readability of the program.

5.5

Demonstration

This section shows that the proposed system is practical by showing a programof a certain size. By modifying the programs in this section, we can use ourlanguage for actual research. Figure 5.6b shows the mathematical formulae of
Christoﬀel symbols and curvature form. These formulae appear in the 4th, 5th,and 8th programs in Figure 5.6a. We can see the sample programs that use thefunctions deﬁned above in Egison Mathematics Notebook [31].
80(a) A program for calculating Riemann curvature tensor of S 2 using the formula ofcurvature form∂gkj
1 ∂gij∂gikΓijk = ( k +
−
)
j
2 ∂x
∂x
∂xi

Γijk = g im Γmjk

Ωij = dω ij + ω ik ∧ ω kj(b) Mathematical formulae used in the above program

Figure 5.6: Program for diﬀerential geometry in our language

5.6

Evaluation

In this section, we evaluate how simple our deﬁnitions of tensor operators areby comparing to the other works. Table 5.1 shows the numbers of lines fordeﬁning tensor operators in ITensor [42], Karczmarczuk’s Haskell library [53],SageMath [15], and our work. We chose these libraries for comparison because
their deﬁnitions of tensor operators are compact compared to the other existingwork. To make the comparison fair, we do not count the number of lines forerror handling. The other approaches require additional descriptions for error
handling because they do not relax the index rules like us.
The deﬁnitions of the tensor operators by our work is shortest among theexisting work. The reason why our deﬁnitions are short is that our simpliﬁed
index rules allow us to remove the descriptions of index rules from the deﬁnitionsof tensor operators. Especially, the numbers of lines required to deﬁne tensor

81Number of lines
addition
multiplication
derivative
wedge productexterior derivative
hodge star

ITensor (Julia)
5
17
n/a
n/a
n/a
n/a

Karczmarczuk
n/a
n/a
n/a
8
9
8

SageMath
27
27
n/a
9
8
14

Egison0
1
0
1
1
5Table 5.1: The number of lines for deﬁning operators for tensors and diﬀerential
forms
addition and derivative operators are zero. It is achieved by deﬁning the additionand derivative operators as scalar functions. The deﬁnition of tensor addition by
ITensor is also short.
function (A::ITensor + B::ITensor)
C = copy(A)C .+= B
return C
end

This is because the broadcast operation, which speciﬁes how to map the operation
to the components of tensors, is deﬁned in ITensor. When the dot mark isprepended to an operator like the line 3 of the above deﬁnition, the operator
is broadcasted. In our approach, scalar functions are automatically mapped toeach tensor component without any actions by users. The language-level supportof scalar parameters allows us to deﬁne the arithmetic operators for tensor evenshorter.
The deﬁnitions of the operators for diﬀerential forms by our work is also
shortest among the existing work. This is because the reuse of our simpliﬁed
index rules releases us from describing complex algebraic rules for diﬀerential
forms. Especially, we can deﬁne the wedge product and exterior derivative in
one line. It is an important discovery that we can reuse symbolic index rules
for tensors for deﬁning operators for diﬀerential forms. In addition, representing
diﬀerential forms using tensors enables us to deﬁne operators for diﬀerential forms
using index notation. It allows us to translate the formula of the hodge operator
directly to a program as shown in Section 5.4.2.
Finally, let us note that the derivative operator ∂/∂ for tensors is supported
only by our proposal. For this purpose we discussed to ﬂip the superscript andsubscript in programs to allow a vector as the second argument of the derivative
operator as explained in Section 5.3.4. The derivative operator that supports
symbolic tensor indices widen the range of formulae we can describe in programs
using index notation. For example, users cannot describe a program that calculate
Riemann curvature tensors without the derivative operator using index notation
as shown in Figure 5.3c. In the existing library-based approaches, the function
for calculating Riemann curvature tensors is provided as a library function.

5.7

Conclusion

In this chapter, we showed that we can import tensor index notation into a programming language by introducing a set of symbolic index reduction rules thatis compatible with scalar and tensor parameters. The proposed method allows
users to deﬁne functions that handle symbolic tensor indices without additional82

descriptions for handling these symbolic tensor indices. We demonstrated the
proposed method by showing our proof-of-concept programming language Egison. The proposed method can be implemented also in the other programming
languages. It is an interesting research topic to think about how to incorporate the proposed method into existing programming languages. For example,
we think it is possible to introduce the concept of scalar and tensor parameters
using a static type system [68]. In a language with a static type system, whether
the parameter of a function is a scalar or tensor parameter can be speciﬁed when
specifying the type of the function.
In particular, it is of substantial signiﬁcance to incorporate the proposed
method into programming languages such as Formura [64] and Diderot [55] thathave a compiler to generate code for executing tensor calculation eﬃciently. For
example, incorporating the proposed method into Formura would enable us todescribe physical simulation using not only the Cartesian coordinate system but
also more general coordinate systems such as the polar and spherical coordinate
systems in simple programs.

83

Chapter 6
Conclusion
6.1

Summary

In this thesis, we have proposed several syntax constructs and facilities of programming languages. We have demonstrated that these syntax constructs andfacilities widen the range of algorithms that we can describe concisely. Speciﬁcally, the contributions of the thesis are as follows.
• In Chapter 2, we presented the design of our pattern-match system for
non-free data types. We proposed three criteria that must be fulﬁlled forpractical pattern matching for non-free data types: (1) eﬃciency of the
backtracking algorithm for non-linear patterns, (2) user-customizability ofpattern-match algorithm, and (3) polymorphism in patterns. We showed
how our language design naturally arises from our criteria of practical pattern matching.
• In Chapter 3, we advocated a new programming paradigm called patternmatch-oriented programming. We introduced many programming techniques that replace explicit recursions with an intuitive pattern by conﬁning
recursions inside patterns. We also proposed several non-standard patternconstructs, such as not-patterns, loop patterns, and sequential patterns,
derived from our pattern-match facility. We classiﬁed these techniques as
pattern-match-oriented programming design patterns.
• In Chapter 4, we presented the implementation of a Haskell library thatembed our pattern-match system into Haskell. We proposed a method fortransforming Egison pattern-match expressions to an equivalent Haskell
program that uses a backtracking monad. We also designed a set of typing
rules for Egison pattern matching. We showed benchmark results that
conﬁrm our library can be used in practical situations.
• In Chapter 5, we discussed a method for importing notations from tensor
calculus into programming languages. We proposed a set of index reduction and completion rules that allows us to deﬁne many tensor operators
without descriptions for handling symbolic tensor indices. In addition tothat, we presented a new syntax construct for declaring symmetries andanti-symmetries of a tensor. We represented many formulae in diﬀerential
geometry by a program whose appearance is very close to the formulae.

6.2

The Three Steps for Creating New Syntax Constructs

While developing new features of programming languages, we become aware of
the following steps for creating new syntax constructs.
84

Step 1. Discover a gap between our recognition and description of an algorithm.
Step 2. Design new syntax for describing algorithms in a form close to our recognition.
Step 3. Design a method for executing the new syntax.
In this section, we categorize our contributions in each step. It gives us insightfor answering research questions about notations: “Is there a general way to ﬁnd
a new notation?”, “Is there a formal method for measuring the superiority ofmultiple notations?”
6.2.1

Step 1: Discover a Gap between Our Recognition and Description of an Algorithm

We have noticed the cognitive gaps four times for pattern matching.
1. When we deﬁned the mapWithBothSides function, we noticed the importanceof pattern matching with multiple results (Section 1.2).
2. When we tried to describe pattern matching for a multiset, we noticed theimportance of non-linear patterns, user-customizability of pattern-matchalgorithms, and polymorphic patterns (Section 2.2, 2.3).
3. When we deﬁned the comb function, we got an idea of loop patterns (Section 3.2.6).
4. When we deﬁned the uniq function, we got an idea of sequential patterns(Section 3.2.7).
After we noticed the importance of pattern matching with multiple results, weconsequently noticed that pattern matching with multiple results is useful for
pattern matching non-free data types. Then, we noticed the importance of nonlinear patterns, user-customizability of pattern-match algorithms, and polymorphic patterns. When redeﬁning various list functions using the pattern-match
facility that satisﬁes all the above features, we got ideas of loop patterns andsequential patterns.
We have noticed the gaps also 4 times for tensor calculus.
5. When we tried to deﬁne tensor multiplication that supports index notation,
we found that the deﬁnition is not easy (Section 1.3, 5.3).
6. When we tried to write down a formula that contains diﬀerential forms, wefound it diﬃcult (Section 5.4).
7. When we tried to declare symmetries of a tensor in a program, we noticed
that we had no concise notation for this purpose (Section 5.3.7).
8. When we deﬁned the covariant derivative operator, we noticed our description verbose (Section 5.3.8).
We noticed these gaps while we tried to write down formulae in a textbook of
diﬀerential geometry as many as possible. All these gaps derive from the factthat we cannot directly write down formulae in programs.
Writing many programs for the ﬁelds in which many researchers of programming languages still do not have an interest is an easy way to ﬁnd the cognitive
gaps. In mathematics, there are still many calculations that we have never tried
to compute using computers.
85

6.2.2

Step 2: Design New Syntax for Describing Algorithms in a
Form Close to Our Recognition

We have designed several new syntax constructs for pattern matching.
1. We designed the matchAll expression that collects all the pattern-match
results. It enables users to handle multiple pattern-match results (Section 2.3.1).
2. We designed the value pattern to represent non-linear patterns (Section 2.3.2).
3. We designed the pattern-match expressions to take an additional argument
matcher. This additional argument is necessary for polymorphic patterns(Section 2.3.3).
4. We designed the matcher expression that enables users to customize a patternmatch algorithm (Section 2.5).
5. We designed the loop pattern and sequential pattern (Section 3.2.6, 3.2.7).
Most of the above syntax arose naturally from the reasons for the gaps that
we analyzed when we noticed the gaps. The patter-match expressions matchAll
and match are designed by extending the existing pattern-match expressions foralgebraic data types. On the other hand, we made much eﬀort to design syntax
for deﬁning matchers. This is because the semantics of pattern-match expressions
are strongly connected to the syntax for deﬁning matchers.
We have designed several new syntax constructs for tensor calculus.
6. We designed how to describe formulae that uses tensor index notation (Section 5.3.8).
7. We designed syntax for declaring tensor symmetries (Section 5.3.7).
For designing how to describe index notation in programming, we have not mademuch eﬀort because we can just import notations from mathematics. On theother hand, it took a lot of time to get an idea for declaring tensor symmetries.
As mentioned in Section 5.3.7, we got an idea of the syntax from the mathematicalnotation for commutators T[ij] = Tij − Tji .
When we designed the syntax for declaring tensor symmetries, we got theidea that a good notation eﬃciently embeds algorithm information in a parsetree. The simplest method for declaring tensor symmetries is describing a list ofsymmetric indices. In contrast, the proposed notation embed this list into a tree
by assuming symmetric indices always adjoin and enclosing them by parenthesis.
We can get a new good notation by ﬁnding a special case that we can convert alist in a parse tree that can be converted to a tree.
In fact, pattern matching is also such an example. In general, functions havemultiple arguments and multiple return values. In functional programming, we
use a list of the let expressions or do-notation that takes a list of input/output
operations to represent sequential applications of functions that have multiple
arguments and multiple return values. However, many functions that we deal
with take multiple arguments and have a single return value. Thanks to that,
we can describe sequential function applications in a tree form like f (g(x), h(y))
instead of a list of the let expressions. On the contrary, we can also describe nested
applications of the functions that take a single argument and return multiple
values in a tree form. Pattern matching is a syntax construct for representing
this kind of nested function application. For example, the pattern $x :: $y :: _86

can be regarded as a nested application of the cons function (::) that has a single
argument and two return values. Sweet Egison reverts a pattern in a tree form
to a list of input/output operations in a do-expression.
6.2.3

Step 3: Design a Method for Executing New Syntax

We have designed the executing methods for pattern matching as follows.
1. We designed an internal pattern-match algorithm of the proposed patternmatch system as reduction of matching states (Section 2.4).
2. We developed a method for converting the proposed pattern-match expressions to programs that use backtracking monads (Section 4.3).
When we designed the execution methods, we tried to make the semantics ofthe language as natural as possible. We feel the semantics of a language naturalwhen it is general and simple.
To make the semantics of our language general we designed our pattern-match
facility for general non-free data types. We noticed the importance of usercustomizable non-linear pattern matching with multiple results when writing a
program that deals with lists and multisets. However, we do not limit our patternmatch facility to the collection data types.
To make the semantics of our language simple we chose backtracking as thebase algorithm for pattern matching. The backtracking algorithm is the most eﬃcient and simplest for handling non-linear pattern matching with multiple results.
Not only that, the backtracking algorithm does not require users complicated descriptions for deﬁning their own patterns.
We have designed the executing methods for tensor calculus as follows.
4. We designed a set of index reduction rules that enables us to describe
function application using index notation (Section 5.3).
5. We designed an execution method of programs that declare a tensor using
index notation (Section 5.3.6).
6. We designed an execution method of programs that deﬁne a tensor operator
using index notation (Section 5.3.8).
7. We designed an execution method of programs that declare symmetries oftensors (Section 5.3.7).
8. We designed index completion rules that enables us to describe formulaethat contain diﬀerential forms (Section 5.4).
Most of the notations for tensor calculus become executable by giving a meaning
to undeﬁned programs. In mathematics, symbolic index rules are deﬁned foreach tensor operator. We simpliﬁed the symbolic index rules so that we canapply them for all the operators.

6.3

Contributions

In this thesis, we have proposed new programming facilities and styles that widen
the range of algorithms that we can describe intuitively. To this end, we foundalgorithms whose description is more complicated than necessary, analyzed thereasons, and designed new programming facilities. Utilizing these new programming facilities, we wrote programs in new programming styles, found algorithms
87

whose description is still complicated, and extend our new programming facilities.
We conducted such research on two independent themes, pattern matching fornon-free data types and importing notations from tensor calculus. We explained
our work for pattern matching in Chapters 2, 3, and 4, and for tensor calculus in
Chapter 5.

6.4

Future Work

This section catalogs and discuss the next goals and research questions we foundwhile developing our proposals.
6.4.1

Increase Application of Pattern-Match-Oriented Programming

Development of new application examples of Egison is important to convince a lotof programmers that Egison is useful for practical use and to make them to think
about new application examples. Implementing various algorithms in Egison
helps us to clarify what pattern-match-oriented programming is and invent newfeatures of programming languages. We have been implementing SAT algorithms
as a representative of algorithms. We explained our implementation of the DavisPutnam algorithm in Section 3.4.1. We also implemented the CDCL algorithm
that has been the basis of the latest SAT algorithm. If we try to implement thestate-of-art algorithm, we want to manage memory usage and use our patternmatch facility in system programming languages such as Rust.
Applying our pattern-match facility to query databases is another promising
application. As a ﬁrst step, we are planning to implement software that translates
our pattern-match expressions to the existing query languages.
6.4.2

Implement the Proposed Pattern Matching in Other Programming Languages

First, we plan to implement our pattern-match facility as a GHC plugin and GHC
extension. We have implemented our pattern-match facility as a Haskell library
in Sweet Egison introduced in Chapter 4. However, this library has limitations
due to meta-programming capability of Haskell. To begin with, quasi-quoting
each match clause is redundant. Not only that, we cannot nest pattern-match
expressions because we cannot nest quasi-quotes. We may avoid these problems
by implementing our pattern-match facility as a GHC plugin and GHC extension.
As a ﬁrst step, we are surveying to conﬁrm that we can implement our patternmatch facility as a GHC plugin.
Second, we plan to embed Egison pattern matching into Rust, a system programming language with strong meta-programming capability. Embedding ourpattern-match facility into a system programming language that allows manual
memory management is an interesting research topic. We found several researchquestions.
• Can we implement more eﬃcient pattern-match algorithms by manually
managing memory usage?
• How to design a pattern-match system limiting the capability of our patternmatch facility for avoiding ineﬃcient memory copies?

886.4.3

Proof Writing Language

In the future, mathematical proofs will be written and checked on computers. It
is currently not common among mathematics researchers because we cannot yet
describe proofs on computers as concisely as in natural languages and formulae.
It is known as Curry-Howard correspondence; there is a strong relationship between computer programs and mathematical proofs. The syntax that is useful fora concise description of programs is also useful for a concise description of proofs.
Pattern matching is also an important syntactic construct for intuitive descriptions of proofs. A vast eﬀort has been devoted to introducing pattern matching
to theorem proving systems [28, 43, 27]. Most modern theorem provers such as
Coq [83], Agda [82], and Lean [29] have a pattern-match facility for algebraic
data types. Applying the pattern-match facility for non-free data types proposedin this thesis can make the descriptions of proofs more concise. With these ideas
in mind, we are designing a proof writing language with our pattern-match facility [36].
6.4.4Pattern Matching for Wider Range of Data Types

We focused on the data abstraction for non-free data types in this thesis. However, there must be more data types waiting to be abstracted. There are still
data types we cannot apply pattern matching. For example, it is diﬃcult to
describe intuitive patterns for multi-dimensional data, such as two-dimensional
arrays. This is because we cannot embed patterns for these data types into a
syntax tree.
6.4.5

Import More Notations from Mathematics

In this thesis, we have imported notations in tensor calculus into programming.
However, there are still many notations in mathematics that are useful but not
yet introduced into programming. Importing these notations is not only useful
but also leads us to deepen our understanding on mathematical notations.
6.4.6

Expressive Complexity

There are no established methods for comparing the readability and writabilityof multiple programs written in diﬀerent styles. The lack of such a method is
considered one of the reasons why the development of new notations is not very
active in programming languages. We always found diﬃculty in evaluating thefeatures of programming languages proposed in this thesis. We believe we haveprovided reasonable evidence to show our proposals are useful, but these pieces ofevidence are subjective and not mathematically formal. With these ideas in mind,
we are considering a method for measuring the readability and writability of aprogram. We call readability and writability of a program expressive complexity
inspired by the computational complexity of algorithms. This section introduces
the current ideas.
Let A and B be programs we want to compare. We assume that A and B
implement the same algorithm and can be compiled to the same machine code.
The reason of this assumption is that it is nonsense to compare the expressive
complexities of programs that implement diﬀerent algorithms even if they havethe same input and output.
First, we investigated whether we can use the number of tokens, variables, andlocal variables, or the depth of a parse tree for expressive complexity. However, we

89found it diﬃcult because they are a constant for each program and the diﬀerence
between these constants is unconvincing to measure the readability of programs.
Currently, we are investigating conversions between A and B. In general, thecomplexity of the conversion from A to B and B to A is not equal. For example,
let A be a pattern-match-oriented style program and B be a program that uses
backtracking monads. In this case, the conversion A from B is relatively easierthan B to A. One reason for this asymmetry is that we can convert all thepattern-match expressions to programs that use backtracking monads, but the
opposite is not true. We are investigating how we can utilize this asymmetry forcalculating expressive complexity.

90References[1] Attributes::attnf - Wolfram Language Documentation. http://reference.
wolfram.com/language/ref/message/Attributes/attnf.html. [Online;
accessed 14-June-2018].
[2] Introduction to Patterns - Wolfram Language Documentation. http://
reference.wolfram.com/language/tutorial/Introduction-Patterns.
html. [Online; accessed 14-June-2018].
[3] Orderless - Wolfram Language Documentation.
http://reference.
wolfram.com/language/ref/Orderless.html. [Online; accessed 14-June2018].
[4] PAKCS. https://www.informatik.uni-kiel.de/~pakcs/. [Online; accessed 14-June-2018].
[5] ViewPatterns - GHC.
https://ghc.haskell.org/trac/ghc/wiki/
ViewPatterns, 2015. [Online; accessed 30-Jan-2020].
[6] The Neo4j Manual v2.3.3. https://neo4j.com/docs/stable/index.html,
2016. [Online; accessed 30-Jan-2020].
[7] XML Path Language (XPath) 3.1.
https://www.w3.org/TR/2017/
REC-xpath-31-20170321, 2017. [Online; accessed 30-Jan-2020].
[8] Listable - Wolfram Language Documentation. http://reference.wolfram.
com/language/ref/Listable.html, 2020. [Online; accessed 30-Jan-2020].
[9] Maxima - a Computer Algebra System. http://maxima.sourceforge.
net/, 2020. [Online; accessed 30-Jan-2020].
[10] Module - Wolfram Language Documentation. http://reference.wolfram.
com/language/ref/Module.html, 2020. [Online; accessed 30-Jan-2020].
[11] NumPy. http://www.numpy.org/, 2020. [Online; accessed 30-Jan-2020].
[12] Sum - Wolfram Language Documentation. http://reference.wolfram.
com/language/ref/Sum.html, 2020.
[13] Table - Wolfram Language Documentation. http://reference.wolfram.
com/language/ref/Table.html, 2020.
[14] Universal functions (ufunc) — NumPy v1.16 Manual. https://docs.
scipy.org/doc/numpy/reference/ufuncs.html, 2020. [Online; accessed
30-Jan-2020].
[15] SageMath - Open-Source Mathematical Software System. https://www.
sagemath.org/, 2021. Accessed: 11-March-2021.
91

[16] Krister Åhlander. Einstein summation for multidimensional arrays. Computers & Mathematics with Applications, 44(8-9):1007–1017, 2002.
[17] Sergio Antoy. Constructor-Based Conditional Narrowing. In Proceedings ofthe 3rd International ACM SIGPLAN Conference on Principles and Practiceof Declarative Programming, Florence, Italy, PPDP, pages 199–206. ACM,
2001.
[18] Sergio Antoy. Programming with narrowing: A tutorial. Journal of Symbolic
Computation, 45(5):501–522, 2010.
[19] John W. Backus. The history of FORTRAN I, II and III. IEEE Ann. Hist.
Comput., 1(1):21–37, 1979.
[20] John W. Backus, Friedrich L. Bauer, Julien Green, C. Katz, John McCarthy,
Alan J. Perlis, Heinz Rutishauser, Klaus Samelson, Bernard Vauquois,
Joseph Henry Wegstein, Adriaan van Wijngaarden, and Michael Woodger.
Report on the algorithmic language ALGOL 60. Commun. ACM, 3(5):299–
314, 1960.
[21] Robert Bernecky. An introduction to function rank. In Leroy J. Dickey and
Lynne C. Shaw, editors, Proceedings of the international conference on APL,
APL 1988, Sydney, Australia, February 1-5, 1988, pages 39–43. ACM, 1988.
[22] Richard S. Bird and Philip Wadler. Introduction to functional programming.
Prentice Hall International series in computer science. Prentice Hall, 1988.
[23] Bernd Braßel, Michael Hanus, Björn Peemöller, and Fabian Reck. Kics2: A
new compiler from curry to haskell. In Herbert Kuchen, editor, Functionaland Constraint Logic Programming - 20th International Workshop, WFLP
2011, Odense, Denmark, July 19th, Proceedings, volume 6816 of Lecture
Notes in Computer Science, pages 1–18. Springer, 2011.
[24] Rod M. Burstall. Proving Properties of Programs by Structural Induction.
The Computer Journal, 12(1):41–48, 1969.
[25] Rod M. Burstall, David B. MacQueen, and Donald Sannella. HOPE: anexperimental applicative language. In Proceedings of the 1980 ACM Conference on LISP and Functional Programming, Stanford, California, UnitedStates, LFP, pages 136–143. ACM, 1980.
[26] Donald D. Chamberlin and Raymond F. Boyce. SEQUEL: A Structured
English Query Language. In Proceedings of the 1974 ACM SIGFIDET (now
SIGMOD) Workshop on Data Description, Access and Control, Ann Arbor,
Michigan, United States, SIGFIDET, pages 249–264. ACM, 1974.
[27] Jesper Cockx. Dependent Pattern Matching and Proof-Relevant Uniﬁcation.
PhD thesis, Katholieke Universiteit Leuven, Belgium, 2017.
[28] Thierry Coquand. Pattern matching with dependent types. In Informal
proceedings of Logical Frameworks, volume 92, pages 66–79. Citeseer, 1992.
[29] Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris Van Doorn, andJakob von Raumer. The lean theorem prover (system description). In International Conference on Automated Deduction, pages 378–388. Springer,
2015.
92

[30] Satoshi Egi. The Egison Programming Language. http://www.egison.
org/, 2011. [Online; accessed 14-June-2018].
[31] Satoshi Egi. Egison Mathematics Notebook. http://www.egison.org/
math/, 2017. [Online; accessed 14-June-2018].
[32] Satoshi Egi. Scalar and Tensor Parameters for Importing Tensor Index Notation including Einstein Summation Notation. In Proceedings of the 18th
Scheme and Functional Programming Workshop, Oxford, United Kingdom,
Co-located with ICFP, 2017.
[33] Satoshi Egi. Loop Patterns: Extension of Kleene Star Operator for More
Expressive Pattern Matching against Arbitrary Data Structures. In Proceedings of the 19th Scheme and Functional Programming Workshop, SaintLouis, Missouri, United States, Co-located with ICFP, 2018.
[34] Satoshi Egi. Scheme Macros for Non-linear Pattern Matching with Backtracking for Non-free Data Types. In Proceedings of the 20th Scheme
and Functional Programming Workshop, Berlin, Germany, Co-located with
ICFP, 2019.
[35] Satoshi Egi. egison/backtracking: Backtracking Monad. https://hackage.
haskell.org/package/backtracking, 2020. [Online; accessed 10-Oct2021].
[36] Satoshi Egi. Pattern-match-oriented proof writing language. In Ademar
Aguiar, Shigeru Chiba, and Elisa Gonzalez Boix, editors, Programming’20:
4th International Conference on the Art, Science, and Engineering of Programming, Porto, Portugal, March 23-26, 2020, pages 223–224. ACM, 2020.
[37] Satoshi Egi, Yoshiaki Maeda, and Steven Rosenberg.
groups of circle bundles over symplectic manifolds.
arXiv:2011.01800, 2020.

Diﬀeomorphism
arXiv preprint[38] Satoshi Egi and Yuichi Nishiwaki. Non-linear pattern matching with backtracking for non-free data types. In Proceedings of APLAS 2018 - Asian Symposium on Programming Languages and Systems, Wellington, New Zealand,
volume 11275 of LNCS, pages 3–23. Springer, 2018.
[39] Martin Erwig. Active patterns. In Proceedings of the 8th International Workshop on Implementation of Functional Languages (IFL 1996), Bad Godesberg, Germany, volume 1268 of LNCS, pages 21–40. Springer, 1996.
[40] Martin Erwig. Functional programming with graphs. In Simon L. Peyton Jones, Mads Tofte, and A. Michael Berman, editors, Proceedings of the1997 ACM SIGPLAN International Conference on Functional Programming(ICFP ’97), Amsterdam, The Netherlands, June 9-11, 1997, pages 52–65.
ACM, 1997.
[41] Sebastian Fischer, Oleg Kiselyov, and Chung-chieh Shan. Purely functional
lazy non-deterministic programming. In Graham Hutton and Andrew P.
Tolmach, editors, Proceeding of the 14th ACM SIGPLAN international conference on Functional programming, ICFP 2009, Edinburgh, Scotland, UK,
August 31 - September 2, 2009, pages 11–22. ACM, 2009.
[42] Matthew Fishman, Steven R. White, and E. Miles Stoudenmire. The ITensor
software library for tensor network calculations, 2020.
93

[43] Healfdene Goguen, Conor McBride, and James McKinna. Eliminating dependent pattern matching. In Algebra, Meaning, and Computation, pages
521–540. Springer, 2006.
[44] Michael Hanus. Multi-paradigm declarative languages. In Proceedings of the
23rd International Conference on Logic Programming (ICLP 2007), Porto,
Portugal, volume 4670 of LNCS, pages 45–75. Springer, 2007.
[45] Michael Hanus, Herbert Kuchen, and Juan Jose Moreno-Navarro. Curry: A
Truly Functional Logic Language. In Proceedings of ILPS’95 Workshop on
Visions for the Future of Logic Programmming, Portland, Oregon, UnitedStates, pages 95–107, 1995.
[46] John Harrison. Handbook of Practical Logic and Automated Reasoning. Cambridge University Press, 2009.
[47] Richard Hartley and Andrew Zisserman. Multiple view geometry in computer
vision. Cambridge university press, 2003.
[48] Paul Hudak, John Hughes, Simon L. Peyton Jones, and Philip Wadler. A
history of Haskell: being lazy with class. In Proceedings of the 3rd ACM
SIGPLAN History of Programming Languages Conference, San Diego, California, United States, HOPL, pages 1–55. ACM, 2007.
[49] Thomas J. R. Hughes. The Finite Element Method: Linear Static and Dynamic Finite Element Analysis. Dover Civil and Mechanical Engineering.
Dover, 2000.
[50] Yuwang Ji, Qiang Wang, Xuan Li, and Jie Liu. A survey on tensor techniques
and applications in machine learning. IEEE Access, 7:162950–162990, 2019.
[51] Simon Peyton Jones, Geoﬀrey Washburn, and Stephanie Weirich. Wobbly
Types: Type Inference for Generalised Algebraic Data Types. Technicalreport, Technical Report MS-CIS-05-26, Univ. of Pennsylvania, 2004.
[52] Guy L. Steele Jr. and Richard P. Gabriel. The evolution of lisp. In John
A. N. Lee and Jean E. Sammet, editors, History of Programming Languages
Conference (HOPL-II), Preprints, Cambridge, Massachusetts, USA, April
20-23, 1993, pages 231–270. ACM, 1993.
[53] Jerzy Karczmarczuk. Functional coding of diﬀerential forms. In Scottish
Workshop on Functional Programming, 1999.
[54] Akira Kawata. egison/typed-egison: Typed Egison. https://github.com/
egison/typed-egison, 2018. [Online; accessed 10-Oct-2019].
[55] Gordon L. Kindlmann, Charisee Chiw, Nicholas Seltzer, Lamont Samuels,
and John H. Reppy. Diderot: a domain-speciﬁc language for portable parallel scientiﬁc visualization and image analysis. IEEE Trans. Vis. Comput.
Graph., 22(1):867–876, 2016.
[56] Mayuko Kori and Satoshi Egi. egison/egison-haskell: Template Haskell Implementation of Egison Pattern Matching. https://github.com/egison/
egison-haskell, 2019. [Online; accessed 21-Feb-2019].
[57] Anna V. Korolkova, Dmitry S. Kulyabov, and Leonid A. Sevastyanov. Tensor computations in computer algebra systems. Program. Comput. Softw.,
39(3):135–142, 2013.
94

[58] Manuel Krebber. Non-linear associative-commutative many-to-one patternmatching with sequence variables. CoRR, abs/1705.00907, 2017.
[59] John M Lee. Ricci: Mathematica package for doing tensor calculations in differential geometry. https://sites.math.washington.edu/~lee/Ricci/,
2016.
[60] Yoshiaki Maeda, Steven Rosenberg, and Fabián Torres-Ardila. Computation of the Wodzicki-Chern-Simons form in local coordinates. Computationsfor S 1 actions on S 2 × S 3 . http://math.bu.edu/people/sr/articles/
ComputationsChernSimonsS2xS3_July_1_2010.pdf, 2010.
[61] Yoshiaki Maeda, Steven Rosenberg, and Fabián Torres-Ardila. The geometryof loop spaces II: Characteristic classes. Advances in Mathematics, 287:485–
518, 2016.
[62] John McCarthy. Symbol manipulating language - revisions of the language.
MIT AI Lab. AI Memo No. 4, 1958.
[63] John McCarthy. History of LISP. In Richard L. Wexelblat, editor, History ofProgramming Languages, from the ACM SIGPLAN History of Programming
Languages Conference, June 1-3, 1978, Los Angeles, California, USA, pages
173–185. Academic Press / ACM, 1978.
[64] Takayuki Muranushi, Seiya Nishizawa, Hirofumi Tomita, Keigo Nitadori,
Masaki Iwasawa, Yutaka Maruyama, Hisashi Yashiro, Yoshifumi Nakamura,
Hideyuki Hotta, Junichiro Makino, Natsuki Hosono, and Hikaru Inoue. Automatic generation of eﬃcient codes from mathematical descriptions of stencil computation. In David Duke and Yukiyoshi Kameyama, editors, Proceedings of the 5th International Workshop on Functional High-Performance
Computing, FHPC@ICFP 2016, Nara, Japan, September 22, 2016, pages
17–22. ACM, 2016.
[65] Chris Okasaki. Views for standard ml. In SIGPLAN Workshop on ML,
pages 14–23. Citeseer, 1998.
[66] Jorge Pérez, Marcelo Arenas, and Claudio Gutiérrez. Semantics and Complexity of SPARQL. In Proceedings of the 5th International Semantic Web
Conference (ISWC 2006), Athens, Georgia, United States, volume 4273 of
LNCS, pages 30–43. Springer, 2006.
[67] Simon L. Peyton Jones. The Implementation of Functional Programming
Languages. Prentice-Hall, 1987.
[68] Benjamin C. Pierce. Types and programming languages. MIT Press, 2002.
[69] Reiner Pope and Brent Yorgey. ﬁrst-class-patterns: First class patterns andpattern matching, using type families. https://hackage.haskell.org/
package/first-class-patterns, 2019. [Online; accessed 13-Mar-2020].
[70] Christian Queinnec. Compilation of Non-Linear, Second Order Patterns on
S-Expressions. In Proceedings of Programming Language Implementationand Logic Programming (PLIP 1990), Linköping, Sweden, volume 456 of
LNCS, pages 340–357. Springer, 1990.
[71] MMG Ricci and Tullio Levi-Civita. Méthodes de calcul diﬀérentiel absolu
et leurs applications. Mathematische Annalen, 54(1-2):125–201, 1900.
95

[72] Marko A. Rodriguez. The Gremlin graph traversal machine and language(invited talk). In Proceedings of the 15th Symposium on Database Programming Languages, Pittsburgh, Pennsylvania, United States, DBLP, pages 1–
10. ACM, 2015.
[73] Min Ru. Hodge theory on Riemannian manifolds. https://www.math.uh.
edu/~minru/Riemann08/hodgetheory.pdf, 2008. [Online; accessed 30-Jan2020].
[74] Bernard F Schutz. Geometrical methods of mathematical physics. Cambridge
university press, 1980.
[75] Tim Sheard and Simon L. Peyton Jones. Template meta-programming forhaskell. ACM SIGPLAN Notices, 37(12):60–75, 2002.
[76] Olin Shivers. SRFI 1: List Library. https://srfi.schemers.org/srfi-1/
srfi-1.html, 1999. [Online; accessed 30-Jan-2020].
[77] Edgar Solomonik and Torsten Hoeﬂer. Sparse tensor algebra as a parallel
programming model. CoRR, abs/1512.00066, 2015.
[78] J. Michael Spivey. Algebras for combinatorial search. J. Funct. Program.,19(3-4):469–487, 2009.
[79] Gerald Jay Sussman and Jack Wisdom. Functional diﬀerential geometry.
MIT Press, 2013.
[80] Don Syme, Gregory Neverov, and James Margetson. Extensible patternmatching via a lightweight language extension. In Ralf Hinze and Norman Ramsey, editors, Proceedings of the 12th ACM SIGPLAN International
Conference on Functional Programming, ICFP 2007, Freiburg, Germany,
October 1-3, 2007, pages 29–40. ACM, 2007.
[81] GHC team. 13.1. Language options — Glasgow Haskell Compiler 8.8.1
User’s Guide. https://downloads.haskell.org/~ghc/8.8.1/docs/html/
users_guide/glasgow_exts.html, 2019. [Online; accessed 18-Dec-2019].
[82] The Agda Development Team. Agda, 2020.
[83] The Coq Development Team. Coq, 2020.
[84] Simon J. Thompson. Laws in miranda. In Proceedings of the 1986 ACM Conference on LISP and Functional Programming, Cambridge, Massachusetts,
United States, LFP, pages 1–12. ACM, 1986.
[85] Simon J. Thompson. Lawful Functions and Program Veriﬁcation in Miranda.
Science of Computer Programming, 13:181–218, 1989.
[86] Sam Tobin-Hochstadt. Extensible Pattern Matching in an Extensible Language. In Preproceedings of the 22nd Symposium on Implementation andApplication of Functional Languages, Alphen aan den Rijn, The Netherlands, IFL, 2010.
[87] Viktor T. Toth. Tensor manipulation in GPL maxima.
s/cs/0503073, 2005.

96

CoRR, ab-

[88] Phil Trinder and Philip Wadler. Improving List Comprehension Database
Queries. In Proceedings of the 4th IEEE Region 10 International Conference
TENCON, pages 186–192. IEEE, IEEE, 1989.
[89] Mark Tullsen. First class patterns. In Proceedings of the 2nd International
Symposium on Practical Aspects of Declarative Languages (PADL 2000),
Boston, Massachusetts, United States, volume 1753 of LNCS, pages 1–15.
Springer, 2000.
[90] David A. Turner. Miranda: A Non-Strict Functional language with Polymorphic Types. In Proceedings of Conference on Functional Programming
Languages and Computer Architecture (FPCA 1985), Nancy, France, volume 201 of LNCS, pages 1–16. Springer, 1985.
[91] Nicolas Vasilache, Oleksandr Zinenko, Theodoros Theodoridis, Priya Goyal,
Zachary DeVito, William S. Moses, Sven Verdoolaege, Andrew Adams,
and Albert Cohen. Tensor comprehensions: Framework-agnostic highperformance machine learning abstractions. CoRR, abs/1802.04730, 2018.
[92] Philip Wadler. Views: A way for pattern matching to cohabit with data abstraction. In Proceedings of the 14th ACM SIGACT-SIGPLAN Symposiumon Principles of Programming Languages, Munich, Germany, POPL, pages
307–313, 1987.

97