Need to figure out how to encode sets of PNats

[bkushigian]

I'm not going to be able to focus on this much for the next few days. We had chatted about encoding sets as functions

Set : tp -> Bool

Certain operations are easy:

union : (a : Set tp) -> (b : Set tp) -> Set tp
union a b = \x => (a x) or (b x)

intersection : (a : Set tp) -> (b : Set tp) -> Set tp
intersection a b = \x => (a x) and (b x)

complement : (a : Set tp) -> Set tp
complement a = not . a

diff : (a : Set tp) -> (b : Set tp) -> Set tp
diff a b = \x => (a x) && complement (b x)

symDiff : (a : Set tp) -> (b : Set tp) -> Set tp
symDiff a b = \x => (diff a b) x || (diff b a) x

Other things are harder. For infinite sets such as PNat, we have no test for the empty set---isEmpty is co-RE but not RE:

isEmpty : Set PNat -> Maybe PNat
isEmpty s = isEmptyHelper 1 where
    isEmptyHelper n = if s n then n else isEmptyHelper s (n + 1)

This may be a feature of constructive set theory, I'm not sure. We can possibly work around this by including the types

emptySet : (tp : Type) -> Set tp
emptySet tp = (\x => False)

data NonEmptySet : (tp : Type) -> Type where
    setWithWitness : (f : Set tp) -> (x : tp ** f x = True) -> NonEmptySet tp

This still has issues: in particular, we cannot talk about subset relations of arbitrary sets on infinite types: the query A subset B? is again coRE...the problem with the empty set is a special case of this. We can again patch this up to a certain degree by allowing ourselves to construct a subset B of a set A, which will present us with both a function and a proof that they are subsets. We can also speak of finite sets of a given size, say

data FinSet : -> (n : Nat) (tp : Type) -> Type where
    finSet : (Fin n -> tp) -> FinSet n tp

Here we are indexing into our tp with Fin n. We can convert this to an 'explicit' easily enough if we want.

Anyway, all this messiness comes from infinite sets, but we will of course want to work with these. The other idea would be a stream-like solution, which enumerates elements. This seems better if we actually wanted to program with elements, but we don't:

data StreamSet : (tp : Type) -> Type where
    anEmptyStreamSet : StreamSet tp
    aStreamSet : (x : tp) -> (cont : () -> StreamSet tp) -> StreamSet

Here we use a thunk () -> StreamSet tp to allow for possibly infinite sets. The obvious problem is that we now have duplicate elements.

I'd love to hear thoughts.

[donald-pinckney]

I think that isEmpty is positioned incorrectly here. When we write it as a function isEmpty : Set PNat -> Maybe PNat we are saying that we want a decision procedure to tell if any possible set is the empty set or not. In other words, we can construct any crazy set we want, and we want Idris to compute if the set if empty or not. But we shouldn't expect this to be decidable (if it were we could solve the Goldbach conjecture right now for example).

Instead, I think a set being empty should be regarded as a proposition which we need to give a proof of. Something like:

data IsEmpty : (s : Set PNat) -> Type where
   AllFalse : ((x : PNat) -> s x = False) -> IsEmpty s

In other words, to prove that the set is empty, you need to supply a proof that s x = False for every x.

[agiera]

To solve duplicate elements in a stream we could force f to be increasing by giving a proof. I think Donald's approach is probably necessary though.

I've been reading about Type Theory vs Set Theory, but am still really confused. There are a lot of articles highlighting their differences, but not much about constructing a Set Theory proof system in a Type system. This is what I've been tinkering with so far. Its basically Donald's approach with more of the ZF axioms.

import Naturals.PNat
import Logic

-- Axioms missing from ZFC
-- 2. Regularity (Might be granted by idris)
-- 9. Well-ordering
-- AC
data Set : (a : Type) -> Type where
  EmptySet : Set a
  Naturals : Set PNat
  Singleton : a -> Set a
  Union : Set a -> Set a -> Set a
  Intersection : Set a -> Set a -> Set a
  Restriction : Set a -> (a -> Type) -> Set a
  Image : Set a -> (a -> b) -> Set b
  Power : Set a -> Set (Set a)

mutual
  data SubsetEq : (s1 : Set a) -> (s2 : Set a) -> Type where
    SubsetEqPf : {x : a} -> (setCont s1 x) -> (setCont s2 x) -> SubsetEq s1 s2

  setCont : (Set a) -> (x : a) -> Type
  setCont EmptySet x = Void
  setCont Naturals x = x = x
  setCont (Singleton y) x = x = y
  setCont (Union s1 s2) x = Either (setCont s1 x) (setCont s2 x)
  setCont (Intersection s1 s2) x = (setCont s1 x, setCont s2 x)
  setCont (Restriction s f) x = (setCont s x, f x)
  setCont (Image s f) x = Exists (\y => (setCont s y, x = f y))
  setCont (Power s1) s2 = SubsetEq s2 s1

