The Godelian Toolkit - Generating Imperative Programs

godelian-auto-constructor.fsx

////////////////////////////////////////////////////////////////////////
///  The Gödelian Toolkit
////////////////////////////////////////////////////////////////////////

module Nat = 
    type Nat = bigint
        
    let sqrt (z: bigint) : bigint =
        if z < 0I then
            invalidArg "z" "Cannot compute the square root of a negative number"
        elif z = 0I then
            0I
        else
            let rec newtonRaphson (x: bigint) : bigint =
                let nextX = (x + z / x) / 2I
                if nextX >= x then x else newtonRaphson nextX

            newtonRaphson z

module MonoPairing = 
    open Nat
    
    let pair (a: Nat) (b: Nat) = 
        if a < b then b * b + a else a * a + a + b
        
    let unpair (n: Nat) = 
        let s = sqrt n
        if n - s * s < s then (n - s * s, s) else (s, n - s * s - s)
        
module Mappings = 
    open Nat

    let nat2pair (z: bigint) : bigint * bigint = MonoPairing.unpair z
        
    let nat2orderedpair (z: bigint) : bigint * bigint =
        let (a, b) = nat2pair z
        (a, a + b)
        
    let pair2ordered (a: bigint, b: bigint) = 
        (a, a + b + 1I)
        
    let nat2pairWithId (skip: bigint) (z: bigint) : bigint * bigint = 
        if z < skip then (z, z)
        else 
            let (a, b) = nat2pair (z - skip)
            (a + skip, b + skip)
            
    let skip (i: bigint) (n: bigint): bigint = n + i

    let nat2orderedPairWithId (z: bigint) : bigint * bigint = 
        let (a, b) = nat2pair z |> pair2ordered
        (a + 1I, b + 1I)
        
        
    let nat2set (n: Nat): Set<Nat> =
        let rec nat2exps n x =
            if n = 0I then []
            else
                let xs = nat2exps (n / 2I) (x + 1I)
                if n % 2I = 0I then xs else x::xs
        (if n >= 0I then nat2exps n 0I else []) |> Set.ofList
        
    let nat2orderedlist (n: Nat) = 
        let s = nat2set n |> Set.toSeq
        [ for (i, a) in Seq.indexed s -> a - (bigint i) ]
        
    let rec nat2unorderedlist (n: Nat) =
        if n = 0I then []
        else
            let (b, a) = nat2pair n
            a :: nat2unorderedlist b

