[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