# [stack] "unit", "cat" and inverses

## Joel Kelso — 2002-06-20 15:42:48

    Thanks to Brent Kerby for his concatenative combinators article,

    really excellent.

    I was thinking: "unit" and "cat" are kind of like _dynamic_

    equivalents of the basic quotation and concatenation program

    construction operations.  In Joy (and "Joy-with-extensional-quotation"),

    given programs "A" and "B", there is a program "A B" and programs

    "[A]" and "[B]".  This is just what "cat" and "unit" express, given

    that their arguments are quotations concatenated in front of the

    operator:

     [A] [B] cat == [A B]

     [A] unit == [[A]]

    How nice and circular: "cat" and "unit" express concatenation and

    quotation using concatentaion and quotation as their syntactic

    glue.

    "unit" has a right-inverse "i", which is just right since the job of

    "i" is exactly undoing quotation.

    The binary concatentation operator doesn't have an

    inverse, though.  Because concatenation is associative, all the

    different ways of grouping the subsequences give the same program,

    so concatentation "throws away" information about the length

    of the programs it is joining together.  So it is a many-to-one

    function with no inverse.

    What happens if we try to define a right inverse for "cat" ?

     [A B] uncat == [A] [B]

    Note that because the "A" and "B" can match sequences of any length,

    "uncat"

    can unglue any concatentation with at least two elements at any joining

    point

    This would be the inverse of "cat":

     cat uncat == id                   =>

     [A] [B] cat uncat == [A] [B] id   =>

     [A B] uncat == [A] [B] id         =>

     [A B] uncat == [A] [B]

    "uncat" has no solution with respect the standard combinators ie there

    is no program "X" with "uncat == X".  If there was we could prove

    nonsense such as

          A

       == [A] i

       == [A] [B C] zap i

       == [A B C] uncat zap i

       == [A B] [C] zap i

       == [A B] i

       == A B

    Which is nice.  I guess "cons" and "cat i" express the same thing

    as "cat", but for some reason I like "cat".

    Joel Kelso

    --

    chiral@...

    NEWS: The Commonwealth is trying to cut back on the ballooning

          costs of the Pharmaceutical Benefits Scheme.

    DKK:  I didn't know the Pharmaceutical Benefits Scheme covered

          ballooning.

## Brent Kerby — 2002-06-20 17:09:52

    > I was thinking: "unit" and "cat" are kind of like _dynamic_

    > equivalents of the basic quotation and concatenation program

    > construction operations.

     Interesting; I bet this could turn out to have some significance.

    Here's some random thoughts regarding inverses:

    - buryn is the inverse of dign, and vice versa.

    - swap is its own inverse (and to generalize, so is flip3, flip4, ...)

    - for "dup", there are two inverses: "zap" and "nip"

    - but neither "zap" nor "nip" have an inverse (because they destroy

    information).

    - like "cat", "cons" has no inverse, assuming we have transparent quotation,

    because

        [A] [zap] cons == [[A] zap] == []

      and nothing after the "cons" can get the "A" back.

    - "i" has no inverse.

    - "take" and "tack" have inverses, but the inverses are not constructible

    from combinators.

    - the inverse of any quotation is "zap".

    One useful fact is that, assuming two programs "A" and "B" are invertible,

    the inverse of "A B" is "b a", where "a" and "b" are the inverses of "A" and

    "B", respectively.

    Another useful fact is that the inverse of "[A] dip" is "[a] dip", where "a"

    is the inverse of "A".

    Combining those facts, for instance, you can find the inverse of "swap [dup]

    dip" is "[zap] dip swap" (i.e., by turning around "swap [dup] dip" to "[dup]

    dip swap", except replacing "dup" with its inverse "zap", and "swap" with

    its inverse, itself).

    I wonder if it would be possible to make an interesting system which

    contained only invertible words, like "buryn", "dign", "flipn", "unit",

    "dup"... Obviously those words alone are not enough. It would be best if the

    system was powerful enough to construct loops somehow... Yet it would seem

    that loops would require dequotation. But how we do this and still only

    admit invertible words?

    This reminds me of Henry Baker's paper, "NREVERSAL of Fortune -- The

    Thermodynamics of Garbage Collection", at

    http://linux.rice.edu/~rahul/hbaker/ReverseGC.html. It says some interesting

    things about "undoing" in general, and may shed some light on this.

    (after a moment of thought ...)

    Here's an idea. Although we can't admit "i", let's admit "run":

      [A] run == A [A]

    How can we invert "run"? By using the "undo" primitive itself, if we are

    willing to admit it; essentially, "run" keeps an extra record of the program

    that was run, so that we are able to undo it. It seems reasonable to admit

    "undo", since the system will be restricted to invertible programs, thus

    guaranteeing that "undo" can be implemented.

    However, this creates another problem. How do we invert "undo" itself? It

    seems that it has no inverse. But wait... the trick again, I bet, is not to

    admit "undo" itself, but to admit a modified version of it that keeps a

    record of what was (un)done. Let's call it "unrun" (it seems like an

    appropriate name since this, not "undo", is the literal inverse of "run"):

      [A] unrun == [A] undo [A]

    This looks promising!

     > Joel Kelso

     - Brent Kerby