# CL Binary tree
We'll define here the free algebra of trees using the concepts already outlined in [Foundations of the gerku language](https://hackmd.io/@qeHlwm2zQ62-hoUHOp_E5w/ry6Nu0GYK) whose contents the reader is supposed to be familiar with and won't be repeated here.

## Data type

The Data type of binary trees of integers has two constructors:

𝓓 = ⟨{ℕ,𝕋}, {bic:ℕ⭢𝕋⭢𝕋⭢𝕋 , empb:𝕋 }⟩

such that

`empb`: returns a binary tree with 0 nodes (an *empty* binary tree)
`bic` : takes a natural 𝓃 and two binary trees 𝓁 and 𝓇 and returns a binary tree whose root is labeled with 𝓃 and has 𝓁 and 𝓇, rispectively as left and right children.

Example:

        1
       / \ 
      2   3

bic(1, bic(2,empb,empb), bic(3,empb,empb))

## Iterative functions on binary tree

   𝑓(empb) = ℎ₀
   𝑓(bic(n,l,r)) = ℎ₁(a,𝑓(l),𝑓(r))

Examples.
The function `sumb:𝕋⭢ℕ` visit the tree and sums up all the integers in the nodes:

   sumb(empb) = 0
   sumb(bic(n,l,r)) = add(n, add(sumb(l), sumb(r)))

The function `preord:` 𝕋⭢𝕃^ℕ returns a list of naturals whose elements are the numbers in the tree nodes visited in preorder:

   preord(empb) = nil
   preord(bic(n,l,r)) = cons(n,cat(preord(l),preord(r)))

## Combinators for binary trees constructurs

  𝐞𝐦𝐩𝐛 𝑏 𝑒 = 𝑒
  𝐛𝐢𝐜 𝑛 𝑙 𝑟 𝑏 𝑒 = 𝑏 𝑛 (𝑙 𝑏 𝑒) (𝑟 𝑏 𝑒)

With this definition for the constructurs, applying a tree to a three arguments function (and an auxiliary argument), will result in visiting the tree depth-first and applying the function to all the nodes (i.e. evaluating the tree in post order):

        1
       / \ 
      2   3

𝐛𝐢𝐜 1 (𝐛𝐢𝐜 2 𝐞𝐦𝐩𝐛 𝐞𝐦𝐩𝐛) (𝐛𝐢𝐜 3 𝐞𝐦𝐩𝐛 𝐞𝐦𝐩𝐛) F X 
  
= F 1 (𝐛𝐢𝐜 2 𝐞𝐦𝐩𝐛 𝐞𝐦𝐩𝐛 F X) (𝐛𝐢𝐜 3 𝐞𝐦𝐩𝐛 𝐞𝐦𝐩𝐛 F X) 
= F 1 (F 2 (𝐞𝐦𝐩𝐛 F X) (𝐞𝐦𝐩𝐛 F X)) (F 3 (𝐞𝐦𝐩𝐛 F X) (𝐞𝐦𝐩𝐛 F X))
= F 1 (F 2 X X) (F 3 X X)
  

## Combinators for the function sumb

We first have to determine the functions ℎ₀ and ℎ₁:

   sumb(empb) = 0  
   sumb(bic(n,l,r)) = add(n, add(sumb(l), sumb(r)))

   𝐬𝐮𝐦𝐛 𝐞𝐦𝐩𝐛 = 𝐇₀ = 0 = 𝐊 
   𝐬𝐮𝐦𝐛 𝐛𝐢𝐜 𝑛 𝑙 𝑟 = 𝐇₁ 𝑛 (𝐬𝐮𝐦𝐛 𝑙) (𝐬𝐮𝐦𝐛 𝑟) =
                 = 𝐚𝐝𝐝 𝑛 (𝐚𝐝𝐝 (𝐬𝐮𝐦𝐛 𝑙) (𝐬𝐮𝐦𝐛 𝑟)) =
                 = Q 𝐚𝐝𝐝 n (𝐬𝐮𝐦𝐛 𝑙) (𝐬𝐮𝐦𝐛 𝑟)
   
   ⇒  𝐇₁ = Q 𝐚𝐝𝐝
   
   with Q defined as:
   
   Q f a b c = f a (f b c) 
             = 𝐁 (f a) (f b) c
             = 𝐁 (𝐁 (f a)) f b c
             = 𝐁 (𝐁 𝐁 f a) f b c
             = 𝐁 𝐁 (𝐁 𝐁 f) a f b c
             = 𝐁 (𝐁 𝐁) (𝐁 𝐁) f a f b c
             = 𝐖 𝐁 (𝐁 𝐁) f a f b c
             = 𝐂 (𝐖 𝐁 (𝐁 𝐁) f) f a b c
             = 𝐁 𝐂 (𝐖 𝐁 (𝐁 𝐁)) f f a b c
             = 𝐖 (𝐁 𝐂 (𝐖 𝐁 (𝐁 𝐁))) f a b c
   
   ⇒ Q = 𝐖 (𝐁 𝐂 (𝐖 𝐁 (𝐁 𝐁)))
   ⇒ 𝐇₁ = 𝐖 (𝐁 𝐂 (𝐖 𝐁 (𝐁 𝐁))) 𝐚𝐝𝐝
   
   
   𝐬𝐮𝐦𝐛 𝑇 = 𝑇 𝐇₁ 𝐇₀
          = 𝑇 (𝐖 (𝐁 𝐂 (𝐖 𝐁 (𝐁 𝐁))) 𝐚𝐝𝐝) 𝐊

## Combinators for the function preord
Left as an exercise to the reader :smile: