LambdaKit 1.0 2025-07-20

---- JavaSE-17 signature
864237698
537548559
380894366

---- Types
(o -> o)  ==  f
(o -> o -> o)  ==  b
((o -> o) -> o -> o)  ==  n
(o -> o -> o -> o)  ==  4
(o -> o -> o -> o -> o)  ==  5
(o -> o -> o -> o -> o -> o)  ==  6
(o -> o -> o -> o -> o -> o -> o)  ==  7
(o -> o -> o -> o -> o -> o -> o -> o)  ==  8
(o -> o -> o -> o -> o -> o -> o -> o -> o)  ==  9

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

---- Convertions
    λ 1
 -> λ 1
    λ λ 2
 -> λ λ 2
    λ λ 2 1 ((λ λ λ 3 1 2) 1)
 -> λ λ 2 1 ((λ λ λ 3 1 2) 1)
    λ λ 2 1
 -> λ λ 2 1
    λ λ 2 (2 (2 1))
 -> λ λ 2 (2 (2 1))
    λ λ λ λ 4 2 (3 2 1)
 -> λ λ λ λ 4 2 (3 2 1)
    λ λ λ λ 4 (3 2) 1
 -> λ λ λ λ 4 (3 2) 1
    λ λ λ 1 3 2
 -> λ λ λ 1 3 2
    λ (λ 1 λ λ 2) (1 λ (λ λ λ 1 3 2) ((λ 1 λ λ 1) 1) ((λ λ λ 2 (3 2 1)) ((λ 1 λ λ 1) 1)) ((λ λ λ 1 3 2) λ λ 1 λ λ 1))
 -> λ (λ 1 λ λ 2) (1 λ (λ λ λ 1 3 2) ((λ 1 λ λ 1) 1) ((λ λ λ 2 (3 2 1)) ((λ 1 λ λ 1) 1)) ((λ λ λ 1 3 2) λ λ 1 λ λ 1))
    λ (λ 1 λ λ 2) (1 λ (λ 1 λ λ 1) 1 ((λ λ λ 1 3 2) ((λ λ λ 2 (3 2 1)) ((λ 1 λ λ 2) 1)) λ λ 1) ((λ λ λ 1 3 2) ((λ 1 λ λ 2) 1) λ λ 2) ((λ λ λ 1 3 2) λ λ 1 λ λ 1))
 -> λ (λ 1 λ λ 2) (1 λ (λ 1 λ λ 1) 1 ((λ λ λ 1 3 2) ((λ λ λ 2 (3 2 1)) ((λ 1 λ λ 2) 1)) λ λ 1) ((λ λ λ 1 3 2) ((λ 1 λ λ 2) 1) λ λ 2) ((λ λ λ 1 3 2) λ λ 1 λ λ 1))
---
    λa.a
 -> λa.a
    λa.λb.a
 -> λa.λb.a
    λa.λb.ab((λc.λd.λe.ced)b)
 -> λa.λb.ab((λc.λd.λe.ced)b)
    λa.λb.ab
 -> λa.λb.ab
    λa.λb.a(a(ab))
 -> λa.λb.a(a(ab))
    λa.λb.λc.λd.ac(bcd)
 -> λa.λb.λc.λd.ac(bcd)
    λa.λb.λc.λd.a(bc)d
 -> λa.λb.λc.λd.a(bc)d
    λa.λb.λc.cab
 -> λa.λb.λc.cab
    λa.(λb.bλc.λd.c)(aλb.(λc.λd.λe.ecd)((λc.cλd.λe.e)b)((λc.λd.λe.d(cde))((λc.cλd.λe.e)b))((λb.λc.λd.dbc)λb.λc.cλb.λc.c))
 -> λa.(λb.bλc.λd.c)(aλb.(λc.λd.λe.ecd)((λc.cλd.λe.e)b)((λc.λd.λe.d(cde))((λc.cλd.λe.e)b))((λb.λc.λd.dbc)λb.λc.cλb.λc.c))
    λa.(λb.bλc.λd.c)(aλb.(λc.cλd.λe.e)b((λc.λd.λe.ecd)((λc.λd.λe.d(cde))((λc.cλd.λe.d)b))λc.λd.d)((λc.λd.λe.ecd)((λc.cλd.λe.d)b)λc.λd.c)((λb.λc.λd.dbc)λb.λc.cλb.λc.c))
 -> λa.(λb.bλc.λd.c)(aλb.(λc.cλd.λe.e)b((λc.λd.λe.ecd)((λc.λd.λe.d(cde))((λc.cλd.λe.d)b))λc.λd.d)((λc.λd.λe.ecd)((λc.cλd.λe.d)b)λc.λd.c)((λb.λc.λd.dbc)λb.λc.cλb.λc.c))
