disorganized notes on 3-coloring lambda terms

gistfile1.txt

it follows from 4ct that:
[[[
every normal term with one free variable has at least one of these colorings:
0

every normal term with two free variables has at least one of these colorings:
12
21

every normal term with three free variables has at least one of these colorings:
220
202
101
110

every normal term with four free variables has at least one of these colorings:
1112
1121
1020
1002
2001
2010
2212
2221
]]]

0-pre-normal colorings:
0 --- 12, 21 --- 000, 220, 022, 011, 110
a normal coloring C is either 0 or
w ^ !w(C) with C normal.

thm: if 4ct, then every normal term has a normal coloring.

thm: no strict prefix of a normal coloring is normal.

proof: by induction.
trivial for 0.
easy for 12, 21.

suppose w ^ !w(C) has a strict prefix that is normal, of length n.
That means C splits as D ^ E with D having length n-1. So w ^ !w(D) is
normal, allegedly. By the definition of normal, then D must be normal.
But then D is a strict normal prefix of C, also normal. By i.h. this
is a contradiction, qed.


if I have a term N1 of size n1 and N2 of size n2 then there exists w and
colorings C1, C2 such that
w(C1) ^ !w(C2)
is normal.


Every term has a coloring C such that exists w such that w(C) ^ !w is normal. Call these colorings "0-pre-normal".
Every term has a coloring C such that exists w such that !w ^ w(C) is normal. <- same as "C is normal".
Every term has a coloring C such that exists w such that w(C) ^ !w(12) is normal or w(C) ^ !w(21) is normal

12 01 02
21 10 20

reasoning principle: If I know of a particular term that has few
colorings, in particular it has only colorings complementary to D, E,
I can infer that every complementary term must be colorable as D or E.
Buuut maybe I shouldn't expect this to happen in practice. My previous
analysis about having "few colorings" was not about terms with lots of
free variables, it was about few internal alternate colorings.

let M be a smallest normal bridgeless term with some free vars whose lambda closure (up to 1 free var) can't be 3-colored.

if M is \x.M0 then M0 is a smaller normal bridgeless term whose lambda closure can't be 3-colored.

So M =
x1, ..., xn |- R    y1, ..., ym |- N
------------------------------------
x1, ..., xn, y1, ..., ym |- R N

     L
    / \
    |  L
   /  /^
  /  v  \
 /  @\   \
/  /  \   \
-->    >@--
        ^
        |

\x.\y. (y x) n

N |- X ->> (X >-> N >-> Y) ->> Y

n
\a
/\
xy

x = n - a
y = n + a
x + y = -n
x - y = a

 /\
/\ \
f::    [n] a, b -> n-a-b, n-a+b, n-a         (nAB, nAb, na)
finv:: x, y, z -> [x+y-z] (-x-y-z, x - y)    [xyZ] (XYZ, xY)


 /\
/ /\
g::    [n] a, b -> n-a, n+a-b, n+a+b         (nA, naB, nab)
ginv:: x, y, z -> [-x+y+z]  (x+y+z,  y-z)    [Xyz] (xyz, yZ)


f; ginv = (a, b) -> (A, ab)

g; finv = (a, b) -> (A, ab)

y C, x c |- y @c x
y CD, x cD, n d |- (y @c x) @d n
x d, n C |- \(CD)y . (y @c x) @d n
n Cd |- \(d)x.\(CD)y . (y @c x) @d n

(c, d) |-> (d, CD)
00 -> 00
20 -> 10
10 -> 20
01 -> 21
02 -> 12
12 -> 02
21 -> 01
11 -> 11
22 -> 22
\x.\y. (y @c x) @d n

            0
            |
    +-------La---+
    A            |
    |      +-aB--Lb--ab+
    |      |           |
    |   +--@c-+aBc     |
    |   |     |        |
    |  aBC    @d       |ab
^   |   |    / \       |
|   |   |   |   |      |
N   X---X   N   Y-aBcd-Y
\____aBcD___/


A = aBC
aBcd = ab
aBcD = 0


a = BC

b = d



            0
            |
    +-------La---B
    G            |
    |      +-R---Lb--G-+
    |      |           |
    |   +--@c-+ B      |
    |   |     |        |
    |  aBC    @d       |ab
^   |   |    / \       |
|   |   |   |   |      |
N   X---X   N   Y-aBcd-Y
\____  R ___/


n lambdas <-> n apps <-> n+1 type vars




let the n-parity of a string s, call it Pn(s), be the parity of the number of ns occurring in s.

a string s is regular if P0(s) != P1(s) = P2(s).
Examples of regular strings:
0
12
21
110
202

thm: the context at every point in the derivation of a well-typed chiral term is always regular.

the counts of 0s, 1s, 2s in a regular string can either be 011 or 100. Mapping a number across a string rotates it.

lambda case: start with a triple b011 where b is 0 or 1
pos. chir. b011 -> b101 -> b100
neg. chir. b011 -> b110 -> b100

application case:
(b011, c011) -> (b101, c110) -> bc(011)
(b011, c011) -> (b110, c101) -> bc(011)

This means that if a context splits at a certain point, there should
be a natural chirality of the application that we can infer, as a linear function
of the annotations in the context.

like if I find
x
then I add -x to make it regular.
If I find
01 I add 1
10 I add 1
02 I add 2
20 I add 2
so if I find
xy I add x+y
if I find
011 I add 0
122 I add 2
200 I add 1
so... 1+x+y+z or maybe 2-(x+y+z)? neither works. hmmm.