Structurally Recursive Solver for Functions Closed Under Constant Zero, Succ, Double and Full (2^x - 1)

Unification-Test.fsx

//  Nerd sniped by Conor Mc Bride
//  https://github.com/pigworker/Samizdat/blob/main/Full.hs
//  Agda Proof - https://github.com/pigworker/Samizdat/tree/main/Full

//  I really have no idea what I'm doing here.

// The data type Fm is a syntax tree with nodes:
// V x = a variable reference
// Z   = zero (a canonical base value)
// D f = double the value represented by 'f'
// S f = successor of the value represented by 'f'
// F f = "full" function (2^n - 1 transformations) on 'f'
//
// Essentially, Fm represents expressions in a tiny arithmetic function language.
// Variables can stand for unknown values to be solved for.
//
// The code is basically doing unification in this arithmetic/function language.
// Unification: finding a substitution for variables that makes two terms equal.

open System

type Var = int
type Fm<'a> =
    | V of 'a  // Variable node
    | Z         // Zero
    | D of Fm<'a> // Double
    | S of Fm<'a> // Successor
    | F of Fm<'a> // Full (one less than a power of two)

// 2 ^ (x + 1 * 2) - 1 = y + 1
    
type Fm = Fm<Var>

// compareFm: Compare two Fm terms structurally.
// Alternative name: "compareTerms"
// Scenario: When implementing a solver, you may need to order terms to apply certain heuristics.
//           Also helps with deterministic unification steps.
let rec compareFm (a: Fm) (b: Fm) : int = 
    // Comparison by "tag" ensures a stable ordering of node types.
    // Then recursively compare sub-terms.
    let tagOrder = function
        | V _ -> 0
        | Z   -> 1
        | D _ -> 2
        | S _ -> 3
        | F _ -> 4

    let cmpTag = compare (tagOrder a) (tagOrder b)
    if cmpTag <> 0 then cmpTag else
        match a, b with
        | V x, V y -> compare x y
        | Z, Z -> 0
        | D f, D g -> compareFm f g
        | S f, S g -> compareFm f g
        | F f, F g -> compareFm f g
        | _ -> 0

// eqFm: Checks if two terms are structurally equal.
// Alternative name: "equalTerms"
// Scenario: Used extensively in unification to quickly detect when two terms match.
let eqFm (a: Fm) (b: Fm) = (compareFm a b = 0)

// db: "db" seems to perform a normalizing function focusing on doubling.
// It turns S-nested zeros into doubling or leaves others as D.
// Alternative name: "ensureEvenForm" or "toDoubleForm"
// Scenario: Might be used to push terms into a canonical form where successor chains are replaced by doubling where possible.
let rec db = function
    | Z -> Z
    | S f' -> S (S (db f')) // Twice successor becomes a pattern to represent even numbers
    | f -> D f              // Otherwise, represent via D if not a pure successor chain.

// fu: "fu" seems to apply a "full" transformation, representing 2^n - 1 forms.
// Alternative name: "fullForm"
// Scenario: Used to transform terms into a form where certain arithmetic properties (like representing a number as 2^n - 1) are standardized. Helpful in arithmetic unification.
let rec fu = function
    | Z -> Z
    | S f -> S (db (fu f))
    | f -> F f

// Store: A context for variable assignments and name supply.
// (Int * (Var * Fm) list): The integer is a "fresh variable" counter, and
// the list maps variables to their substituted forms.
// Alternative name: "Context" or "SubstitutionEnvironment"
// Scenario: During unification, you track what each variable stands for. The store is where you keep these mappings.
type Store = int * (Var * Fm) list

// va: Look up a variable in the store.
// Alternative name: "lookupVar"
// Scenario: When a variable is encountered, check if it's already been assigned a form.
let va (x: Var) ((_, xns): Store) =
    match List.tryFind (fun (y, _) -> y = x) xns with
    | Some (_, n) -> n
    | None -> V x

// nm: Normalization function that applies va, db, fu transformations.
// Alternative name: "normalizeTerm"
// Scenario: Before unification, you want both terms in a canonical form. nm applies context-based substitutions and normalizations to handle even/odd and full transformations.
let rec nm f (ga: Store) =
    match f with
    | V x -> va x ga
    | Z -> Z
    | S g -> S (nm g ga)
    | D g -> db (nm g ga)
    | F g -> fu (nm g ga)

