3 people like it.

Seemingly impossible program defines equality between arbitrary functions

It is well known that it is impossible to define equality between arbitrary functions. However, there is a large class of functions for which we can determine equality, and it’s strange and surprising. We explore this idea using F# code translated from the Swift programming language.

 1: 
 2: 
 3: 
 4: 
 5: 
 6: 
 7: 
 8: 
 9: 
10: 
11: 
12: 
13: 
14: 
15: 
16: 
17: 
18: 
19: 
20: 
21: 
22: 
23: 
24: 
25: 
26: 
27: 
28: 
29: 
30: 
31: 
32: 
33: 
34: 
35: 
36: 
37: 
38: 
39: 
40: 
41: 
42: 
43: 
44: 
45: 
46: 
47: 
48: 
49: 
50: 
51: 
52: 
53: 
54: 
55: 
56: 
57: 
58: 
59: 
60: 
61: 
62: 
63: 
64: 
65: 
66: 
67: 
68: 
69: 
70: 
71: 
72: 
73: 
74: 
75: 
76: 
77: 
78: 
79: 
80: 
81: 
82: 
83: 
84: 
85: 
86: 
87: 
88: 
89: 
90: 
91: 
92: 
93: 
94: 
// https://www.fewbutripe.com/2018/12/05/seemingly-impossible.html

type Bit =
    | Zero = 0
    | One = 1

/// An infinite sequence of bits.
type BitSequence =
    {
        /// Answers the bit at the given index. Article calls this "atIndex".
        Item : uint32 -> Bit
    }

[<AutoOpen>]
[<CompilationRepresentation (CompilationRepresentationFlags.ModuleSuffix)>]
module BitSequence =

    /// Creates a bit sequence with the given lookup function.
    let create f = { Item = f }

    /// Dumps the beginning of the given sequence to the console.
    let dump (seq : BitSequence) =
        [0u .. 10u]
            |> Seq.iter (fun i ->
                printfn "%d: %A" i seq.[i])

    /// Prepends the given bit to the given lazy sequence.
    let (++) bit (lseq : Lazy<BitSequence>) =
        create (fun i ->
            if i = 0u then bit
            else lseq.Value.[i - 1u])   // don't reify the given sequence until we have to

    /// Finds a sequence for which the given predicate is true.
    /// Warning: answers garbage sequence if no such sequence exists.
    let rec find (pred : BitSequence -> bool) =
        let zeroPred seq = pred (Bit.Zero ++ lazy seq)
        if exists zeroPred then
            Bit.Zero ++ lazy (find zeroPred)
        else
            let onePred seq = pred (Bit.One ++ lazy seq)
            Bit.One ++ lazy (find onePred)

    /// Is there a sequence for which the given predicate is true? Article calls this "anySatisfy".
    and exists pred =
        let lseq = lazy (find pred)
        let seq = create (fun i -> lseq.Value.[i])
        pred seq

    /// Do all sequences satisfy the given predicate? Article calls this "allSatisfy".
    and forall pred =
        pred >> not
            |> exists
            |> not

    /// Equality of functions that have BitSequence as their domains.
    let (==) (f1 : BitSequence -> 'a) (f2 : BitSequence -> 'a) =
        forall (fun seq -> f1 seq = f2 seq)

let oneOnFirstFiveEvens () =
    let seq = BitSequence.find (fun seq ->
        seq.[0u] = Bit.One
            && seq.[2u] = Bit.One
            && seq.[4u] = Bit.One
            && seq.[6u] = Bit.One
            && seq.[8u] = Bit.One)
    BitSequence.dump seq

let equality () =

    let f (seq : BitSequence) = int seq.[1u] * int seq.[2u]
    let g (seq : BitSequence) = int seq.[1u] + int seq.[2u]
    printfn "f = f: %A" (f == f)
    printfn "g = g: %A" (g == g)
    printfn "f = g: %A" (f == g)

    let h (seq : BitSequence) =
        match seq.[1u], seq.[2u] with
            | Bit.One, Bit.One -> 1
            | _ -> 0
    printfn "f = h: %A" (f == h)
    printfn "g = h: %A" (g == h)

    let k (seq : BitSequence) =
        ((int seq.[1u] + int seq.[2u] + 908) % 6) / 4
    printfn "f = k: %A" (f == k)
    printfn "g = k: %A" (g == k)
    printfn "h = k: %A" (h == k)

[<EntryPoint>]
let main argv =
    oneOnFirstFiveEvens ()
    printfn ""
    equality ()
    0
Bit.Zero: Bit = 0
Bit.One: Bit = 1
type BitSequence =
  {Item: uint32 -> Bit;}

Full name: Script.BitSequence


 An infinite sequence of bits.
BitSequence.Item: uint32 -> Bit


 Answers the bit at the given index. Article calls this "atIndex".
Multiple items
val uint32 : value:'T -> uint32 (requires member op_Explicit)

