Conversion patterns of pattern matching to disjoint patterns

Learning
1

Hi all!

I need to develop algorithm to convert common patterns (without guards) to equivalent disjoint patterns.

For example, for type

type tree = Leaf | Node of tree * tree

I would like to convert program

match x with
| Node (_, Leaf) -> 1
| Node (Leaf, _) -> 2
| _              -> 3

to

match x with
| Node (_, Leaf)                 -> 1
| Node (Leaf, Node (_, _))       -> 2
| Node (Node (_, _), Node(_, _)) -> 3
| Leaf ->                           3

I guess this problem already has solved, but I can’t find any solutions.

I would be grateful for any links to papers or code, keywords, anything that you think will help to find these solutions.

2

This can easily be done using “matrix decomposition” approaches to pattern-matching analysis. See for example Compiling Pattern Matching to good Decision Trees, Luc Maranget, 2008. Pattern matrices and matrix decomposition are explained on pages 2 and 3.

In your example, the decomposition may go as follows:

| Node (_, Leaf) -> 1
| Node (Leaf, _) -> 2
| _              -> 3

= (split first column in Node|Leaf)

Node(â–ˇ)  | (_, Leaf) -> 1
Node(â–ˇ)  | (Leaf, _) -> 2
Node(â–ˇ)  | (_, _) -> 3
Leaf     | -> 3

= (split first tuple column)

Node(â–ˇ, â–ˇ) | _   Leaf -> 1
Node(â–ˇ, â–ˇ) | Leaf _ -> 2
Node(â–ˇ, â–ˇ) | _    _ -> 3
Leaf       | -> 3

= (split first colum in Node|Leaf)

Node(Node(â–ˇ, â–ˇ), â–ˇ) | _ _ Leaf -> 1
Node(Node(â–ˇ, â–ˇ), â–ˇ) | _ _ _ -> 3
Node(Leaf, â–ˇ) | Leaf -> 1
Node(Leaf, â–ˇ) | _ -> 2
Node(Leaf, â–ˇ) | _ -> 3
Leaf | -> 3

= (push two colums)

Node(Node(_, _), â–ˇ) | Leaf ->1
Node(Node(_, _), â–ˇ) | _ -> 3
Node(Leaf, â–ˇ) | Leaf -> 1
Node(Leaf, â–ˇ) | _ -> 2
Node(Leaf, â–ˇ) | _ -> 3
Leaf | -> 3

= (split first column in Node|Leaf)

Node(Node(_, _), Node(â–ˇ,â–ˇ)) | _ _ -> 3
Node(Node(_, _), Leaf) | -> 1
Node(Node(_, _), Leaf) | -> 3
Node(Leaf, Node(â–ˇ,â–ˇ)) | _ _ -> 2
Node(Leaf, Node(â–ˇ,â–ˇ)) | _ _ -> 3
Node(Leaf, Leaf) | -> 1
Node(Leaf, Leaf) | -> 2
Node(Leaf, Leaf) | -> 3
Leaf | -> 3

= (push two columns)

Node(Node(_, _), Node(_,_)) | -> 3
Node(Node(_, _), Leaf) | -> 1
Node(Node(_, _), Leaf) | -> 3
Node(Leaf, Node(_,_)) | -> 2
Node(Leaf, Node(_,_)) | -> 3
Node(Leaf, Leaf) | -> 1
Node(Leaf, Leaf) | -> 2
Node(Leaf, Leaf) | -> 3
Leaf | -> 3

= (remove unreachable rows, final result)

Node(Node(_, _), Node(_,_)) -> 3
Node(Node(_, _), Leaf) -> 1
Node(Leaf, Node(_,_)) -> 2
Node(Leaf, Leaf) -> 1
Leaf -> 3
3 Likes
3

Hi not_kill !

It is more than a guess, ocaml compiler does it:

type tree = Leaf | Node of tree * tree
let f = function
| Node (_, Leaf) -> 1
| Node (Leaf, _) -> 2;;
Characters 8-60:
Warning 8: this pattern-matching is not exhaustive.
Here is an example of a case that is not matched:
(Node (Node (_, _), Node (_, _))|Leaf) (* copy paste here when lazy *)
val f : tree -> int = <fun>

I think gasche suggest a really good resource to do this. If ever you want more, you can type keywords like “compiling pattern matching” or “pattern matching exhaustive check” on your search engine.
Have a good day !

4

Thanks, this is similar to what I need!
But also I would like to minimize count of patterns (in my example after conversion we have 4 patterns, but after sequence of decompositions we have 5 patterns).

I going to converse ocaml pattern matching to miniKanren relational program. And I need as few disjoint patterns as possible.

Do you know how to convert patterns while minimizing disjoint patterns number?
As above, any ideas, links, keywords will be useful to me!

6

Hi ruyblast!

Thank you for the answer!

Indeed, the problem of construction exhaustive patterns is similar to the problem I need to solve.
But I already have exhaustive patterns and I need to construct equivalent disjoint patterns. In this case, it will be possible to process the patterns independently.

7

Ok you want to collapse

Node(Node(_, _), Leaf) -> 1
Node(Leaf, Node(_,_)) -> 2
Node(Leaf, Leaf) -> 1

in

Node(_, Leaf) -> 1
Node(Leaf, _) -> 2