// gro: Graft a substitution into the store.
// Alternative name: "extendSubstitution"
// Scenario: When unification decides that a variable must equal a certain term, 
// gro updates the store so that variable maps to that term and also updates other 
// substitutions.
let rec gro x f ((k, xns): Store): Store = 
    (k, (x, f) :: (List.map (fun (y, n) -> (y, sb x f n)) xns))

// sb: substitution in a term.
// Alternative name: "substituteTerm"
// Scenario: Replace all occurrences of variable x in a term with f.
and sb x f tm =
    match tm with
    | V y -> if x = y then f else V y
    | Z -> Z
    | S g -> S (sb x f g)
    | D g -> db (sb x f g)
    | F g -> fu (sb x f g)

// occ: Occur check. Does variable x occur in fm?
// Alternative name: "occursIn"
// Scenario: Avoid infinite regress in unification. If x occurs in a term 
// supposed to define x, that would create a cycle.
let occ x (fm: Fm) =
    let rec go fm =
        match fm with
        | V y -> (y = x)
        | Z -> false
        | S g -> go g
        | D g -> go g
        | F g -> go g
    go fm

// zee: Tries to unify something with Z (zero-like forms).
// Alternative name: "unifyWithZero"
// Scenario: After normalization, unify a term with zero if possible by extending the substitution or concluding impossibility.
let rec zee fm ga : option<Store> =
    match fm with
    | V x -> Some (gro x Z ga)   // Variable becomes zero
    | Z -> Some ga               // Already zero, no change
    | S _ -> None                // Can't unify with zero if S is at top
    | D f -> zee f ga            // Try to unify inside D
    | F f -> zee f ga            // Try to unify inside F

// suu: Handle successor-like unifications (S).
// Alternative name: "splitSuccessorTerm"
// Scenario: If we try to unify with a successor form, we must consider 
// if the other term can be broken down into something that matches after removing one S.
let rec suu fm ga : option<Fm * Store> =
    match fm with
    | V x ->
        let (k, xns) = ga
        // Introduce a new variable k and say: Vx = S(Vk)
        Some (V k, gro x (S (V k)) (k+1, xns))
    | Z -> None
    | S f -> Some (f, ga)
    | D f ->
        // If fm is D f, try to interpret it as an S-type form by processing f
        match suu f ga with
        | Some (g, ga') -> Some (S (db g), ga')
        | None -> None
    | F f ->
        // Similarly for F f
        match suu f ga with
        | Some (g, ga') -> Some (db (fu g), ga')
        | None -> None

// evn: Handle even forms (D).
// Alternative name: "handleEvenForm"
// Scenario: Some forms represent even numbers or double operations. 
//    evn tries to unify or transform them into a simpler form plus an updated store.
let rec evn fm ga : option<Fm * Store> =
    match fm with
    | V x ->
        let (k, xns) = ga
        Some (V k, gro x (D (V k)) (k+1, xns))
    | Z ->
        Some (Z, ga)
    | S f ->
        // If S f is encountered in an even context, try to break it down with ood (odd)
        match ood f ga with
        | Some (g, ga') -> Some (S g, ga')
        | None -> None
    | D f -> 
        Some (f, ga)
    | F f ->
        // If we can unify f with zero (zee), then result is (Z, ga)
        match zee f ga with
        | Some ga' -> Some (Z, ga')
        | None -> None

// ood: Handle odd forms.
// Alternative name: "handleOddForm"
// Scenario: Similar to evn, but for odd contexts. Distinguishes terms that must 
// represent odd numbers or forms that can't be broken down further.
and ood fm ga : option<Fm * Store> =
    match fm with
    | V x ->
        let (k, xns) = ga
        Some (V k, gro x (S (D (V k))) (k+1, xns))
    | Z -> None
    | S f ->
        match evn f ga with
        | Some (g, ga') -> Some (g, ga')
        | None -> None
    | D _ -> None
    | F f ->
        match suu f ga with
        | Some (g, ga') -> Some (fu g, ga')
        | None -> None