data SetEq : (s1 : Set a) -> (s2 : Set a) -> Type where
  SetEqPf : {x : a} -> (Iff (setCont s1 x) (setCont s2 x)) -> SetEq s1 s2

[bkushigian]

@donald-pinckney : nice idea--this is the dual notion of the NonEmptySet datatype, yes? Question: are there use cases where this would be more useful than simply defining an empty set data type as the constant function False?

@agiera :Interesting idea with Stream. This does limit us to working with things with an ordering, but for PNat this is fine. More of an issue, for infinite sets that aren't well founded (think rationals greater than 1) this will not work. Also, this formulation of sets trivially proves theorem 27 (a feature or a bug? you decide!)

WRT your Set datatype, this is interesting and may be the way to go. Question: is the SetEq correct? It looks like I can prove that A = B if I can provide an x such that x \in A iff x \in B. Am I reading this correctly? I think we want

data SetEq : (s1 : Set a) -> (s2 : Set a) -> Type where
    SetEqPf : ( (x : a) -> Iff (setCont s1 x) (setCont s2 x)) -> SetEq s1 s2

Also, the idea for setCont seems correct but we might want to return a separate data type:

data SetCont (Set a) -> (x : a) -> Type where
    ...

This will be a proof witnessing inclusion of x in the set.

[agiera]

I think we need the setCont function to calculate the proposition necessary for the proof, but adding a SetCont type seems like good form.

And if we had a set and proof that it was empty, we could show it like this:

prf : (x : PNat) -> Iff (SetCont s x) (SetCont EmptySet x)
SetEqPf prf

I think this is equivalent to Donald's IsEmpty function, in the case that s = Restriction Naturals f. Here f could be:

f : (x : PNat) -> Type
f x = x .< 1

Then the prf would be:

