Thread Links Date Links
Thread Prev Thread Next Thread Index Date Prev Date Next Date Index

Tetrits and "stickiness"

Dan,

I think I found a way to make tetrits "sticky".

If we start with the two real predicates:

   predIn(f,x) : x is in the domain of f(x)
   predOut(f,x) : x is not in the domain of f(x)

then for any interval xx, we define the two existentially-qualified
propositions:

   domainIn(f,xx) iff (there exists x in xx)predIn(f,x)
   domainOut(f,xx) iff (there exists x in xx)predOut(f,x)

The "defined" decoration is then the cartesian product of these two
propositions:

   defined(f,xx) := ( domainIn(f,xx), domainOut(f,xx) ).

If we use binary digits "1" and "0" instead of "true" and "false", then,
e.g., we have your "tetrits" mapping:

   defined(sqrt, [1,2]) = ( 1, 0 )
   defined(sqrt, [-2,1]) = ( 1, 1 )
   defined(sqrt, [-2,-1) = ( 0, 1 )
   defined(sqrt, [empty] ) = ( 0, 0 )

Now, the trouble is, for "sticky" behavior with decorations, we'd like a new
decoration to be the infimum of two input decorations. For example, it would
be nice if we can simply take the bitwise-AND of two tetrits, as can be done
with trits.

Notice, however, that the infimum of

   defined(sqrt, [1,2]) = ( 1, 0 ) and defined(sqrt, [-2,1]) = ( 1, 1 )

is ( 1, 0 ). This is not the result we want, since it means "sqrt was
everywhere defined" but this was not true for the decoration of
sqrt([-2,1]).

This can be fixed if we re-define the "defined" decoration as:

   defined(f,xx) := ( domainIn(f,xx), domainIn(f,xx) xor domainOut(f,xx) ).

For example, now we have:

   defined(sqrt, [1,2]) = ( 1, 1 )
   defined(sqrt, [-2,1]) = ( 1, 0 )
   defined(sqrt, [-2,-1) = ( 0, 1 )
   defined(sqrt, [empty] ) = ( 0, 0 )

Notice that the mapping produces tetrits that are properly ordered, so
taking the infimum (the bitwise-AND in this case) of two decorations always
gives the proper result. For example, the infimum of

   defined(sqrt, [1,2]) = ( 1, 1 ) and defined(sqrt, [-2,1]) = ( 1, 0 )

is again ( 1, 0 ), but now this means "sqrt was somewhere defined and
somewhere not defined", which is what we want.

Nate