// unify: The core unification algorithm.
// Alternative name: "unifyTerms"
// Scenario: Given two terms f and g and a context ga, find a store (substitution) 
//           that makes f and g identical. This uses normalization (nm), occur 
//           checks, zero/unfolding strategies (zee), successor splitting (suu), 
//           even/odd decomposition (evn/ood) to produce a substitution or fail.
let rec unify f g ga : option<Store> =
    let rec go f g =
        if eqFm f g then
            Some ga
        else
            let c = compareFm f g
            // Ensure we always unify the "smaller" term first for determinism
            if c > 0 then go g f else
                match f with
                | V x ->
                    // If x doesn't occur in g, we can unify by substituting x = g
                    // Else try zee g ga to see if we can unify g with zero form
                    if not (occ x g) then Some (gro x g ga) else zee g ga
                | Z ->
                    zee g ga
                | D f' ->
                    // For D forms, try evn g ga
                    match evn g ga with
                    | Some (h, ga') -> unify f' h ga'
                    | None -> None
                | S f' ->
                    // For S forms, try suu g ga
                    match suu g ga with
                    | Some (h, ga') -> unify f' h ga'
                    | None -> None
                | F f' ->
                    // For F forms, both must be F forms to unify
                    match g with
                    | F g' -> go f' g'
                    | _ -> None
    go (nm f ga) (nm g ga)

// normalize and fmToString: Convert a term to a human-friendly string form.
// Alternative name: "termToString"
// Scenario: Useful for debugging or showing the end result of a unification. 
// The internal logic tries to present arithmetic forms in a more comprehensible way (like showing successors and doubles as numbers).

let rec normalize (f: Fm) (ga: Store) = nm f ga

let rec fmToString (f: Fm) =
    let f' = normalize f (0, [])
    let rec go f =
        match f with
        | V x -> "V" + x.ToString()
        | Z -> "0"
        | S f' -> mo 1 f'
        | D f' -> moD 1 f'
        | F f' -> "[" + go f' + "]"
    and mo k f = 
        match f with
        | Z -> k.ToString()
        | S f' -> mo (k+1) f'
        | _ -> k.ToString() + "+" + go f
    and moD k f =
        match f with
        | D f' -> moD (k+1) f'
        | _ ->
            let po i =
                let a = (2I ** (int i)).ToString()
                a
            po k + "*" + go f
    go f'



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 Pairing


let rec natToFm maxVars n  = 
    let natToFm n = natToFm maxVars n
    if n = 0I then Z
    else if n > 0I && n < maxVars + 1I then
        V(int (n))
    else
        let n = n - (maxVars + 1I)
        let (d, r) = bigint.DivRem(n, 3)
        match int r with
        | 0 -> F (natToFm d)
        | 1 -> D (natToFm d)
        | 2 -> S (natToFm d)

//let rec natToFm n = 
//    if n = 0I then Z
//    else
//        let n = n - 1I
//        let (d, r) = bigint.DivRem(n, 3)
//        match int r with
//        | 0 -> F (natToFm d)
//        | 1 -> D (natToFm d)
//        | 2 -> S (natToFm d)
        
//let rec termCount = function
//    | Z -> 1
//    | S f' -> 1 + termCount f'
//    | D f' -> 1 + termCount f'
//    | F f' -> 1 + termCount f'
//
//let rec calc = function
//    | Z -> 0
//    | S f' -> 1 + calc f'
//    | D f' -> 2 * calc f'
//    | F f' -> int(Math.Pow(2, float((calc f')))) - 1

let rec maxVar = function
    | V x -> x + 1
    | Z -> 0
    | S f' -> maxVar f'
    | D f' -> maxVar f'
    | F f' -> maxVar f'

//let exprs = [ 0I..20I ] |> List.map (natToFm 1I)
let expr n = natToFm 1I n

//let quickUnify a b = 
//    let r = unify a b (1, [])
//    match r with
//    | Some(_, (v1, t)::_) -> $"{a} == {b} when V 1 = {t}"
//    | Some(_, []) -> $"{a} == {b}"
//    | _ -> $"{a} != {b}"    
//
//quickUnify (S (F (D (V 0)))) (D (F (V 0))) |> Dump

let testUnify x y = 
    let a = expr x
    let b = expr y
    let result = try 
                    if x <= y then "" 
                    else
                        let lastVar = (max (maxVar a) (maxVar b))
                        let r = unify a b (lastVar, [])
                        let toForm (v, t) = $"V {v} = {t}"
                        match r with
                        | Some(_, l) ->
                            let l = l |> List.filter (fun (v, t) -> v <= lastVar)
                            match l with
                            | [] -> "" // $"{a} == {b}"
                            | l  -> $"{a} == {b} when {l |> List.truncate lastVar |> List.map toForm}"
                        | None -> $""
                 with ex -> $"{ex}"
    result

let c = 20
let arr2d = Array2D.init c c (fun x y -> testUnify x y)
             |> Array2D.map (sprintf "%s")

arr2d.Dump()