On How to define Eq on Cont r a

ProofOfContEq.md

Let's define a type class Searchable.

class Searchable a where
    epsilon :: (a -> Bool) -> a

    -- [Law]
    --  (∃x :: a. p a == True) => p (epsilon p) = True

We want to show that the following instance is valid.

instance (Ord a, Searchable r) => Searchable (a -> r) where
    epsilon :: ((a -> r) -> Bool) -> a -> r
    epsilon p = go Map.empty
      where
        go guess a = case Map.lookup a guess of
          Just r -> r
          Nothing -> epsilon $ \r ->
            let f b | b < a     = go guess b
                    | otherwise = go (Map.insert a r guess) b
            in p f

Remark. If a function p :: (a -> r) -> Bool is total function, p f evaluates the value of f x at most N values of x :: a. (Otherwise, p f doesn't terminate on a certain f.)

Thiis part is probably not correct. Probably I need to say "Searchable r must respect some total order on r"?

Remark. Searchable a imposes linear ordering on a, defined by

∀(x y : a), x <= y  ⇔  ∃p, epsilon p = x AND p y = True

Under this relation, epsilon p gives the smallest element among values of type a satisfies p.

∀x. p x ⇒ epsilon p <= x

[Proof]

(1) Suppose p x = True holds. (2) epsilon p <= x ⇔ ∃q, epsilon q = epsilon p AND q x = True. (3) epsilon p = epsilon p AND p x = True holds.

Section 1

Let me call these points {x_1, x_2, ..., x_N} "the set of needed points of p".

Now, let the notation p[r/x] be a funcion \f -> p (\y -> if x == y then r else f y). Note that the set of needed point of p[r/x] is x removed from the set of needed point of p.

For all 1 <= k <= N and 1 <= j < k, if we know that r_j = epsilon p x_j,

epsilon p x_k = go Map.empty
  where
    go guess a = case Map.lookup a guess of
      Just r -> r
      Nothing -> epsilon $ \r ->
        let f b | b < a     = go guess b
                | otherwise = go (Map.insert a r guess) b
        in p f
  = epsilon $ \r ->
      let f x_j | x_j < x_k = go Map.empty x_j
                | otherwise = go (Map.insert x_k r guess) x_j
      in p f
  = epsilon $ \r ->
      let f x_j | x_j < x_k = epsilon p x_j = r_j
                | otherwise = go (Map.insert x_k r guess) x_j
      in p f

In the otherwise branch, go (Map.insert x_k r guess) x_j means "We search epsilon p x_j, but each time p queries the value for x_k, it's r." This means we can say

  go (Map.insert x_k r guess) x_j = epsilon p[r/x_k] x_j

Also, if x_j < x_k, it's value is r_j. It means

   = epsilon $ \r ->
       p (epsilon p[r_1/x_1][r_2/x_2]...[r_{k-1}/x_{k-1}][r/x_k])

Especially, for k=1, the following holds.

epsilon p x_1 = epsilon $ \r -> p (epsilon p[r/x_1])

Section 2

Let's prove "(∃f :: a -> r. p f == True) => p (epsilon p) = True".

For each p :: (a -> r) -> Bool (thus it's set of needed points {x_1, x_2, ..., x_N}), we can define "pre-total-order" on f :: a -> r, defined by

f <= g  ⇔  (f x_1, f x_2, ...) <= (g x_1, g x_2, ...)
  Where ordering on N-tuple is defined by lexicographic order
        using order on r induced by `Searchable r`.

Suppose some f exist such that p f == True. We can take one of minimum function among them, minimum using (<=) defined above. Let's call it f*.

We can show that (This part is also suspicious)

epsilon p x_1 = f* x_1

Proof.

epsilon p x_1 = epsilon $ \r -> p (epsilon p[r/x_1]).

If for any r `p (epsilon p[r/x_1]) == False`,
setting r = f* x_1 yields contradiction.
so there is some `r` such that `p (epsilon p[r/x_1]) == True`,
where `r = f* x_1` being one example.

For such `r`,
    `epsilon p[r/x_1] >= f*` from the minimality of `f*`.
==> `(r, epsilon p[r/x_1] x_2, ...) >= (f* x_1, f* x_2, ...)`
==> `r >= f* x_1`

And from minimality property of `epsilon` on `r`,

`epsilon $ \r -> p (epsilon p[r/x_1]) = f* x_1`.

Similarly, using induction on k, we can show

epsilon p x_2 = f* x_2
epsilon p x_3 = f* x_3
  :
epsilon p x_N = f* x_N

And using the fact p f can't distinguish value of f at x other than {x_1, x_2, ...},

p (epsilon p) = p f* = True

This was what we wanted to show. QED.