---
(λn.((λf.(λx.x x) (λx.f (x x))) (λc.λn.λm.λf.λx.(λd.(λn.n (λx.(λa.λb.b)) (λa.λb.a)) d ((λf.λx.x) f x) (f (c d m f x))) ((λm.λn.n (λn.λf.λx.n (λg.λh.h (g f)) (λu.x) (λu.u)) m) n m))) ((λn.λf.λx. f (n f x)) n))
λa.(λb.(λc.cc)λc.b(cc))λb.λc.λd.λe.λf.(λg.(λh.hλi.λj.λk.kλi.λj.i)g((λh.λi.i)ef)(e(bgdef)))((λg.λh.hλi.λj.λk.iλl.λm.m(lj)λl.kλl.lg)cd)((λb.λc.λd.c(bcd))a)
λa.(λb.(λc.cc)λc.b(cc))λb.λc.λd.λe.λf.(λg.(λh.hλi.λj.λk.kλl.λm.l)g((λh.λi.i)ef)(e(bgdef)))((λg.λh.hλi.λj.λk.iλl.λm.m(lj)λn.kλo.og)cd)((λg.λh.λi.h(ghi))a)
λa.(λb.(λc.cc)λc.b(cc))λbcdef.(λg.(λh.hλijk.kλlm.l)g((λhi.i)ef)(e(bgdef)))((λgh.hλijk.iλlm.m(lj)λn.kλo.og)cd)((λghi.h(ghi))a)

---- Reducing
λ (λ 2) λ 1  -β-> λ 1
---
(λ λ 2) λ 1 -β-> λ λ 1
---
λ (λ λ 2 (2 (2 (2 (2 (2 (2 (2 1)))))))) λ λ 2 (2 1)
 =β=> decimal 0 binary 0 hexa 0 using 26 ms for 510 reductions, 772 substitutions.

λ (λ λ 2 (2 (2 (2 (2 (2 (2 (2 (2 1))))))))) λ λ 2 (2 1)
 =β=> decimal 0 binary 0 hexa 0 using 14 ms for 1022 reductions, 1541 substitutions.

λ (λ λ 2 (2 (2 (2 (2 (2 (2 (2 (2 (2 1)))))))))) λ λ 2 (2 1)
 =β=> decimal 0 binary 0 hexa 0 using 39 ms for 2046 reductions, 3078 substitutions.

λ (λ λ 2 (2 (2 (2 (2 (2 (2 (2 (2 (2 (2 1))))))))))) λ λ 2 (2 1)
 =β=> decimal 0 binary 0 hexa 0 using 113 ms for 4094 reductions, 6151 substitutions.

λ (λ λ 2 (2 (2 (2 (2 (2 (2 (2 (2 (2 (2 (2 1)))))))))))) λ λ 2 (2 1)
 =β=> decimal 0 binary 0 hexa 0 using 339 ms for 8190 reductions, 12296 substitutions.

Terms(int) 58422

---- Logic
(not false)-> λ λ 2
(not true)-> λ λ 1
---
(xor true false)-> λ λ 2
(xor false true)-> λ λ 2
(xor false false)-> λ λ 1
(xor true true)-> λ λ 1
(notxor true false)-> λ λ 1
(notxor false true)-> λ λ 1
(notxor false false)-> λ λ 2
(notxor true true)-> λ λ 2

---- Arithmetic
(incr 1)-> λ λ 2 (2 1)
(decr 3)-> λ λ 2 (2 1)
(divByTwo 6)-> λ λ 2 (2 (2 1))
(isOdd 6)-> λ λ 1
(eq0 0)-> λ λ 2
(eq0 1)-> λ λ 1
---
(add 2 2)-> λ λ 2 (2 (2 (2 1)))
(mult 2 3)-> λ λ 2 (2 (2 (2 (2 (2 1)))))
(sub 3 5)-> λ λ 1
(sub 5 3)-> λ λ 2 (2 1)
(sub 3 3)-> λ λ 1
(lessOrEqual 3 5)-> λ λ 2
(lessOrEqual 5 3)-> λ λ 1
(lessOrEqual 3 3)-> λ λ 2

---- Alternance
λ 1 λ λ 2 (2 1) λ λ 2
λ 1 λ λ 2 (2 (2 1)) λ λ 1

---- Type assignmment
λ 1 1 : untyped
λ 1 : [o] -> [o]
λ λ 2 : [o] -> [f]
λ λ 1 : [o] -> [f]
λ λ λ 3 2 1 : [b] -> [b]
λ λ 2 1 : [f] -> [f]
λ λ 2 (2 1) : [f] -> [f]
λ λ λ 2 (3 2 1) : [n] -> [n]
λ λ λ λ 4 2 (3 2 1) : [b] -> [f -> b]
λ λ λ λ 4 (3 2) 1 : [b] -> [f -> b]
λ λ λ 3 1 2 : [b] -> [b]
λ λ 2 ((λ λ λ 3 1 2) 1) 1 : [b] -> [f]
λ λ λ 1 3 2 : [o] -> [b]

---- Couples
[ λ 1 , λ 1 ]
 : [f -> f -> o] -> [o]
[ λ λ 2 , λ λ 1 ]
 : [b -> b -> o] -> [o]
[ λ λ 1 , λ λ 2 ]
 : [b -> b -> o] -> [o]
[ λ λ 2 1 , λ λ 2 1 ]
 : [n -> n -> o] -> [o]
[ λ λ 2 , λ λ 2 1 ]
 : [b -> n -> o] -> [o]
[ λ λ 2 1 , λ λ 2 ]
 : [n -> b -> o] -> [o]

---- TypedLambda demonstration page end
1271 abstractions
4175 pairs
28015 leaves

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