prf x = IffPf (\sPf => case sPf of                                    -- sPf : (x : PNat) -> SetCont (SetCont Naturals x, x .< 1)
  (SetContPf (SetContPf Refl, SetContPf contra) => SetContPf (theoremx x)
)          (\emptyPf -> case of                                   -- sPf : (x :PNat) -> SetCont Void
  (SetContPf contra => SetContPf (SetContPf Refl, SetContPf (void contra))

[donald-pinckney]

@bkushigian:

Question: are there use cases where this would be more useful than simply defining an empty set data type as the constant function False?

I think having some sort of an IsEmpty proposition / type is necessary (or that it could be built up from @agiera's stuff or similar). We can definitely a constant called emptyPNatSet which has the function which always returns false. But suppose I give you the set using the function which returns n > 10 && n < 5 for some PNat n. This set is indeed empty, but you don't know that beforehand, you only know that after you prove that n > 10 && n < 5 is always false. This is what my IsEmpty type lets you do.

[bkushigian]

@agiera I agree that we want to do something similar to what you are doing, but I don't think that this approach will quite work. For instance, in the singleton case of setCont, if x isn't y we can never return something of the type x = y, so the function isn't total. Likewise, I don't quite know what the Either is doing for the union. It seems like we are guaranteeing that one or the other contains the thing we are looking for--either Left or Right signifies that the thing was in the left set or the thing was in the right set.

Maybe I'm misunderstanding what the setCont does though, I'm assuming it evaluates whether or not a set contains a value. Is this correct?

Another issue: I think we can't pattern match on types. So if I get a type back from setCont, I don't think I can really do anything with it. We would need to use reflection which is probably not the way to go.

[bkushigian]

@donald-pinckney Agreed

[bkushigian]

@donald-pinckney @agiera So here is another question: what sort of Set "API" will we want to use? Or, in math speak, what are the set theoretic operations that we want to have? This might involve looking ahead a bit.

If we go with the axiomatic set theory approach it will probably be good to get a set theory module going with some useful results that come up regularly.

I just turned in a problem set last (aka this morning) and I have another due in a couple days. I also need to get my group moving on our project so I will probably at best be playing devil's advocate with whatever you guys suggest. If you want to figure out the sanest next step we can go from there. I'm hoping that by Saturday I should have some time to finally do some more work here.

[agiera]

setCont returns the Type of the proof that would be necessary to prove that x is contained in s. So, we aren't returning a proof that x = y, but we are actually returning the type x = y. If we can give a proof that x = y, then we know x is in Singleton y.

mutual
  setContProp : (Set a) -> (x : a) -> Type
  setContProp EmptySet x = Void
  setContProp Naturals x = x = x
  setContProp (Singleton y) x = x = y
  setContProp (Union s1 s2) x = Either (setContProp s1 x) (setContProp s2 x)
  setContProp (Intersection s1 s2) x = (setContProp s1 x, setContProp s2 x)
  setContProp (Restriction s f) x = (setContProp s x, f x)
  setContProp (Image s f) x = Exists (\y => (setContProp s y, x = f y))
  setContProp (Power s1) s2 = SubsetEq s2 s1

  data SetCont : (s : Set a) -> (x : a) -> Type where
    SetContPf : (setContProp s x) -> SetCont s x

[donald-pinckney]

Sorry I’ve been out of the loop for a bit. I have a ton of math hw due on Thursday, so I should be more free to make forward progress on this then.

[donald-pinckney]

@bkushigian @agiera I spent a lot more time playing around with this today. I just pushed the set stuff I prototyped to the branch sets, in a file landau/Sets2.idr, so you can check that out. I'll give the highlights of what I did and my personal conclusions here.

First, I strongly think that representing a set by a function PNat -> Bool is not a good idea for us to commit to, since it means that the only sets we can talk about are decidable sets. On the other hand, this representation does let us conveniently use some results such as Theorem 27. However, I'll show how we can recover this advantage while being able to talk about undecidable sets below.

The alternative is to represent a set by a function PNat -> Type, which is what I have in Sets2.idr, line 11:

-- A set of PNats is a family of propositions indexed by PNats
PSet : Type
PSet = PNat -> Type

The idea is that for each PNat n, you have a proposition P n, and the elements of the set are the ns for which P n is true. So to show that n is an element, you need to give a proof of P n:

-- A PNat x is in the set if the proposition (P x) is true (has a proof)
data SetElem : (x : PNat) -> (s : PSet) -> Type where
    Satisfies : (prf : s x) -> SetElem x s

With this setup we can define set operations:

setIntersection : PSet -> PSet -> PSet
setIntersection u v = \n => (u n, v n)

setUnion : PSet -> PSet -> PSet
setUnion u v = \n => Either (u n) (v n)

setComplement : PSet -> PSet
setComplement u = \n => Not (u n)

What does it look like to define an actual set? I think its pretty clean:

-- Here is an example of a set, all the PNats that are not equal to O
NotOne : PSet
NotOne = \n => Not (n = O)

Then we can prove what elements are and aren't in the set:

-- We can show that O is not an element of it
oneNotElem : Not (O `SetElem` NotOne)
oneNotElem = \elem => case elem of
    (Satisfies prf) => prf Refl

-- And that any n >= 2 is an element
ge2Elem : (x : PNat) -> (x .>= 2) -> x `SetElem` NotOne
ge2Elem (N u) (PlusOnRight Refl) = Satisfies (axiom3 u)

We can also talk about sets that are empty, and prove that they are empty. A set is known to be the empty set if we can refute the proposition for all n:

-- A set has been proved to be empty if we can prove the proposition is false for all n
data IsEmpty : (s : PSet) -> Type where
    AllFalse : ((n : PNat) -> Not (n `SetElem` s)) -> IsEmpty s

As for more proving stuff in the book, using this framework of sets we can give a proof of axiom5 (though I'm not sure if its actually very useful since we would normally use Idris's recursion for induction):

-- We can show axiom5
axiom5 : (s : PSet) -> O `SetElem` s -> ((x : PNat) -> x `SetElem` s -> (N x) `SetElem` s) -> (y : PNat) -> y `SetElem` s
axiom5 s one_elem next_elem O = one_elem
axiom5 s one_elem next_elem (N i) = next_elem i (axiom5 s one_elem next_elem i)

However, in the general framework of possibly undecidable sets, I couldn't give a proof of theorem27. I can't say for sure that its impossible, but based on this page: https://ncatlab.org/nlab/show/well-founded+relation I think it should be impossible as otherwise it would imply the axiom of choice, which should be impossible to prove.

That being said, if we restrict ourselves to decidable sets (which PNat -> Bool gave us) then we can prove theorem27. Instead of defining all sets to be decidable though, we can have a proposition that a given set is in fact decidable:

-- A set of PNats is a decidable set if the proposition for each n is decidable
data SetDec : (s : PSet) -> Type where
    AllDec : ((n : PNat) -> Dec (s n)) -> SetDec s

Proving that a set is decidable amounts to giving a decision procedure for it. With this framework, we can give proofs of theorems about undecidable sets (such as axiom5), and we can give proofs of theorems that only work for decidable sets, such as theorem27:

theorem27 : (g : PSet) -> (gDec : SetDec g) -> ContainsSomething g -> (x : PNat ** (x `SetElem` g, (y : PNat) -> y `SetElem` g -> x .<= y))

The full proof is given in the file.

Sorry this was a super long comment. Let me know your thoughts so we can move forward.

[bkushigian]

@agiera @donald-pinckney Apologies for dropping off the face of the earth---I've had a pretty busy couple weeks.

@donald-pinckney So this is nicer than the PNat -> Bool idea for sure. I don't know enough to compare it to @agiera's idea, which also looks like it has some nice properties. I'd say that your version looks a little more type-theory-y, which is nice, but then again, we are working through a book founded in set theory.

@agiera have you had any luck playing with the set theory stuff?

Anyway, this is something I want to dive into but I'm scrambling with courses/projects/presentation prep. There are two really good ideas here and I don't know how to proceed. I guess I would say that if either of you is convinced by the other's idea, great! Otherwise, this is why god made branches :)

Oh! Re: "PNat -> Bool only works for decidable sets": I'm gonna have to look at this when I'm fresher. Were you able to prove theorem 27 with the PNat -> Bool definition? The theorem seems to indicate that if (X, <) is any set with a classically well-founded ordering (with the y < x criterion) then we can prove LEM--but we can define the set with only the number 2 in it, and this is classically well-founded, no? I'll have to look in the AM, I'm too tired to keep thoughts in my head :)

Question: will we ever need to work with sets of things that aren't PNats? Like power sets of PNats?

[donald-pinckney]

Question: will we ever need to work with sets of things that aren't PNats? Like power sets of PNats?

I purposely didn’t parameteize my set stuff over types so that it could look a bit clearer for these discussions, but it should be very easy to stick an arbitrary type in there in place of PNat. As for power sets, I think it should be easy to write a powerset function.

I don't know enough to compare it to @agiera's idea

I’m not completely sure, but I suspect it is roughly equivalent. @agiera organized things differently, by putting a ton of stuff into data constructors. For example, Intersection : Set a -> Set a -> Set a is a data constructor, but otherwise resembles my intersection function. I think in particular my definition of set lines up with Restriction.

Oh! Re: "PNat -> Bool only works for decidable sets": I'm gonna have to look at this when I'm fresher. Were you able to prove theorem 27 with the PNat -> Bool definition?

I didn’t try the PNat -> Bool definition, but I’m very sure I could. However, the proof has 2 restrictions: 1. The set needs to be decidable (which you can substitute the PNat -> Bool definition for) and 2. for “non-empty set” you need to provide an actual element in the set.

[agiera]

I believe they're equivalent ideas but with different packaging. One advantage to using more structure is that we can pattern match on sets if we need to. The structure also prevents other files from adding inconsistent axioms or operations to our sets like unrestricted comprehension. It is a bit cumbersome and doesn't utilize type theory. I'm not sure how compatible type theory and ZF are. It's not great that s n = Int is a valid set when defining a set as PSet = PNat -> Type.

In regards to theorem27, I think we can prove it using either structure. It also doesn't imply AoC because we have already constructed our well-ordering of PNats (.<=). We just have to prove that it is a well-ordering. If we proved that an arbitrary set of any type has a well-ordering, that would imply AoC. Like you said, using a proof that a set is not empty is a bit tricky. I'll give it a shot today.

[agiera]

I suppose the same could be said for Restriction Naturals (\n => Int). I'm not sure how to fix this.

[donald-pinckney]

I think the \n => Int problem isn’t a problem we need to solve. In a way it’s a perfectly valid set, the set of all n such that there exists an Int. It’s just really weird to write set that way. But we can already do this with anything else, for example we could prove a theorem weirdTheorem : n .< m -> Int, which is just as weird as such a set.

[agiera]

That makes sense. It turns out my implementation of Set won't work correctly in Idris. It has to do with the limitations of its general recursion: https://cstheory.stackexchange.com/questions/41037/what-are-the-limitations-of-dependent-typing. For example:

isSingleton : Bool -> Type
isSingleton True = Nat
isSingleton False = List Nat

-- works without recursion
ex : isSingleton False
ex = []

s : Set PNat
s = Singleton 3

prf : (N (N O)) = (N (N O))
prf = Refl

-- setContProp s 3 = (3 = 3)
asdf7 : setContProp (Singleton (N (N O))) (N (N O))
asdf7 = prf

I get the following errors:

- + Errors (2)
 |-- test.idr line 31 col 8:
 |   When checking right hand side of asdf7 with expected type
 |           setContProp (Singleton (N (N O))) (N (N O))
 |
 |   Type mismatch between
 |           N (N O) = N (N O) (Type of prf)
 |   and
 |           setContProp (Singleton (N (N O))) (N (N O)) (Expected type)
 `-- Set.idr line 26 col 2:
     Set.setContProp is possibly not total due to: Set.Power

The link in the first paragraph explains why setContProp is not total. I'm not totally clear on why Idris doesn't compute setContProp (Singleton (N (N O))) (N (N O)) and just leaves it alone. I could just rewrite setContProp as a data type, but it would be very cumbersome.

The lectures you sent are very good. I'm glad Ben and I studied some category theory last year.