> (I'll mention one such rule which I stumbled upon a while back:
> swap [i] dip == dip)
> [...]
> - Manfred
Rules like these are kind of interesting. Here a few more:
swap [swap] dip swap == [swap] dip swap [swap] dip
cat dip == [dip] dip dip
dip zap == [zap] dip i
[zap] dip == swap zap
What's interesting is that in an applicative system it is possible to have a
finite set of these kinds of axioms (say, 10 of them or so), from which all
others can be derived. I'm guessing the same kind of thing will happen in
Joy, but I'm not quite sure how to do it. Curry had some sort of systematic
way of generating the axioms, starting with the rewrite rules (i.e., "Cfxy
== fyx", etc.), and abstracting away one variable at a time ...
However, even if we did have a complete set of axioms, it is not
neccessarily practical to use them to test two combinators for equality,
because of the problem you described (if two combinators are equivalent,
then there _is_ a way using the axioms to rewrite one so it matches the
other; however, it may require using the "expanding" directions of the
axioms. To use an analogy, getting one combinator to match an equivlaent one
using the axioms is like wandering through a bizarre maze, where each room
leads to ten or more others, and even though the path from the start to the
finish is fairly short, there are infinitely many rooms you can get lost in
which will never lead you to the finish).
On the other hand, if I remember correctly, if you permit axiom _schemes_,
in addition to axioms, then I think the approach becomes feasible, because
then only one direction of the axiom becomes neccessary. Here's what a
couple axiom schemes in Joy might look like:
[A B] dip => [A] dip [B] dip
[A] dip zap => zap A
I can't guarantee that this would actually work, but that is what I recall
happening in a Curry's certain formalization of applicative combinators, at
least. Again, I remember him starting from the rewrite rules and abstracting
how one variable at a time. Hmm... so we could start with
[B] [A] dip == A [B]
and then abstract out the A, giving
A\ [B] [A] dip => A\ A [B]
[[B]] dip dip => i [B]
Wow, this is a valid scheme. Then we abstract out the "B" also to get:
[] cons dip dip => [i] dip
Wow, this is a valid rule (it says "swap dip => [i] dip", basically, since
"[] cons dip" is "swap"; this is similar to the rule you initially pointed
out).
Now, if we'd done the abstraction in a different order, we'd get different
rules, I bet:
B\ [B] [A] dip => A [B]
[A] dip => [A] dip
Ahh, a pointless rule. Perhaps that always happens when abstracting the last
parameter.
Well, this is looking promising. Let's try it with "cons":
A\ [B] [A] cons => A\ [[B] A]
[[B]] dip cons => [[[B]] dip i] cons
Interesting that this gives an expanding rule ... Anyway, abstracting out
the B, we get
[] cons dip cons => [[] cons dip i] cons cons
This seems to be a dead end. These are all the rules we'll get with this
approach (just the two axioms and two axiom schemes), if we're in the base
{i, cons, dip, dup, zap}. However, I remember now, actually, for the
approach to work with axiom schemes, you have to have an _infinite_ number
of them ( :-) ), although there is a pattern for generating them. The trick
is to, say, start with "zap"'s rewrite rule
[A] zap =>
But then prepend a "B" to both sides, which makes another valid rewrite
rule.
B [A] zap => B
Now we can abstract an "A" and something meaningful happens:
A\ B [A] zap => A\ B
[B] dip zap => zap B
This is a valid scheme (it was mentioned earlier, actually) ...
Yeah, this gets kind of weird. We start with the rewrite rules as the basic
axiom schemes. But then, you can always generate more axiom schemes by
either abstracting out a variable from an axiom scheme, or by prepending or
postpending something to an axiom scheme (which creates more possibilities
for abstracting variables out).
Somehow though it worked out where only a finite number of rules were
needed, as long as they were allowed to be bidirectional.
I don't know. All these axiom schemes get kind of messy and puzzling. Maybe
another day they'll make more sense.
I think really the best way to test two combinators for equality is not to
try to reduce them with axiom schemes, but to actually run them, and see if
they give the same results (this is the approach my brute-force searcher
uses); of course, the problem there is that if one of them is
non-terminating then you'll never get an answer (although the same problem
will probably happen with the axiom-scheme approach, because some
axiom-schemes are expanding, which could lead to non-terminating reductions;
but, I bet a combinator will only fail to reduce by the axiom-schemes if it
is non-terminating).
By the way, Manfred ... I started on that article; it really is going to
happen :-)
- Brent