# Combinatory Axioms

## Brent Kerby — 2002-04-08 09:13:52

    > (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