TypedLambda 1.0 2025-01-18

---- JavaSE-17 signature
1552787810
1361960727
739498517

---- Types
(o -> o)  ==  f
(o -> o -> o)  ==  b
((o -> o) -> o -> o)  ==  n

n -> n
true

---- Sub-Types
o -> o -> o              o -> o -> o              yes  yes  yes
o -> o -> o              (o -> o) -> o            no   no   no 
o -> o                   o -> o -> o              no   no   yes
o -> o -> o              (o -> o) -> o -> o       no   no   yes
o -> o                   (o -> o) -> o -> o       no   no   yes

---- Term convertions
\a.a  ->  \ 1  ->  \a.a
\ab.a  ->  \ \ 2  ->  \ab.a
\ab.b  ->  \ \ 1  ->  \ab.b
\ab.ab  ->  \ \ 2 1  ->  \ab.ab
\ab.a(ab)  ->  \ \ 2 (2 1)  ->  \ab.a(ab)
\ab.a(a(ab))  ->  \ \ 2 (2 (2 1))  ->  \ab.a(a(ab))
\ab.ba  ->  \ \ 1 2  ->  \ab.ba
\abc.abc  ->  \ \ \ 3 2 1  ->  \abc.abc
\abc.b(abc)  ->  \ \ \ 2 (3 2 1)  ->  \abc.b(abc)
\abc.cab  ->  \ \ \ 1 3 2  ->  \abc.cab
\abc.ab  ->  \ \ \ 3 2  ->  \abc.ab
\abc.ac  ->  \ \ \ 3 1  ->  \abc.ac
\abcd.ac(bcd)  ->  \ \ \ \ 4 2 (3 2 1)  ->  \abcd.ac(bcd)
\abcd.a(bc)d  ->  \ \ \ \ 4 (3 2) 1  ->  \abcd.a(bc)d
\ 1  ->  \ 1
\ \ 2  ->  \ \ 2
\ \ 1  ->  \ \ 1
\ \ 2 1  ->  \ \ 2 1
\ \ 2 (2 1)  ->  \ \ 2 (2 1)
\ \ 2 (2 (2 1))  ->  \ \ 2 (2 (2 1))
\ \ 1 2  ->  \ \ 1 2
\ \ \ 3 2 1  ->  \ \ \ 3 2 1
\ \ \ 2 (3 2 1)  ->  \ \ \ 2 (3 2 1)
\ \ \ 1 3 2  ->  \ \ \ 1 3 2
\ \ \ 3 2  ->  \ \ \ 3 2
\ \ \ 3 1  ->  \ \ \ 3 1
\ \ \ \ 4 2 (3 2 1)  ->  \ \ \ \ 4 2 (3 2 1)
\ \ \ \ 4 (3 2) 1  ->  \ \ \ \ 4 (3 2) 1
(\ 1) \ 1  ->  (\ 1) \ 1
\ 1 \ 1  ->  \ 1 \ 1
\ (1 \ 1)  ->  \ 1 \ 1

---- Type assignment
UntypedTermException
\a.a : [o] -> [o]
\ab.a : [o] -> [f]
\ab.b : [o] -> [f]
\ab.ab : [f] -> [f]
\ab.a(ab) : [f] -> [f]
\ab.a(a(ab)) : [f] -> [f]
\ab.ba : [o] -> [f -> o]
\abc.abc : [b] -> [b]
\abc.b(abc) : [n] -> [n]
\abc.cab : [o] -> [o -> b -> o]
\abc.ab : [f] -> [b]
\abc.ac : [f] -> [b]
\abcd.ac(bcd) : [b] -> [b -> b]
\abcd.a(bc)d : [b] -> [f -> b]
\abc.abc : [b] -> [b]
\abcd.abcd : [o -> b] -> [o -> b]
f
f -> o
b
o -> f -> o
n
o -> b
b -> o
o -> b -> o
f -> b
o -> o -> b -> o
b -> b
n -> n
b -> f -> b
o -> b -> o -> b
b -> b -> b
0 0 0 1 0 0 0 3 0 0 0 5 0 0 0 0 0 0 0 2 0 0 0 2 0 0 0 2 0 0 0 0 

---- Reducing
(\ \ 4 2 \ 1 3) \ 5 1
 =B=> \ 3 \ 6 1 \ 1 \ 7 1
\ 1 = \ 1
\ \ 2 = \ \ 2
\ \ 1 = \ \ 1
\ \ 2 1 = \ \ 2 1
\ \ 2 (2 1) = \ \ 2 (2 1)
\ \ 2 (2 (2 1)) = \ \ 2 (2 (2 1))
\ \ 1 2 = \ \ 1 2
\ \ \ 3 2 1 = \ \ \ 3 2 1
\ \ \ 2 (3 2 1) = \ \ \ 2 (3 2 1)
\ \ \ 1 3 2 = \ \ \ 1 3 2
\ \ \ 3 2 = \ \ \ 3 2
\ \ \ 3 1 = \ \ \ 3 1
\ \ \ \ 4 2 (3 2 1) = \ \ \ \ 4 2 (3 2 1)
\ \ \ \ 4 (3 2) 1 = \ \ \ \ 4 (3 2) 1
(\ \ 4 2 \ 1 3) \ 5 1 = (\ \ 4 2 \ 1 3) \ 5 1