(dropping Node (Leaf, Leaf) and ending with a minimal number of disjoint pattern). This issue is addressed by usual pattern matching compilation I think. This algorithm is known as “F algorithm” I think (if I remember well ^^). In such algorithm, you have your matrix of patterns, and a column of corresponding actions (numbers 1 to 3 in your example). The result of the algo enable you both to find every patterns, but also to withdraw patterns that are never reached (which correspond to your minimal disjoint pattern number as far as I understand, after collapsing), by identifying actions that are not taken (because covered by previous set of constructors). Although I do not know how to exactly do that, (so I’ll stop posting so that someone really qualified can answer accurately to your post) I think this will be covered in resource that gasche advised to you, and by the way, this is really linked to pattern matching compilation (with both exhaustive check and redundancy detection, that you get for free in the algorithm), at least for the kind of example you provided.
(And if ever you are desperate, in the worst case, to collapse your patterns, there is brute force algorithm where you exhaustively try to identify full sets of variants from a same constructor (here Leaf and Node) in the same position in rows of your pattern matrix that leads to a same action (here, it would collapse

Node(Node(_, _), Leaf) -> 1
Node(Leaf, Leaf) -> 1

in

Node(_, Leaf) -> 1

because both leads to action 1. Then you could also similarly try to generalize patterns for cases covered up by previous rows in your matrix. Here it would collapse

Node(_, Leaf) -> 1
Node(Leaf, Node(_,_)) -> 2

into

Node(_, Leaf) -> 1
Node(Leaf, _) -> 2

because case Node(Leaf, Leaf), when column 2 is reached, has already be covered by case 1.)
Tell me if I misunderstood what you intended but for now I think this is the tool you are searching for.
Good luck for your project !
Best !

8

@ruyblast I think that the behavior you propose in your example does not satisfy @not_kill’s question, because the two patterns are not disjoint anymore (Node(Leaf, Leaf) matches both). @not_kill is converting a pattern-matching in a logic program, think of a series of independent Prolog clauses, so it is important to have a semantics that does not depend on clause order. The pattern-matching algorithms that I know typically assume a top-to-bottom order. (But I am not an expert on pattern-matching compilation, so I may miss something obvious to make them non-order-independent.)

Last time I looked at this topic I thought that I didn’t know how to minimized as @not_kill would like to. But now, after thinking more about it from @ruyblast answer, I think I have a proposal.

Remark that pattern-matching decomposition is good at merging/sharing “common prefixes” during the traversal: during decomposition each submatrix corresponds to all reachable sub-patterns from a given prefix of the input. If at some point, all rows point to the same action, we can stop testing further (replace it with wildcard patterns). On the other hand, it is not good at finding “common suffixes”, where different inputs have the same continuation of tests to do. (Note: Indeed as @ruyblast suggests this is certainly addressed in pattern-matching compilation literature, for example I think that this is addressed specifically in the “Compiling pattern-matching to good decision trees” paper.)

In the example of the decomposition I proposed earlier:

Node(Node(_, _), Node(_,_)) -> 3
Node(Node(_, _), Leaf) -> 1
Node(Leaf, Node(_,_)) -> 2
Node(Leaf, Leaf) -> 1
Leaf -> 3

we have disjointness, but the two -> 1 cases share a common suffix: after matching the first argument of the node (which is different in each case), there is only a Leaf test to do before returning 1, which suggests that in fact some of the distinctions we made before were not useful.

My naive idea is to re-do a decomposition of the matrix in reverse order, from right to left, to merge common suffixes. If we get the same matrix, we stop simplifying. If we get a simpler matrix, we do another iteration (from left to right), etc., until we reach a fixpoint (each simplification strictly decreases the total size). On this example, the second decomposition goes as follows (it gives the expected, minimal result):

Node(Node(_, _), Leaf) -> 1
Node(Leaf, Node(_,_)) -> 2
Node(Leaf, Leaf) -> 1
Leaf -> 3

=>

Node(â–ˇ, â–ˇ):
  Node(_, _) Node(_,_) -> 3
  Node(_, _) Leaf -> 1
  Leaf       Node(_,_) -> 2
  Leaf,      Leaf -> 1
Leaf -> 3

=> 

Node(â–ˇ, Node(â–ˇ, â–ˇ)):
  Node(_, _) _ _ -> 3
  Leaf       _ _ -> 2
Node(â–ˇ, Leaf):
  Node(_, _) -> 1
  Leaf,      -> 1
Leaf -> 3

=> 

Node(â–ˇ, Node(_, _)):
  Node(_, _) -> 3
  Leaf       -> 2
Node(_, Leaf) -> 1
Leaf -> 3

=> 

Node(Node(_, _), Node(_, _)) -> 3
Node(Leaf, Node(_, _)) -> 2
Node(_, Leaf) -> 1
Leaf -> 3
1 Like
9

Note: I’m not sure that this proposal really provides minimality (I can’t find a counter-example; but maybe there can be a source of efficiency “in the middle” that is caught by neither order). In fact I seem to remember that there are NP-hardness results for similar problems, so it may be impossible to have a reasonably fast minimization algorithm. (If this algorithm is not minimizing, then a naturally related one would be to exhaustively try all column orders instead of just left-to-right and right-to-left, and that one is exponential in the number of columns.)