A Gödelian Encoding for Tree Calculus

tree-calculus.fsx

//  The irony of this snippet is that Tree Calculus, unlike Lambda Calculus, is a 
//  system that was designed to be reflective so one doesn't have to resort to things
//  like Gödelian numbering systems or other schemes in order for it to reason about
//  its own programs.

//  But seeing how I know little to nothing about Tree Calculus, I figured this would be 
//  an interesting way to explore it.

//  Interestingly enough, this snippet was written one month before reading this post:
//  https://github.com/barry-jay-personal/blog/blob/main/2025-01-06-diagonal.md


type T = 
    | Leaf
    | Stem of T
    | Fork of T * T
with
    member this.ToDump() = sprintf "%A" this
    
//  Left-hand sides and the combinators that inspired them
//  AAyx = y            (K)
//  A(Ax)yz = yz(xz)    (S)
//  A(Awx)yz = zwx      (F)

//  Notice
//  K deletes the third argument
//  S duplicate the third argument
//  F decomposes the first argument to expose its branches
//  These rules will prove to be enough to represent the calculi that inspired them.
    
let rec apply a b = 
    match a with
    | Leaf                     -> Stem b
    | Stem a                   -> Fork (a, b)
    | Fork (Leaf, a)           -> a
    | Fork (Stem a1, a2)       -> apply (apply a1 b) (apply a2 b)
    | Fork (Fork (a1, a2), a3) ->
        match b with
        | Leaf -> a1
        | Stem u -> apply a2 u
        | Fork (u, v) -> apply (apply a3 u) v

// K = AA
// Kyz = AAyz = y
let K = apply Leaf Leaf
// I = A(AA)(AA)
// Ix = A(AA)(AA)x = AAx(Ax) = x
let I = apply (apply Leaf K) K

// D = A(AA)(AAA)
// Dxyz = A(AA)(AAA)xyz
//      = AAAx(Ax)yz
//      = A(Ax)yz
//      = yz(xz)
        

let rec depth = 
    function
        | Leaf -> 0
        | Stem t -> 1 + depth t
        | Fork (t1, t2) -> 1 + max (depth t1) (depth t2)

//  Page 30

//  M^k(N) = M(M...(MN)...) where M is applied K times
//  We can identify the natural number K with t^k t
let rec encode (n:int) = 
    if n = 0 then Leaf
    else Stem (encode (n - 1))
    

module Nat = begin

    open System.Numerics

    //type nat = int64
    type nat = bigint
    
    let inline nat(n: int) = bigint(n)

    let sqrt (x: bigint): bigint = 
        if x <= 1I then x else
        let rec iter (guess: bigint): bigint =
            let next = (guess + x / guess) >>> 1
            if next < guess then
                iter next
            else
                guess
        iter (x / 2I)

end

//  Matthew Szudzick's Elegant Pairing
module Pairing = begin

    open Nat

    //  Unpair two integers
    let unpair (n: nat): nat * nat = 
        let s = sqrt n
        let s2 = s * s
        if n - s2 < s then (n - s2, s) else (s, n - s2 - s)

    //  Pair two integers
    let pair (a: nat, b: nat): nat =
        if a < b then b * b + a else a * a + a + b
    
end


open Nat
open Pairing

let rec natToTerm (n: nat) = 
    if n = 0I then Leaf
    else
        //
        let n = n - 1I
        let option = n.IsEven  // Even numbers create Stems, odd Forks
        let d = n >>> 1     //  Divide by 2
        if option then
            Stem (natToTerm d)
        else
            let (a, b) = unpair d  //  Use 
            Fork (natToTerm a, natToTerm b)
            
let rec termToNat (t: T): nat = 
    match t with
    | Leaf -> 0I
    | Stem t -> 1I + (termToNat t <<< 1)
    | Fork (a, b) -> 1I + ((pair (termToNat a, termToNat b) <<< 1) + 1I)

let testEncodeDecode() = 
    for n in 0I..100000I do
        assert(termToNat(natToTerm(n)) = n)
    printfn "It looks like a bijection?!?!?!"
    
//  testEncodeDecode()
        
let terms = [ for n in 0I..100I do
                    let t = natToTerm n
                    let d = depth t
                    d, n, t ]

//  Let's look at the terms
for t in (terms |> List.sort) do
    printfn "%A" t