The Coq mailing list

[Talia Ringer <tringer AT cs.washington.edu>]

I like this because it rules out terms like False_ind via other encodings. I'll try to think more about a syntactic restriction (it makes sense that it should be too restrictive); I'm interested if anyone has any ideas. The interactive version sounds easy enough to implement, so I could see what happens when I do that; I imagine the proof burden is prohibitive, but if I'm not going for useful, that's probably fine :)

On Fri, Mar 29, 2019, 1:40 AM Amin Timany <amintimany AT gmail.com> wrote:

Hi Talia,

Let me participate in this musing as well. I wonder if the following restriction is going to be enough for ruling out the explosion law?

Any type in Coq (CIC) is of the form Π(x_1:A_1). … Π(x_n:A_n) . B where B itself is not of this form, i.e., not a Π type. The restriction I’m thinking of is the following:

Π(x_1:A_1). … Π(x_n:A_n) . B is well-typed (it is a term of the appropriate sort) if either, all A_i’s are inhabited, or B is uninhabited.

This essentially disallows any function that could express explosion, i.e., any function type whose domain is empty while its codomain is not. Whether this restriction works or not, it is a semantic restriction and not syntactic. So one needs to come up with a syntactic approximation which would likely be too restrictive. Or, one could require the user to prove inhabitedness of a type A by exhibiting a term t : A and uninhabitedness of a type A by exhibiting a term t : A -> False (which is a valid type as the codomain is uninhabited!).

Regards,

Amin

On 29 Mar 2019, at 06:09, Talia Ringer <tringer AT cs.washington.edu> wrote:

The point of this side-project is just to have fun, not to make something useful, though if something useful falls out of it that's nice too. I spend most of my work life trying to make useful Coq tooling, so every so often it's a nice break to just do the thing that interests me most in that moment without any regard to whether anyone will care about the result, especially if it's quick.

I'm interested in two things right now: paraconsistent logics and the implications of removing features from Coq's logic on the resulting logical system. This would combine the two, though I think at this point I'm more likely to try removing many different features in different branches and seeing if any of the resulting logics are interesting. We spend so much time building upwards, and in doing so we've strayed so far from CoC; it's interesting to think now about what happens when we trim out small pieces of the result and explore the space in between CoC and Coq.

On Thu, Mar 28, 2019 at 10:04 PM Jason Gross <jasongross9 AT gmail.com> wrote:

Regarding

> I anticipate being bored next week, and I'd like a quick, fun, and interesting side project to fill my time (and I'm familiar enough with the Coq internals that playing with the code can meet these criteria).

I'd be more interested in a fork of Coq that supported some sort of linear or affine logic (though as far as I'm aware, how to integrate linear logic with dependent types is still an area of research).  Also this is possibly a much less quick side-project.

On Fri, Mar 29, 2019, 00:23 Talia Ringer <tringer AT cs.washington.edu> wrote:

I don't know. I was hoping coq-club would know, or at least be able to muse. The musing part is happening, so that's good :)

I can define the term you've given me in Type, but not in Prop. I have to wonder if this is really a problem, though; you may get that Fin 0 -> False, but without eliminating False, there's no way to get that False -> Fin 0, and so there's no way to get False -> P. What you get is that some encoding of false via some other uninhabitable type -> P, but in this logic, that encoding does not imply False. It does sort of fundamentally change what False actually means though; not all uninhabitable types would imply each other anymore. There would, in that model, be uninhabitable types with constructors that explode, but uninhabitable empty types would not explode. Would this be meaningful?

If this wouldn't be meaningful, then what is the minimum set of restrictions one would need to make to prevent something like Jason's term (which I'm calling fin0_ind)?

On Thu, Mar 28, 2019 at 9:21 PM Jason Gross <jasongross9 AT gmail.com> wrote:

Is there an existing theory that combines paraconsistent logic with dependent types?  You can do a lot with just the Church encoding of inductives, and all you need for that is Pi.

On Thu, Mar 28, 2019, 23:52 Talia Ringer <tringer AT cs.washington.edu> wrote:

Interesting! I can't say I had a plan; I thought of this while going for a run 30 minutes ago. I wonder if there's a restriction that it is possible to place either on inductive types or on pattern matching that makes this possible, but still leaves a useful and interesting set of inductive types and their eliminators. 

On Thu, Mar 28, 2019 at 8:49 PM Jason Gross <jasongross9 AT gmail.com> wrote:

What are your plans for the Church encoding of False := forall A : Prop, A?

I think you can also get False_ind by defining Fin : nat -> Set and then doing a match on an element of Fin 0:

(fun A x => match x in Fin n return match n with O => A | _ => True end with <each ctor> => I end) : forall A, Fin 0 -> A

On Thu, Mar 28, 2019, 23:38 Talia Ringer <tringer AT cs.washington.edu> wrote:

I anticipate being bored next week, and I'd like a quick, fun, and interesting side project to fill my time (and I'm familiar enough with the Coq internals that playing with the code can meet these criteria). I think, if so tasked, I could write a paraconsistent proof assistant from scratch. But what if I wanted to fork Coq and trim it down to a paraconsistent proof assistant? What is the minimal set of changes I would need to make?