(\ \ 2 (2 (2 (2 (2 (2 (2 (2 1)))))))) \ \ 2 (2 1)
 =B=> decimal 256 binary 100000000 hexa 100 using 31 ms for 510 reductions, 772 substitutions.

(\ \ 2 (2 (2 (2 (2 (2 (2 (2 (2 1))))))))) \ \ 2 (2 1)
 =B=> decimal 512 binary 1000000000 hexa 200 using 43 ms for 1022 reductions, 1541 substitutions.

(\ \ 2 (2 (2 (2 (2 (2 (2 (2 (2 (2 1)))))))))) \ \ 2 (2 1)
 =B=> decimal 1024 binary 10000000000 hexa 400 using 61 ms for 2046 reductions, 3078 substitutions.

(\ \ 2 (2 (2 (2 (2 (2 (2 (2 (2 (2 (2 1))))))))))) \ \ 2 (2 1)
 =B=> decimal 2048 binary 100000000000 hexa 800 using 296 ms for 4094 reductions, 6151 substitutions.

(\ \ 2 (2 (2 (2 (2 (2 (2 (2 (2 (2 (2 (2 1)))))))))))) \ \ 2 (2 1)
 =B=> decimal 4096 binary 1000000000000 hexa 1000 using 1086 ms for 8190 reductions, 12296 substitutions.
Terms(int) 54178

---- Arithmetic
+1 = \abc.b(abc) == \ \ \ 2 (3 2 1) : n -> n
+2 = \abc.b(b(abc)) == \ \ \ 2 (2 (3 2 1)) : n -> n
+3 = \abc.b(b(b(abc))) == \ \ \ 2 (2 (2 (3 2 1))) : n -> n
*1 = \abc.abc == \ \ \ 3 2 1 : b -> b
*2 = \abc.ab(abc) == \ \ \ 3 2 (3 2 1) : b -> b
*3 = \abc.ab(ab(abc)) == \ \ \ 3 2 (3 2 (3 2 1)) : b -> b

---- Couples
NotInNormalFormException
<I,I> =B= \ab.ab : [f] -> [f]
<K,K> =B= \abcd.ab : [f] -> [o -> b]
<F,F> =B= \abcd.ad : [f] -> [o -> b]
<1,1> =B= \abcd.a(bcd) : [f] -> [b -> b]
<2,2> =B= \abcd.a(b(bc)(b(bc)d)) : [f] -> [b -> b]
<^,^> =B= \abcd.a(d(cb)) : [f] -> [o -> f -> f -> o]
<+,+> =B= \abcdefgh.a(bd(cde)g(fgh)) : [f] -> [o -> o -> b -> b -> o -> o -> b -> b]
<*,*> =B= \abcdefgh.a(b(cd)e(fg)h) : [f] -> [o -> o -> b -> f -> o -> o -> f -> b]

---- Type assignment reasoning
\ \ \ \ [4, [[3, 2], 1]]@fa03bf3d
Type assignment of \abcd.a(bcd)
abstractions naming
N0 = A0 = \ \ \ \ [4, [[3, 2], 1]]
N1 = A1 = \ \ \ [4, [[3, 2], 1]]
N2 = A2 = \ \ [4, [[3, 2], 1]]
N3 = A3 = \ [4, [[3, 2], 1]]
leaves naming
L0 -> A0
L1 -> A1
L2 -> A2
L3 -> A3
applications naming
N4 = P0 = [L1 L2] = [3, 2]
N5 = P1 = [P0 L3] = [[3, 2], 1]
N6 = P2 = [L0 P1] = [4, [[3, 2], 1]]
application rules step 1
L2 : o
P0 : o
=> (L2 -> P0) : o -> o
L3 : o
P1 : o
=> (L3 -> P1) : o -> o
P1 : o
P2 : o
=> (P1 -> P2) : o -> o
N1 : o -> o
N4 : o -> o
N0 : o -> o
application rules step 2
L2 : o
P0 : o -> o
=> (L2 -> P0) : o -> o -> o
L3 : o
P1 : o
=> (L3 -> P1) : o -> o
P1 : o
P2 : o
=> (P1 -> P2) : o -> o
N1 : o -> o -> o
application rules step 3
L2 : o
P0 : o -> o
=> (L2 -> P0) : o -> o -> o
L3 : o
P1 : o
=> (L3 -> P1) : o -> o
P1 : o
P2 : o
=> (P1 -> P2) : o -> o
abstraction rules
B : o
(N3 -> B) : [o] -> [o]
(N2 -> B) : [o] -> [o -> o]
(N1 -> B) : [o -> o -> o] -> [o -> o -> o]
(N0 -> B) : [o -> o] -> [(o -> o -> o) -> o -> o -> o]

---- TypedLambda demonstration page end

αBγδεζηθικ\μνξοπρςστυφχψω