module GodelianTooklit =

    open Nat

    let memoizeRec f =
        let cache = System.Collections.Concurrent.ConcurrentDictionary()
        let rec recF x =
            cache.GetOrAdd(x, lazy f recF x).Value
        recF    


    // A constructor for an infinite domain
    //type InfCtor<'T> = InfCtor of ctor: (bigint -> 'T)
    type InfCtor<'T> = (bigint -> 'T)
    
    type FinCtor<'T> = FindCtor of size: bigint * ctor: (bigint -> 'T)

    let sqrt (z: bigint) : bigint =
        if z < 0I then
            invalidArg "z" "Cannot compute the square root of a negative number"
        elif z = 0I then
            0I
        else
            let rec newtonRaphson (x: bigint) : bigint =
                let nextX = (x + z / x) / 2I
                if nextX >= x then x else newtonRaphson nextX

            newtonRaphson z

    let encodePair (z: bigint) : bigint * bigint = MonoPairing.unpair z

    let (|Pair|) = encodePair

    let decodePair (a: bigint, b: bigint) : bigint = MonoPairing.pair a b


    let combineChoices (functionList: ((InfCtor<'a>) -> InfCtor<'a>) list) (n: bigint): 'a =
        let length = bigint (List.length functionList)

        let rec chooseFunction n =
            let (d, r) = bigint.DivRem(n, length)
            let f = functionList.[int (r)]
            f chooseFunction d

        chooseFunction n


    let combineChoicesWithContext (getOptions: 'a -> (('a -> InfCtor<'b>) -> InfCtor<'b>) list) (initialContext: 'a): InfCtor<'b> =

        //  We add a parameter that now includes context
        let rec chooseFunction context n =
            let functionList = getOptions (context)
            let length = bigint (List.length functionList)
            let (d, r) = bigint.DivRem(n, length)
            let f = functionList.[int (r)]
            f chooseFunction d

        chooseFunction initialContext


    let tryFiniteFirst (numberOfFiniteOptions: int) (finiteConstuctor: int -> 'b) (infiniteConstructors: ('a -> InfCtor<'b>) list) =
        let numberOfFiniteOptions = numberOfFiniteOptions - 1
        let length = bigint (List.length infiniteConstructors)

        if numberOfFiniteOptions >= 0 then
            [ (fun enc n ->
                  if n <= (bigint numberOfFiniteOptions) then
                      finiteConstuctor (int n)
                  else
                      let n = n - (bigint (numberOfFiniteOptions + 1))
                      let (d, r) = bigint.DivRem(n, length)
                      let f = infiniteConstructors.[int r]
                      f enc d) ]
        else
            infiniteConstructors


module MetaFSharp = 
    
    open FSharp.Reflection
    open GodelianTooklit
    
    
        
    /// Given an integer and a count, decode the integer into a list of ‘count’ integers
    let rec decodeParts (n: bigint) (k: int) : bigint list =
        if k <= 0 then []
        elif k = 1 then [n]
        else
            let (a, b) = encodePair n
            a :: decodeParts b (k - 1)
            
    //  Convert a bigint to a variable name using letters
    //  a, b, ..., aa, ab, ..., ba, bb, ...
    let toVarName (n: bigint): string = 
            let rec toVarName' n acc =
                if n < 0I then acc
                else
                    let charCode = int (n % 26I) + int 'a'
                    let newChar = char charCode
                    toVarName' (n / 26I - 1I) (string newChar + acc)
            toVarName' n ""
            
    /// Recursively build a Gödelian constructor for any supported type.
    /// The returned function takes a bigint and produces an instance boxed as obj.
    let createGodelianConstructorForType (recMake: Type -> InfCtor<'obj>) (t: Type) : (InfCtor<'obj>) =
        if t = typeof<string> then
            fun n -> box(toVarName(n))
        else if t = typeof<int> then
            fun n -> box (int n)
        elif t = typeof<bool> then
            // For booleans, we might use even/odd as false/true.
            fun n -> box ((n % 2I) = 0I)
        elif t = typeof<bigint> then
            fun n -> box n
        elif FSharpType.IsUnion(t) then
            // For each union case, create a constructor function that uses the Gödelian
            // encoding to “fill in” its fields.
            let caseConstructors = 
                lazy
                    // For union types, enumerate the union cases.
                    let cases = FSharpType.GetUnionCases(t)
                    cases
                    |> Array.map (fun unionCase ->
                        let fields = unionCase.GetFields()
                        let fieldConstructors = fields |> Array.map (fun f -> recMake f.PropertyType)
                        fun (n: bigint) ->
                            if fieldConstructors.Length = 0 then
                                // Nullary case: no fields.
                                FSharpValue.MakeUnion(unionCase, [||])
                            elif fieldConstructors.Length = 1 then
                                // Single field: pass the entire number.
                                let fieldVal = fieldConstructors.[0] n
                                FSharpValue.MakeUnion(unionCase, [| fieldVal |])
                            else
                                // Multiple fields: split n into as many parts as needed.
                                let parts = decodeParts n fieldConstructors.Length
                                let fieldVals =
                                    fieldConstructors
                                    |> Array.mapi (fun i cons -> cons parts.[i])
                                FSharpValue.MakeUnion(unionCase, fieldVals)
                    )
            fun (n: bigint) ->
                let caseConstructors = caseConstructors.Value
                // Use the input number to choose the union case.
                let len = bigint (Array.length caseConstructors)
                let (d, r) = bigint.DivRem(n, len)
                // d is passed into the chosen case’s constructor for its field(s)
                caseConstructors.[int r] d
        elif FSharpType.IsRecord(t) then
            // For records, build a constructor that decodes each field.
            
            let fieldConstructors = 
                lazy 
                    let fields = FSharpType.GetRecordFields(t)
                    fields |> Array.map (fun f -> recMake f.PropertyType)
            fun (n: bigint) ->
                let fieldConstructors = fieldConstructors.Value
                if fieldConstructors.Length = 0 then
                    FSharpValue.MakeRecord(t, [||])
                elif fieldConstructors.Length = 1 then
                    let fieldVal = fieldConstructors.[0] n
                    FSharpValue.MakeRecord(t, [| fieldVal |])
                else
                    let parts = decodeParts n fieldConstructors.Length
                    let fieldVals =
                        fieldConstructors
                        |> Array.mapi (fun i cons -> cons parts.[i])
                    FSharpValue.MakeRecord(t, fieldVals)
        else
            failwithf "Type %A is not supported by the Godelian constructor" t



    let makeConstructor = memoizeRec createGodelianConstructorForType

    /// The public API: automatically create a Gödelian constructor for type 'T.
    let createGodelianConstructorFor<'T> () : bigint -> 'T =        
        let cons = makeConstructor(typeof<'T>)
        fun n -> cons n |> unbox<'T>        

open GodelianTooklit

    
open MetaFSharp
    
module Printer =

    open System

    type Writer =
        inherit IDisposable

        abstract Write: string -> unit

    type Printer =
        abstract Line: int
        abstract Column: int
        abstract PushIndentation: unit -> unit
        abstract PopIndentation: unit -> unit
        abstract Print: string -> unit
        abstract PrintNewLine: unit -> unit

    type PrinterImpl(writer: Writer, ?indent: string) =
        let indentSpaces = defaultArg indent "    "
        let builder = Text.StringBuilder()
        let mutable indent = 0
        let mutable line = 1
        let mutable column = 0

        member _.Flush() =
                if builder.Length > 0 then
                    writer.Write(builder.ToString())
                    builder.Clear() |> ignore

        interface IDisposable with
            member _.Dispose() = writer.Dispose()

        interface Printer with
            member _.Line = line
            member _.Column = column

            member _.PrintNewLine() =
                builder.AppendLine() |> ignore
                line <- line + 1
                column <- 0

            member _.PushIndentation() = indent <- indent + 1

            member _.PopIndentation() =
                if indent > 0 then
                    indent <- indent - 1

            member _.Print(str: string) =
                if not (String.IsNullOrEmpty(str)) then

                    if column = 0 then
                        let indent = String.replicate indent indentSpaces
                        builder.Append(indent) |> ignore
                        column <- indent.Length

                    builder.Append(str) |> ignore
                    column <- column + str.Length



module Example1 = 
    
    type Term = 
        | Var of int
        | Lambda of Term
        | App of Term * Term


    let naiveConstructor: bigint -> Term =
        combineChoices
            [ fun enc n -> Var(int(n))
              fun enc (Pair(name, body)) -> Lambda(enc body)
              fun enc (Pair(l, r)) -> App(enc l, enc r) ]
              
    //for i in 0I..10I do
    //   printfn "%A - %A" i (naiveConstructor i)

//  We get this output
//0 - Var 0
//1 - Lambda (Var 0)
//2 - App (Var 0, Var 0)
//3 - Var 1
//4 - Lambda (Lambda (Var 0))
//5 - App (Var 0, Lambda (Var 0))
//6 - Var 2
//7 - Lambda (Lambda (Var 0))
//8 - App (Lambda (Var 0), Lambda (Var 0))
//9 - Var 3
//10 - Lambda (Var 0)

module Example2 = 

    //  Consider this language
    type Term = 
        | Value of bigint
        | Add of Term * Term
        | Mul of Term * Term
    with
        override this.ToString() = 
            match this with
            | Value b -> sprintf "%A" b
            | Add (t1, t2) -> sprintf "(%O + %O)" t1 t2
            | Mul (t1, t2) -> sprintf "(%O * %O)" t1 t2
    

    //  Now, let's see what we can do to implement it for this...
    let pick = createGodelianConstructorFor<Term>()

    //  When we sample our terms, we see we end up creating a lot of expressions
    //  that evaluate to zero while we count numbers

    for i in 0I..100I do
       printfn "//  %A - %s" i ((pick i).ToString())

    //  0 - 0
    //  1 - (0 + 0)
    //  2 - (0 * 0)
    //  3 - 1
    //  4 - (0 + (0 + 0))
    //  5 - (0 * (0 + 0))
    //  6 - 2
    //  7 - ((0 + 0) + 0)
    //  8 - ((0 + 0) * 0)
    //  9 - 3
    //  10 - ((0 + 0) + (0 + 0))
    //  11 - ((0 + 0) * (0 + 0))
    //  12 - 4
    //  13 - (0 + (0 * 0))
    //  14 - (0 * (0 * 0))
    //  15 - 5
    //  16 - ((0 + 0) + (0 * 0))
    //  17 - ((0 + 0) * (0 * 0))
    //  18 - 6
    //  19 - ((0 * 0) + 0)
    //  20 - ((0 * 0) * 0)
    //  21 - 7
    //  22 - ((0 * 0) + (0 + 0))
    //  23 - ((0 * 0) * (0 + 0))
    //  24 - 8
    //  25 - ((0 * 0) + (0 * 0))
    //  26 - ((0 * 0) * (0 * 0))
    //  27 - 9
    //  28 - (0 + 1)    
    
    //  What we want to do is create an algebraic specification for this language that tightens the
    //  space so we're not creating these duplicate and redundant terms in the first place using 
    //  algebraic rules like so:
    
    //  0 + a = a                  //  0 is the identity
    //  a + b = b + a              //  Addition is commutative
    //  (a + b) + c = a + (b + c)  //  Addition is associative
    //  
    //  0 * a = 0                  //  0 is ????  for multiplication
    //  1 * a = a                  //  1 is the identity for multiplication
    //  a * b = b + a              //  Multiplication is commutative
    //  (a * b) * c = a * (b * c)  //  Multiplication is associative
    //  
    //  The OBJ and Maude programming languages have built in features that can easily apply these
    //  rules to constructors.  When terms are constructed, they are automatically reduced to their 
    //  normal form.
    //
    //  For example, commutivity implies the thing reduce to a form where the left component is always
    //  less than the right component.
    //
    //  A non-associative, non-commutative binary operation can be used to construct a binary tree 
    //  whereas an associative, non-commutative binary operation can be used to construct a list.
    //  Adding commutivity to the list turns the list into an ordered list, resembling a multiset.
    //  If one defines idempotence as (a * a = a), that multiset turns into an ordered list with 
    //  distinct elements which reflects a set.
    //
    //  I want you to consider how the above functions in the Mappings module, like nat2set and pair2ordered,
    //  play a role in creating a tighter bijection.  
    //
    //  Let's consider a number of different ways to approach this:
    //
    //  1. We could annotate types with attributes.
    //  2. Rather than createGodelianConstructorFor returning a (bigint -> 'T) function, we could
    //     return an object that would allow us to further refine construction:
    //
    //     For example:
    //
    //     let ctor = createGodelianConstructorFor<Term>()
    //                  .MarkCommutative(Add)
    //                  .HasIdentity(Add, 0)
    //  3. Ideally, it would be cool to leverage expressions to define these rules, for example:
    //
    //     let ctor = createGodelianConstructorFor<Term>()
    //                  .Refine(fun (a) -> Add(a, a) = a)
    //                  .Refine(fun (a, b) -> Add(a, b) = Add(b, a))
    //
    //     But I don't know how to go about beginning to implement that.  I feel like need to deeply understand
    //     OBJ / Maude and Instutions to begin to approach it.
    //  
    //  I'm not thrilled about the above suggestions and I'm open to other ideas, but I'd like to explore
    //  how to approach this problem.
    
    
    



module Example3 = 

    type expression =
      | Variable of int (* a variable *)
      | Numeral of int (* integer constant *)
      | Plus of expression * expression  (* addition [e1 + e2] *)
      //| Minus of expression * expression (* difference [e1 - e2] *)
      //| Times of expression * expression (* product [e1 * e2] *)
      //| Divide of expression * expression (* quotient [e1 / e2] *)
      //| Remainder of expression * expression (* remainder [e1 % e2] *)

    type boolean =
      | True (* constant [true] *)
      | False (* constant [false] *)
      | Equal of expression * expression (* equal [e1 = e2] *)
      | Less of expression * expression (* less than [e1 < e2] *)
      | And of boolean * boolean (* conjunction [b1 and b2] *)
      | Or of boolean * boolean (* disjunction [b1 or b2] *)
      | Not of boolean (* negation [not b] *)

    type command =
      //| Skip (* no operation [skip] *)
      //| New of string * expression * command (* variable declaration [new x := e in c] *)
      //| Print of expression (* print expression [print e] *)
      | Assign of string * expression (* assign a variable [x := e] *)
      | Sequence of command * command (* sequence commands [c1 ; c2] *)
      | While of boolean * command (* loop [while b do c done] *)
      | Conditional of boolean * command * command (* conditional [if b then c1 else c2 end] *)


    let rec printCommand (p: Printer.Printer) (c:command) : unit = 
        //  Let's print the above commands to resemble that of a language that
        //  resembles JavaScript where we don't have to declare variables before we use them
                match c with
                | Assign(var, expr) ->
                    p.Print(var)
                    p.Print(" = ")
                    printExpression expr p
                    p.Print(";")
                | Sequence(c1, c2) ->
                    printCommand p c1
                    p.PrintNewLine()
                    printCommand p c2
                | While(cond, body) ->
                    p.Print("while (")
                    printBoolean cond p
                    p.Print(") {")
                    p.PushIndentation()
                    p.PrintNewLine()
                    printCommand p body
                    p.PopIndentation()
                    p.PrintNewLine()
                    p.Print("}")
                | Conditional(cond, thenCmd, elseCmd) ->
                    p.Print("if (")
                    printBoolean cond p
                    p.Print(") {")
                    p.PushIndentation()
                    p.PrintNewLine()
                    printCommand p thenCmd
                    p.PopIndentation()
                    p.PrintNewLine()
                    p.Print("} else {")
                    p.PushIndentation()
                    p.PrintNewLine()
                    printCommand p elseCmd
                    p.PopIndentation()
                    p.PrintNewLine()
                    p.Print("}")
        
    and printExpression (e: expression) (p: Printer.Printer): unit =
        match e with
        | Variable v -> p.Print(sprintf "x%d" v)
        | Numeral n -> p.Print(sprintf "%d" n)
        | Plus(e1, e2) ->
            printExpression e1 p
            p.Print(" + ")
            printExpression e2 p

    and printBoolean (b: boolean) (p: Printer.Printer): unit =
        match b with
        | True -> p.Print("true")
        | False -> p.Print("false")
        | Equal(e1, e2) ->
            printExpression e1 p
            p.Print(" == ")
            printExpression e2 p
        | Less(e1, e2) ->
            printExpression e1 p
            p.Print(" < ")
            printExpression e2 p
        | And(b1, b2) ->
            printBoolean b1 p
            p.Print(" && ")
            printBoolean b2 p
        | Or(b1, b2) ->
            printBoolean b1 p
            p.Print(" || ")
            printBoolean b2 p
        | Not(b) ->
            p.Print("!")
            printBoolean b p
        
        
    

    //  Now, let's see what we can do to implement it for this...
    let pick = createGodelianConstructorFor<command>()

    type ConsoleWriter() = 
        interface Printer.Writer with
            member _.Write(s: string) = Console.Write(s)
        interface IDisposable with
            member _.Dispose() = ()
    
    let printer = Printer.PrinterImpl(ConsoleWriter())  // :> Printer.Printer

    pick 12398723498732423409824232498723498734I |> printCommand printer
    
    printer.Flush()

//  Prints the following
//
//  while (x10 == x0 + x0 + x0 + x0 || false || true && false || true && !false) {
//    if (478 == 18 + x0) {
//        if (true) {
//            a = x0;
//        } else {
//            a = x0;
//        }
//        a = x0;
//        a = x0;
//        if (false) {
//            a = x0;
//            a = x0;
//        } else {
//            a = x0;
//        }
//    } else {
//        if (true) {
//            a = x0;
//            a = x0;
//        } else {
//            a = x0;
//        }
//        e = 1;
//    }
//  }


//