Clearly, I would need for the principle of explosion to no longer hold, which means that False_ind and similar terms should no longer type-check. This means that empty pattern matching ought to be impossible, since in Coq:

False_ind :=

  fun (P : Prop) (f : False) => match f return P with end

: forall (P : Prop), False -> P.

It looks like in so doing, I would make disjunctive syllogism (forall A B, or A B -> ~ A -> B) impossible to prove, since I think all proofs of this in Coq must go through a term like False_ind. Am I wrong?

If this makes disjunctive syllogism unprovable, then I would not need to remove or_introl or or_intror. Does this mean that I could keep inductive types? Or would they cause unforeseen problems?

What about other features that Coq has?

Best,

Talia

On Thu, Mar 28, 2019 at 10:04 PM Jason Gross <jasongross9 AT gmail.com> wrote:

Regarding

> I anticipate being bored next week, and I'd like a quick, fun, and interesting side project to fill my time (and I'm familiar enough with the Coq internals that playing with the code can meet these criteria).

I'd be more interested in a fork of Coq that supported some sort of linear or affine logic (though as far as I'm aware, how to integrate linear logic with dependent types is still an area of research).  Also this is possibly a much less quick side-project.

On Fri, Mar 29, 2019, 00:23 Talia Ringer <tringer AT cs.washington.edu> wrote:

I don't know. I was hoping coq-club would know, or at least be able to muse. The musing part is happening, so that's good :)

I can define the term you've given me in Type, but not in Prop. I have to wonder if this is really a problem, though; you may get that Fin 0 -> False, but without eliminating False, there's no way to get that False -> Fin 0, and so there's no way to get False -> P. What you get is that some encoding of false via some other uninhabitable type -> P, but in this logic, that encoding does not imply False. It does sort of fundamentally change what False actually means though; not all uninhabitable types would imply each other anymore. There would, in that model, be uninhabitable types with constructors that explode, but uninhabitable empty types would not explode. Would this be meaningful?

If this wouldn't be meaningful, then what is the minimum set of restrictions one would need to make to prevent something like Jason's term (which I'm calling fin0_ind)?

On Thu, Mar 28, 2019 at 9:21 PM Jason Gross <jasongross9 AT gmail.com> wrote:

Is there an existing theory that combines paraconsistent logic with dependent types?  You can do a lot with just the Church encoding of inductives, and all you need for that is Pi.

On Thu, Mar 28, 2019, 23:52 Talia Ringer <tringer AT cs.washington.edu> wrote:

Interesting! I can't say I had a plan; I thought of this while going for a run 30 minutes ago. I wonder if there's a restriction that it is possible to place either on inductive types or on pattern matching that makes this possible, but still leaves a useful and interesting set of inductive types and their eliminators. 

On Thu, Mar 28, 2019 at 8:49 PM Jason Gross <jasongross9 AT gmail.com> wrote:

What are your plans for the Church encoding of False := forall A : Prop, A?

I think you can also get False_ind by defining Fin : nat -> Set and then doing a match on an element of Fin 0:

(fun A x => match x in Fin n return match n with O => A | _ => True end with <each ctor> => I end) : forall A, Fin 0 -> A

On Thu, Mar 28, 2019, 23:38 Talia Ringer <tringer AT cs.washington.edu> wrote:

I anticipate being bored next week, and I'd like a quick, fun, and interesting side project to fill my time (and I'm familiar enough with the Coq internals that playing with the code can meet these criteria). I think, if so tasked, I could write a paraconsistent proof assistant from scratch. But what if I wanted to fork Coq and trim it down to a paraconsistent proof assistant? What is the minimal set of changes I would need to make?

Clearly, I would need for the principle of explosion to no longer hold, which means that False_ind and similar terms should no longer type-check. This means that empty pattern matching ought to be impossible, since in Coq:

False_ind :=

  fun (P : Prop) (f : False) => match f return P with end

: forall (P : Prop), False -> P.

It looks like in so doing, I would make disjunctive syllogism (forall A B, or A B -> ~ A -> B) impossible to prove, since I think all proofs of this in Coq must go through a term like False_ind. Am I wrong?

If this makes disjunctive syllogism unprovable, then I would not need to remove or_introl or or_intror. Does this mean that I could keep inductive types? Or would they cause unforeseen problems?

What about other features that Coq has?

Best,

Talia