Controlling Reductions

Haskell has an option for user defined reductions. I have no idea how it works.

Felix also has two ways to do this.

The first way is complete but hard to use: the parser accepts user defined patterns in the form of grammar productions, and then the user writes Scheme code to manipulate the parse tree to produce any combination of a fixed set of AST terms they like.

The second way is simpler but typed, and looks roughly like this:

reduce strings 
  | (a:string,b:string) : a + b=> scat ([b,a]) ;
reduce scat2 
  | (x:list[string], y:string) : scat ([y, scat x]) => scat (Snoc (x,y)) ;

Its polymorphic though that's not seen in this example. The vertical bar indicates you can provide several alternatives which are tried in sequence. The algorithm applies each reduction, and each is applied top down. The above example doesn't work! The intent was to replace string concatenation using a left associative binary operator with a faster function scat, operating on a list. Clearly I needed the algo to work bottom up.

The contrast between these two methods is that the first method has a complete general purpose programming language available to perform the reductions, the pattern matching uses a fixed algorithm (the GLR+ parser). The second method recognises terms and performs the reductions using a fixed algorithm so is much weaker.

What I want is something less complex than having to hand write the whole reduction machinery in a general purpose language (I could do that, using dynamically compiled and loaded Ocaml modules but it's too hard for end users).

So I'm looking for a *compromise* which is reasonably simple, but also reasonably capable. I added alternatives for this reason and am thinking to add an adjective which specifies if a reduction should be applied top down or bottom up. A more complex option is to allow for nested reductions (so that if one reduction succeeds it triggers another one).

Any ideas?

Hm

In your example of application, is it possible to produce a reduction system that does not depend on the application order of the rules? Here would be a proposal:


rewrite
| (?a + ?b) => concat(list(?a) ++ list(?b))
| list(?a + ?b) => list(?a) ++ list(?b)
| list(concat(?li)) => ?li
| list(?s) => [?s]

where, on an arbitrary syntax node, rules are tried top-down and the first matching one applies (in particular the last one only applies when no other matches), and the result of rewriting can still be rewritten later.

(This does not really answer your question, and I don't think it composes particularly well, as other rewrite rules may produce new (a + b) nodes and not mesh well with the syntactic way "not a concat or a +" is implemented by the last rule, but I thought it was a fun puzzle.)

By gasche at Sat, 2017-02-25 00:46 | login or register to post comments

Overlapping and Pure Prolog

If you disallow overlapping so only one rule can match, then there can only be one order. You can recover lost functionality by allowing negative matches in the clause heads. For example the classic case of overlapping "(?a, ?a)" and "(?a, ?b)" can be expressed in a non-overlapping way by replacing the latter with "(?a, ?b) where ?a != ?b".

My solution for these kind of things is to provide a variant of pure Prolog as a meta-language. So Prolog rules match the parse tree (or the parse tree metadata) something like "rule(InTree, OutTree)".

By Keean Schupke at Sat, 2017-02-25 09:28 | login or register to post comments

Order

Actually it is NOT true that there is only one order if rules don't overlap. Heck, this is Lambda-The-Ultimate! Lambda calculus has only ONE reduction, beta-reduction. Yet, there is more than one order and the results may not be the same (some orders diverge).

By skaller at Sun, 2017-03-05 02:01 | login or register to post comments

One order

There can only be one order of matches, that does not mean there is only one valid order. It depends whether you are looking for one solution or all solutions. For many problems finding one solution is proof there is a solution, or finding no solution is proof there is none. We are not often interested in the number of ways of proving something, nor in finding the optimal (shortest proof).

We can actually recover the shortest proof at a small cost (2 O) by using iterative deepening. So we can find the shortest proof, we can know there is no shorter proof, however we do not know how many equally short proofs there may be.

So for a parser we can deterministically know the shortest parse, without having to match more than one order at any step of the iterative deepening.

By Keean Schupke at Sun, 2017-03-05 08:04 | login or register to post comments

I think some Computer Algebra Systems do this

Some Computer Algebra Systems (CAS) seem to do this. The Wolfram language has somewhat of an implementation what seems to do what you seem to want. (But the pattern matching code seems to be around 250 pages.)

In its simplest form, a CAS can be implemented as rewriting machinery on Lisp-like expressions. I.e., Lisp like nodes for expression representation and a pattern compiler for rewrite definitions. It shouldn't be that hard.

Usually, you'll end up with a slow but robust math language where you'll find you'll need lots of reduction strategy interaction primitives to implement wanted functionality. (Generalized pattern matching is pretty powerful but you often need lots of "Do this after that" variants.)

Or maybe you're looking for Knuth-Bendix? That's a manner of deducing a confluent rewrite systems, if one exists, for a set of rewrite rules. That's used in some symbolic provers I imagine but its too simple for a CAS, where you need more control and don't really want confluency.

Something like the above?

By marco at Sat, 2017-02-25 18:20 | login or register to post comments

Optimization

My understanding of the example, and the mention of GHC's rewriting rule, is that the idea is to have a way to express rewriting rules that represent meaning-transforming but performance-improving transformations of programs for optimization purpose: you would run them "statically" at compilation time, and they should preserve the dynamic semantics of the program. In particular, I would expect performance of rewriting to not be a central issue, and robustness and predictability of the behavior to be central (for example, robustness of applicability of optimizing rewritings with respect to small changes in the program source).

By gasche at Sat, 2017-02-25 21:37 | login or register to post comments

Performance is always an issue

Performance is always an issue.

Anyway. Like that, huh? I guess it shouldn't be hard to patch something together like that but it would also become almost instantly Turing complete. That's not bad, it would enable you to implement a lot of (compiler) optimizations directly in the language but also would imply that with all that power under your fingertips you'll soon run into performance considerations.

By marco at Sun, 2017-02-26 02:41 | login or register to post comments

Scheme code

You don't need a Scheme code to manipulate the parse tree, you just have to have a parse tree on both sides. It could be all about reductions, that is - one expression reduces to another. And it doesn't really matter what either expression means from the aspect of rewriting rules. The code that catches the final expression deals with it, being Javascript, C, or Felix.

By Ivan V. at Mon, 2017-02-27 20:35 | login or register to post comments

Lambda the Ultimate

User login

Navigation