Using the Rieger-Nishimura lattice as a decision procedure failure result

gistfile1.txt

given (p || ~p)
prove (~~p -> p)

proof :: (p + (p -> 0)) -> (((p -> 0) -> 0) -> p)
proof p_or_p0 p0_0 =
  case p_or_p0
    Left p =>
      p
    Right p0 =>
      absurd (p0_0 p0)

(--p -> p) + -p + --p

proof p00p_or_p0_or_p00
  In 0 p00p => Right p00p
  In 1 p0 => Right (\p00 -> absurd (p00 p0))
  In 2 p00 => Left p00


ImpliesNode n = ImpliesNode (n - 1) -> UnionNode (n - 2)
UnionNode n = ImpliesNode (n - 1) + UnionNode (n - 1)
ImpliesNode 1 = -p
UnionNode 1 = p
UnionNode 0 = 0


prove that UnionNode (n - 1) -> ImpliesNode n for sufficiently large n
that's equivalent to
UnionNode (n - 1) -> ImpliesNode n
UnionNode (n - 1) -> (ImpliesNode (n - 1) -> UnionNode (n - 2))
UnionNode (n - 1) -> ((ImpliesNode (n - 2) -> UnionNode (n - 3)) -> UnionNode (n - 2))
(ImpliesNode (n - 2) + UnionNode (n - 2)) -> ((ImpliesNode (n - 2) -> UnionNode (n - 3)) -> UnionNode (n - 2))
(ImpliesNode (n - 2) + (ImpliesNode (n - 3) + UnionNode (n - 3))) -> ((ImpliesNode (n - 2) -> UnionNode (n - 3)) -> UnionNode (n - 2))
(ImpliesNode (n - 2) + (ImpliesNode (n - 3) + UnionNode (n - 3))) -> ((ImpliesNode (n - 2) -> UnionNode (n - 3)) -> (ImpliesNode (n - 3) + UnionNode (n - 3)))
now we can set
a = ImpliesNode (n - 2)
b = ImpliesNode (n - 3)
c = UnionNode (n - 3)
to get
(a + (b + c)) -> ((a -> c) -> (b + c))
which is straightforward

prove that UnionNode 1 -> ImpliesNode 2
that's equivalent to
UnionNode 1 -> ImpliesNode 2
UnionNode 1 -> (ImpliesNode 1 -> UnionNode 0)
p -> (-p -> 0)
which is straightforward

prove that UnionNode 0 -> ImpliesNode 1
that's equivalent to
UnionNode 0 -> ImpliesNode 1
0 -> -p
which is straightforward


ImpliesNode n = ImpliesNode (n - 1) -> UnionNode (n - 2)
UnionNode n = ImpliesNode (n - 1) + UnionNode (n - 1)

means...
ImpliesNode n =
  (
    (
      (... ((--p -> p) -> UnionNode 2) ...
        -> UnionNode (n - 5))
      -> UnionNode (n - 4))
    -> UnionNode (n - 3))
  -> UnionNode (n - 2)

UnionNode n = UnionNode (n - 1) +
  (
    (
      (... ((--p -> p) -> UnionNode 2) ...
        -> UnionNode (n - 6))
      -> UnionNode (n - 5))
    -> UnionNode (n - 4))
  -> UnionNode (n - 3)

UnionNode n =
  ImpliesNode (n - 1)
    + ImpliesNode (n - 2)
    + ImpliesNode (n - 3)
    + ImpliesNode (n - 4)
    + ...
    + ImpliesNode 2
    + -p
but the infinite regress is actually not necessary here:
UnionNode n = ImpliesNode (n - 1) + ImpliesNode (n - 2)


UnionNode 1 = p
ImpliesNode 1 = -p
ImpliesNode 2 = --p
ImpliesNode 3 = --p -> p
ImpliesNode 4 = (--p -> p) -> (p + -p)
ImpliesNode n =
  (
    (
      (... (((--p -> p) -> (p + -p)) -> (ImpliesNode 1 + ImpliesNode 2)) ...
        -> (ImpliesNode (n - 7) + ImpliesNode (n - 6)))
      -> (ImpliesNode (n - 6) + ImpliesNode (n - 5)))
    -> (ImpliesNode (n - 5) + ImpliesNode (n - 4)))
  -> (ImpliesNode (n - 4) + ImpliesNode (n - 3))


For functional programming, we probably have a pretty different situation going on. Even though the type (a + a + b) has functions back and forth with (a + b + b), those functions lose information both ways when + is like Haskell's Either. In general, in functional programming, we care about which inhabitant we have when a type has more than one. Furthermore, in *unsound* functional programming contexts like Racket, we don't have all that much use for programming with types that ostensibly have no inhabitants (aside from the idea that it might give us some informal reassurance and a head start at porting to a sound language).

Let's look at the reason we're exploring the Rieger-Nishimura lattice anyway. We're considering this as a more expressive family of results for a partial decision procedure to return, rather than just returning a proof of the proposition tested, a refutation of it, or nothing. We're examining confidence levels a little bit more useful than nothing but not quite as useful as a proof or a refutation.

There are a few concrete ways we could make this useful.

First, we could focus in on the types that are uncallable functions and substitute them with potentially more useful concrete types, in the spirit of apartness witnesses:

construction (c) => p
refutation (r) => -p
construction (c) OR nonconstructive justification (j) => --p

