Re: [Epigram] Definitional equality in observational type theory
Hi Bas, thank you - indeed this is a very interesting observation. This was the proof I had in mind when I first claimed that the axiom of choice is provable in OTT. However, I was deluded in believing that OTT/ predicative topoi exactly characterize the theory of the setoid model. As you clearly point out this is not the case. To me this is an incompleteness of the formal system (OTT/predicative topoi) wrt the intended interpretation. This should be fixable, leading to OTT+X or predicative topoi + X which should be complete wrt the setoid model. More categorically we could say that X characterizes the predicative topoi obtained by an exact completion of an LCCC - I think. First of all, I am not sure whether a "fix" is needed. My recent experience in constructive mathematics is that it is actually quite pleasant to work without countable choice. Initial experience shows that it may lead to better algorithms implicit in the proofs. (Most of this is in my work with Thierry Coquand.) As you know, choice breaks abstract datatypes. See for instance the encoding of ADT as existential types by Mitchell and Plotkin. This is not possible in dependent type theory precisely because we have choice (this was pointed out to me by Jesper Carlstrom some time ago). I understand one motivation for your work on OTT as an attempt to bring back (some?) ADTs in type theory. It would be a pity to throw them out again without a good reason. I'd like to understand this better - in the moment I am unconvinced. Instead of "choice", I'd like f : Pi a:A.(B a)/(~ a) - lift f: (Pi a:A.B a)/~' for "discrete" types A, which means that I work in the internal language of the setoid model. Quotient types, even with lift, seem to be a good way to capture ADTs. Also if you want to reject lift, it would be good to have a model construction (maybe like the setoid model) which refutes it. Other things which you want may become true in this model. Having said that here are some quick remarks on your proposal below. Having choice for N->N as somewhat uncommon. It is not present in Bishop's constructive mathematics, i.e. more or less the setoid model of ML type theory. However, it is present in Brouwerian intuitionism and in some realizability models. Brouwer does not have choice for (N->N)->N. Martin Hofmann has some discussion on choice and extensionality in his thesis, but uses a syntactic criterion somewhat like the one that you outline. I alreay realized that I should reread Martin's thesis. One semantic candidate for X could be `all types have a projective cover'. This is what is used in realizability theory and what Erik Palmgren translated to type theory. A type P is projective if for all f:A->B and every function g:P->B there is a function h:P->A with f o h = g. Projective types "have choice". The idea is that the projective types are Bishop's pre-sets or the types in the setoid construction. I'll think about this. Cheers, Thorsten This message has been checked for viruses but the contents of an attachment may still contain software viruses, which could damage your computer system: you are advised to perform your own checks. Email communications with the University of Nottingham may be monitored as permitted by UK legislation.
Re: [Epigram] Definitional equality in observational type theory
Hi Conor, I'm not sure I understand what's going on here. This happens if you don't type check your definitions. I got carried away with my non-dependent simplification of the story. Thank you for actually reading it. Indeed, in the setoid model we can construct a function f : A -> [B] -- lift f : [A -> B] if the setoid A is "trivial", i.e. has the identity as its equivalence relation. I can do it if A is decided. If you give me a : A, then I pick lift f = iI const (f a) Ii Indeed, however your trick won't work for the dependent version: f : Pi a:A.[B a] - lift f: [Pi a:A.B a] f : A -> B/~ - lift f : (A -> B)/~' Again, if you give me some a : A, I say lift f = const (f a) -- const respects the equivalence because const b a ~' const b' a if b ~ b' Dito. We need f : Pi a:A.(B a)/(~ a) - lift f: (Pi a:A.B a)/~' where ~' is defined as before: f ~' g = Pi a:A.f a ~ g a but for f,g : Pi a:A.B a and ~ is actually a family of equivalence relations ~' : Pi a:A.(B a) -> (B a) -> Prop. We define the type of non-empty subsets of Bool as NE = Sigma Q : Bool-> Prop.Sigma x:Bool.Q x Note that NE is inhabited, eg by moo = (const 1; true; ()). We define the equivalence relation of extensional equality of subsets ~ : NE -> NE -> Prop (Q,_) ~ (R,_) = forall b:Bool.Q b <-> R b Now we derive: h : NE/~ -> [ NE ] We define h0 : Pi (P,_):NE . [ Sigma b:2.P b ] h0 (P,p) = return p and observe that this trivially preserves ~ and hence we obtain h : Pi (P,_):NE/~ . [ Sigma b:2.P b ] Now, if we were able to lift h we get lift h : [ NE/~ -> NE] return (const moo) : [ NE/~ -> NE] lift h : [ Pi (P,_):NE/~ . Sigma b:2.P b ] and your version ceases to work. Obviously, NE/~ isn't a setoid with a trivial equality! The Diaconescu argument shows that we can prove for any P:Prop H : NE/~ -> NE -- Dia H : P \/ not P = [P + not P] Corrected: H : Pi (P,_):NE/~ . Sigma b:2.P b Dia H : P \/ not P = [P + not P] Dia (const moo) : P \/ not P see below for a Epigram 2+n style proof of Dia. Under the circumstances, I really hope you've cocked this up. I have. We can also see what goes wrong in general: The principle f : A -> B/~ - lift f : (A -> B)/~' fails because given the setoid A = (A0,~A) the premise gives us an underlying function f0:A0 -> B (for simplicity we assume that B is trivial) s.t. a ~A b implies f0 a ~B f0 b, where to use the same function to construct an element of A -> B we need to show that a ~A b implies f0 a = f0 b, and there is no reason to believe this - unless ~A is the equality. I just about swallow that. But if A0 is decided, you need to use the spec part (which you're eliding for simplicity) to force me to use f0 in the way you're suggesting. You are right. The reasoning only works for the dependent version. P.S. For completeness: Dia itself can be constructed as in the COQ script: we use T,F : Bool -> Prop T b = (b=true) \/ P F b = (b=false) \/ P by applying H to the equivalence classe , and projecting out the components we get t,f : Bool t = fst (H ) f = fst (H ) snd (H ) : t=true \/ P snd (H ) : f=false \/ P Are you sure? I thought H had return type NE, giving (P; a; p) = fst (H ), (Q, b, q) := fst(H ) : Bool -> Prop where a,b : Bool, p : P a, q : Q b but no connection necessary between T and P, F and Q. This should now work with the correct type of H. Cheers, Thorsten This message has been checked for viruses but the contents of an attachment may still contain software viruses, which could damage your computer system: you are advised to perform your own checks. Email communications with the University of Nottingham may be monitored as permitted by UK legislation.
Re: [Epigram] Definitional equality in observational type theory
Hi Thorsten I'm not sure I understand what's going on here. Thorsten Altenkirch wrote: Indeed, in the setoid model we can construct a function f : A -> [B] -- lift f : [A -> B] if the setoid A is "trivial", i.e. has the identity as its equivalence relation. I can do it if A is decided. If you give me a : A, then I pick lift f = iI const (f a) Ii or, in less idiomatic longhand lift f = do c <- return const b <- f a return (c b) If you give me A -> 0, it's easy. f : A -> B/~ - lift f : (A -> B)/~' Again, if you give me some a : A, I say lift f = const (f a) -- const respects the equivalence because const b a ~' const b' a if b ~ b' But hang on - what stops us from doing a Diaconescu? Excluded middle doesn't hold in the setoid model, even though we only get P \/ not P where A \/ B = [A + B]. But this would still require that we have P + not P in the underlying set. So what goes wrong? We define the type of non-empty subsets of Bool as NE = Sigma Q : Bool-> Prop.Sigma x:Bool.Q x Note that NE is inhabited, eg by moo = (const 1; true; ()). We define the equivalence relation of extensional equality of subsets ~ : NE -> NE -> Prop (Q,_) ~ (R,_) = forall b:Bool.Q b <-> R b Now we derive: h : NE/~ -> [ NE ] which is just the indentity on the underlying elements. The point is that obviously ~ implies the trivial equality of [..]. Now, if we were able to lift h we get lift h : [ NE/~ -> NE] return (const moo) : [ NE/~ -> NE] Obviously, NE/~ isn't a setoid with a trivial equality! The Diaconescu argument shows that we can prove for any P:Prop H : NE/~ -> NE -- Dia H : P \/ not P = [P + not P] Dia (const moo) : P \/ not P see below for a Epigram 2+n style proof of Dia. Under the circumstances, I really hope you've cocked this up. We can also see what goes wrong in general: The principle f : A -> B/~ - lift f : (A -> B)/~' fails because given the setoid A = (A0,~A) the premise gives us an underlying function f0:A0 -> B (for simplicity we assume that B is trivial) s.t. a ~A b implies f0 a ~B f0 b, where to use the same function to construct an element of A -> B we need to show that a ~A b implies f0 a = f0 b, and there is no reason to believe this - unless ~A is the equality. I just about swallow that. But if A0 is decided, you need to use the spec part (which you're eliding for simplicity) to force me to use f0 in the way you're suggesting. P.S. For completeness: Dia itself can be constructed as in the COQ script: we use T,F : Bool -> Prop T b = (b=true) \/ P F b = (b=false) \/ P by applying H to the equivalence classe , and projecting out the components we get t,f : Bool t = fst (H ) f = fst (H ) snd (H ) : t=true \/ P snd (H ) : f=false \/ P Are you sure? I thought H had return type NE, giving (P; a; p) = fst (H ), (Q, b, q) := fst(H ) : Bool -> Prop where a,b : Bool, p : P a, q : Q b but no connection necessary between T and P, F and Q. Now, I know that my pathological functions are not the functions you're thinking of, but it does rather show that the real action, whatever it is, lies in the "spec" parts which you're throwing away. More later Conor PS I blogged a bit about implementing OTT...
Re: [Epigram] Definitional equality in observational type theory
Hi Thorsten, On Thursday 01 February 2007 08:55:30 Thorsten Altenkirch wrote: > thank you - indeed this is a very interesting observation. This was > the proof I had in mind when I first claimed that the axiom of choice > is provable in OTT. However, I was deluded in believing that OTT/ > predicative topoi exactly characterize the theory of the setoid > model. As you clearly point out this is not the case. To me this is > an incompleteness of the formal system (OTT/predicative topoi) wrt > the intended interpretation. This should be fixable, leading to OTT+X > or predicative topoi + X which should be complete wrt the setoid > model. More categorically we could say that X characterizes the > predicative topoi obtained by an exact completion of an LCCC - I think. First of all, I am not sure whether a "fix" is needed. My recent experience in constructive mathematics is that it is actually quite pleasant to work without countable choice. Initial experience shows that it may lead to better algorithms implicit in the proofs. (Most of this is in my work with Thierry Coquand.) As you know, choice breaks abstract datatypes. See for instance the encoding of ADT as existential types by Mitchell and Plotkin. This is not possible in dependent type theory precisely because we have choice (this was pointed out to me by Jesper Carlstrom some time ago). I understand one motivation for your work on OTT as an attempt to bring back (some?) ADTs in type theory. It would be a pity to throw them out again without a good reason. Having said that here are some quick remarks on your proposal below. Having choice for N->N as somewhat uncommon. It is not present in Bishop's constructive mathematics, i.e. more or less the setoid model of ML type theory. However, it is present in Brouwerian intuitionism and in some realizability models. Brouwer does not have choice for (N->N)->N. Martin Hofmann has some discussion on choice and extensionality in his thesis, but uses a syntactic criterion somewhat like the one that you outline. One semantic candidate for X could be `all types have a projective cover'. This is what is used in realizability theory and what Erik Palmgren translated to type theory. A type P is projective if for all f:A->B and every function g:P->B there is a function h:P->A with f o h = g. Projective types "have choice". The idea is that the projective types are Bishop's pre-sets or the types in the setoid construction. Best, Bas --- Research Group Foundations/ Institute for Computing and Information Sciences Radboud University Nijmegen www.cs.ru.nl/~spitters/
Re: [Epigram] Definitional equality in observational type theory
Hi Bas, thank you - indeed this is a very interesting observation. This was the proof I had in mind when I first claimed that the axiom of choice is provable in OTT. However, I was deluded in believing that OTT/ predicative topoi exactly characterize the theory of the setoid model. As you clearly point out this is not the case. To me this is an incompleteness of the formal system (OTT/predicative topoi) wrt the intended interpretation. This should be fixable, leading to OTT+X or predicative topoi + X which should be complete wrt the setoid model. More categorically we could say that X characterizes the predicative topoi obtained by an exact completion of an LCCC - I think. Indeed, in the setoid model we can construct a function f : A -> [B] -- lift f : [A -> B] if the setoid A is "trivial", i.e. has the identity as its equivalence relation. The construction is exactly the one you point out & it actually corresponds to my previous informal explanation why this is "not unreasonable": Note that this is not completely unreasonable: we observe the hidden choice made by f, but we compensate by this by hiding our knowledge. Which setoids have a trivial equality? Certainly all first order types. However, if we start with an extensional theory (which can be justified with the setoid model) than also higher types N -> N have a trivial equality (indeed the extensional equality here is the "finest" equality). Hence we certainly get considerable more than countable choice. Actually, instead of using only [..] we can formulate a more general operator for quotient types, given an equivalence relation ~ : B -> B -> Prop, we define ~' : (A -> B) -> (A->B)->Prop as f ~' g = forall a:A.f a ~ g a. We obtain the following generalisation: f : A -> B/~ - lift f : (A -> B)/~' But hang on - what stops us from doing a Diaconescu? Excluded middle doesn't hold in the setoid model, even though we only get P \/ not P where A \/ B = [A + B]. But this would still require that we have P + not P in the underlying set. So what goes wrong? We define the type of non-empty subsets of Bool as NE = Sigma Q : Bool-> Prop.Sigma x:Bool.Q x We define the equivalence relation of extensional equality of subsets ~ : NE -> NE -> Prop (Q,_) ~ (R,_) = forall b:Bool.Q b <-> R b Now we derive: h : NE/~ -> [ NE ] which is just the indentity on the underlying elements. The point is that obviously ~ implies the trivial equality of [..]. Now, if we were able to lift h we get lift h : [ NE/~ -> NE] Obviously, NE/~ isn't a setoid with a trivial equality! The Diaconescu argument shows that we can prove for any P:Prop H : NE/~ -> NE -- Dia H : P \/ not P = [P + not P] and combining the two using bind we get (lift h) >>= Dia : P \/ not P see below for a Epigram 2+n style proof of Dia. We can also see what goes wrong in general: The principle f : A -> B/~ - lift f : (A -> B)/~' fails because given the setoid A = (A0,~A) the premise gives us an underlying function f0:A0 -> B (for simplicity we assume that B is trivial) s.t. a ~A b implies f0 a ~B f0 b, where to use the same function to construct an element of A -> B we need to show that a ~A b implies f0 a = f0 b, and there is no reason to believe this - unless ~A is the equality. The main question is how to characterize abstractly the types A for which lift is valid. Syntactically we could say "All types not containing quotients" but this is not very nice. I'd like a semantic condition for the type. Cheers, Thorsten P.S. For completeness: Dia itself can be constructed as in the COQ script: we use T,F : Bool -> Prop T b = (b=true) \/ P F b = (b=false) \/ P by applying H to the equivalence classe , and projecting out the components we get t,f : Bool t = fst (H ) f = fst (H ) snd (H ) : t=true \/ P snd (H ) : f=false \/ P By analyzing the cases of the propositional components we get two cases in which we can prove P (hence we are done with P \/ not P) and one where we have t=true f=false In this case we can prove not P: we assume p:P and using this we can prove T b, F b for any b and hence T b <-> F and therefore = but then t=f and true=false and we have derived a contradiction. On 1 Feb 2007, at 03:10, Bas Spitters wrote: Hi Thorsten and others, On Tuesday 30 January 2007 21:22:53 [EMAIL PROTECTED] wrote: I do indeed think that Observational Type Theory with quotient types should be the language of a Predicative Topos. I don't see in the moment that the setoid model would introduce anything which isn't provable in the Type Theory and at least in the moment I don't see how to prove the countable axiom of choice
