algebra_tree.hvml

// Repeated Application
@rep(n f x) = ~ n !f !x {
  0: x
  p: !&0{f0 f1}=f (f0 @rep(p f1 x))
}

// Squared Application
@sqr(n f x) = ~ n !f !x {
  0: x
  p:!&0{p0 p1}=(+ p 1)
    !&0{fA f0}=f
    !&0{f1 f2}=fA
    @sqr((/ p0 2) λk(f0 (f1 k)) @rep((% p1 2) f2 x))
}

@N(a b) = λo λi λt (t (o a) (i b))
@L(x)   = x

//@view(&s) = ~&s {
  //0 : λx x
  //&p: λx (x λx#0{(@view(&p) x)} λx#1{(@view(&p) x)} λa λb [a b])
//}

@view(&s) = ~&s {
  0 : λx x
  &p: λx (x
    λx λt (t 0 (@view(&p) x))
    λx λt (t 1 (@view(&p) x))
    λa λb (a λaK λaV (b λbK λbV ~aK !aV !bV {
      0: #0{aV bV}
      p: #1{aV bV}
    })))
}

@inc(s) = ~s {
  0: λx x
  p: λx λO λI λT (x λx(I (@inc(p) x)) λx(O x) T)
}

@dec(s) = ~s {
  0: λx x
  p: λx λO λI λT (x λx(O x) λx(I (@dec(p) x)) T)
}

@zero = @N(@N(@N(7 7) @N(7 7)) @N(@N(7 7) @N(7 7)))
@main = (@view(3) (@sqr(5000 @inc(3) @zero)))

// 0 = #0(#0(#0__ #0__) #0(#0__ #0__))
// 1 = #1(#1(#1__ #0__) #0(#0__ #0__))
// 2 = #0(#1(#1__ #0__) #1(#1__ #0__))
// 3 = #1(#0(#1__ #1__) #1(#1__ #0__))
// 4 = #0(#0(#1__ #1__) #0(#1__ #1__))
// 5 = #1(#1(#0__ #1__) #0(#1__ #1__))
// 6 = #0(#1(#0__ #1__) #1(#0__ #1__))
// 7 = #1(#0(#0__ #0__) #1(#0__ #1__))
// 8 = #0(#0(#0__ #0__) #0(#0__ #0__))