ImpliesNode n = ImpliesNode (n - 1) -> UnionNode (n - 2)
UnionNode n = ImpliesNode (n - 1) + UnionNode (n - 1)
ImpliesNode 2 = c + j
ImpliesNode 1 = r
UnionNode 1 = c

prove that UnionNode 2 -> ImpliesNode 3
that's equivalent to
UnionNode 2 -> ImpliesNode 3
(ImpliesNode 1 + UnionNode 1) -> ImpliesNode 3
(ImpliesNode 1 + UnionNode 1) -> (ImpliesNode 2 -> UnionNode 1)
(r + c) -> ((c + j) -> c)
the (c + j) means r is a contradiction, so we have a c, and we're done (note that we probably need this step to be a function supplied by the user along with the types c, r, and j, if only so that we know what to do when we have multiple c's to choose between and what to do when we need a c and only have an r and a j)

prove that UnionNode 1 -> ImpliesNode 2
that's equivalent to
UnionNode 1 -> ImpliesNode 2
c -> (c + j)
straightforward

It's probably easy to show these are closed under union and implication with the following back-and-forth type conversions (not necessarily isomorphisms):
ImpliesNode a + ImpliesNode (a - 1) = UnionNode (a + 1)
ImpliesNode a + ImpliesNode (a - b - 2) = ImpliesNode a
ImpliesNode a + UnionNode a = UnionNode (a + 1)
ImpliesNode a + UnionNode (a - b - 1) = UnionNode (a + 1)
ImpliesNode a + UnionNode (a + b + 1) = UnionNode (a + b + 1)
UnionNode a + UnionNode b = UnionNode (max a b)
(ImpliesNode a -> UnionNode (a + b + 1)) = 1
(ImpliesNode a -> UnionNode a) = ImpliesNode (a + 1)
(ImpliesNode a -> UnionNode (a - 1)) = ImpliesNode (a + 1)
(ImpliesNode a -> UnionNode (a - 2)) = ImpliesNode (a - 1)
(ImpliesNode a -> UnionNode (a - b - 3)) = UnionNode (a - b - 3)
(ImpliesNode a -> ImpliesNode (a + b)) = 1
(ImpliesNode a -> ImpliesNode (a - b - 1)) = ImpliesNode (a - b - 1)
(UnionNode a -> ImpliesNode (a + b + 1)) = 1
(UnionNode a -> ImpliesNode (a - b)) = ImpliesNode (a - b)
(UnionNode a -> UnionNode (a + b)) = 1
(UnionNode a -> UnionNode (a - 1)) = ImpliesNode a
(UnionNode a -> UnionNode (a - b - 2)) = UnionNode (a - b - 2)

Secondly (returning to our list of ways we could make the lattice useful), we could consider the + and -> types to be generic interfaces, so that we can in fact express certain isomorphisms in ways that actually round-trip.

Thirdly, we could consider every element of the lattice to be its own user-supplied type like c, r, and j. We could regard the lattice as an automated way to wire up these values, passing some to the other ones' arguments according to their signatures in order to find the value they correspond to at the lattice's "meet" type for them.

Fourthly, we could realize that in all these approaches, the act of comparing values for equality will have to respond to a subcomparison result anything short of 1 by reporting something that falls short of fully known equality. Upon failure, we can report a partially zipped up value with some of the fields successfully filled in with equality witnesses, some of the fields not attempted yet, and with a fallen-short result for one of the fields. We could potentially have more than one value being zipped up at a time, with some way to change that number as we resume.

That's... an effect handler receiving a continuation. Multiple values being zipped up at the same time is SIMD, vectorization, or reactivity.

In the case of an ordered comparison, we'll want to treat less-than-or-incomparable and greater-than-or-incomparable evidence by keeping track of it and resuming the comparison, while we treat the combination of both (incomparability evidence) as time to exit and do something else. And this is in some sense two decision procedures in progress (the less-than-or-equal one and the greater-than-or-equal one), with either one of them potentially completing even when the other one is stuck.

In terms of effects, and in terms of that automatic wiring-up, this exit condition when both comparisons are stuck seems like an effect arising out of coordinated action by two concurrent processes. (Or a failure by two backtracking branches.)

In that lattice of knowledge gained, there's a bit of a threshold set going on (in the LVars paper sense) to determine when an effect is unhandled. Or I guess we could say there's a homomorphism from that lattice to a two-element lattice {Handled, Unhandled} with Handled < Unhandled. (As we gain knowledge, we move down in the lattice to states of more knowledge until we reach a state that's unhandled.)

If we embrace the concurrency idea and imagine each process being a declaration in a Cene module, communicating via the blackboard metaphor... then the exit condition is halting the declarations partway through their concurrent operation because sufficient knowledge has been gained or because they've all blocked on reads. (Stopping because they've written inconsistent things is different; that makes part of the concurrent execution wrong in hindsight, and it should probably be considered a fatal error. But... well, that could block on a read too, in the hopes of being told how to unify the old value and the new value.)

Hey, treating field comparisons concurrently too could explain types with mutually dependent types for their fields. The second part of a dependent sum type depends on the relatedness witness of the first part to know what operation the second part should use to check relatedness. (If the first part holds first-class types, relatedness between those types determines a way to check relatedness between their values, which is good because the second parts might be typed according to those related types.) But if we think about this happening concurrently, then we could have the first part also depend on the equality witness of the second part, just being careful to use this power in such a way that each of them makes progress. If they're like Cene modules, then they could have access to closed-world assumption familiarity tickets to witness each other's state so they can depend on these equality witnesses (and maybe other intermediate results too).