Full name: Microsoft.FSharp.Core.Operators.uint32

--------------------
type uint32 = System.UInt32

Full name: Microsoft.FSharp.Core.uint32
type Bit =
  | Zero = 0
  | One = 1

Full name: Script.Bit
Multiple items
type AutoOpenAttribute =
  inherit Attribute
  new : unit -> AutoOpenAttribute
  new : path:string -> AutoOpenAttribute
  member Path : string

Full name: Microsoft.FSharp.Core.AutoOpenAttribute

--------------------
new : unit -> AutoOpenAttribute
new : path:string -> AutoOpenAttribute
Multiple items
type CompilationRepresentationAttribute =
  inherit Attribute
  new : flags:CompilationRepresentationFlags -> CompilationRepresentationAttribute
  member Flags : CompilationRepresentationFlags

Full name: Microsoft.FSharp.Core.CompilationRepresentationAttribute

--------------------
new : flags:CompilationRepresentationFlags -> CompilationRepresentationAttribute
type CompilationRepresentationFlags =
  | None = 0
  | Static = 1
  | Instance = 2
  | ModuleSuffix = 4
  | UseNullAsTrueValue = 8
  | Event = 16

Full name: Microsoft.FSharp.Core.CompilationRepresentationFlags
CompilationRepresentationFlags.ModuleSuffix: CompilationRepresentationFlags = 4
val create : f:(uint32 -> Bit) -> BitSequence

Full name: Script.BitSequenceModule.create


 Creates a bit sequence with the given lookup function.
val f : (uint32 -> Bit)
val dump : seq:BitSequence -> unit

Full name: Script.BitSequenceModule.dump


 Dumps the beginning of the given sequence to the console.
Multiple items
val seq : BitSequence

--------------------
type seq<'T> = System.Collections.Generic.IEnumerable<'T>

Full name: Microsoft.FSharp.Collections.seq<_>
module Seq

from Microsoft.FSharp.Collections
val iter : action:('T -> unit) -> source:seq<'T> -> unit

Full name: Microsoft.FSharp.Collections.Seq.iter
val i : uint32
val printfn : format:Printf.TextWriterFormat<'T> -> 'T

Full name: Microsoft.FSharp.Core.ExtraTopLevelOperators.printfn
val bit : Bit
val lseq : Lazy<BitSequence>
Multiple items
active recognizer Lazy: Lazy<'T> -> 'T

Full name: Microsoft.FSharp.Core.ExtraTopLevelOperators.( |Lazy| )

--------------------
type Lazy<'T> = System.Lazy<'T>

Full name: Microsoft.FSharp.Control.Lazy<_>
property System.Lazy.Value: BitSequence
val find : pred:(BitSequence -> bool) -> BitSequence

Full name: Script.BitSequenceModule.find


 Finds a sequence for which the given predicate is true.
 Warning: answers garbage sequence if no such sequence exists.
val pred : (BitSequence -> bool)
type bool = System.Boolean

Full name: Microsoft.FSharp.Core.bool
val zeroPred : (BitSequence -> bool)
val exists : pred:(BitSequence -> bool) -> bool

Full name: Script.BitSequenceModule.exists


 Is there a sequence for which the given predicate is true? Article calls this "anySatisfy".
val onePred : (BitSequence -> bool)
val forall : pred:(BitSequence -> bool) -> bool

Full name: Script.BitSequenceModule.forall


 Do all sequences satisfy the given predicate? Article calls this "allSatisfy".
val not : value:bool -> bool

Full name: Microsoft.FSharp.Core.Operators.not
val f1 : (BitSequence -> 'a) (requires equality)
val f2 : (BitSequence -> 'a) (requires equality)
val oneOnFirstFiveEvens : unit -> unit

Full name: Script.oneOnFirstFiveEvens
Multiple items
module BitSequence

from Script

--------------------
type BitSequence =
  {Item: uint32 -> Bit;}

Full name: Script.BitSequence


 An infinite sequence of bits.
val equality : unit -> unit

Full name: Script.equality
val f : (BitSequence -> int)
Multiple items
val int : value:'T -> int (requires member op_Explicit)

Full name: Microsoft.FSharp.Core.Operators.int

--------------------
type int = int32

Full name: Microsoft.FSharp.Core.int

--------------------
type int<'Measure> = int

Full name: Microsoft.FSharp.Core.int<_>
val g : (BitSequence -> int)
val h : (BitSequence -> int)
val k : (BitSequence -> int)
Multiple items
type EntryPointAttribute =
  inherit Attribute
  new : unit -> EntryPointAttribute

Full name: Microsoft.FSharp.Core.EntryPointAttribute

--------------------
new : unit -> EntryPointAttribute
val main : argv:string [] -> int

Full name: Script.main
val argv : string []
Raw view Test code New version

More information

Link:http://fssnip.net/7VE
Posted:5 years ago
Author:Brian Berns
Tags: lazy , recursion