[Coq-Club] [Agda] Re: [HoTT] newbie questions about homotopy theory & advantage of UF/Coq

Thu Jan 9 12:06:59 CET 2014

Le 09/01/2014 11:18, Altenkirch Thorsten a écrit :
>>
>>
>> Higher-order datatypes are a bit more difficult, and I admit I never
>> worked it out. I believe it's possible though.
>>
>>>> The fact that the implementation is behind the theoretical capabilities
>>>> is just that, an implementation problem.
>>> The eliminators are like axioms in set theory and it is worthwhile to
>>> translate any extension by reducing them to the axiom instead of adding
>>> new ones even though they may be semantically justified.
>> That's fair, but I don't see why eliminators have a more powerful
>> ontological status than sized-types.
> It is maybe not the ontological status but they are a hell easier to write
> down!
>
> Do I believe in a foundational system which consists of pages with rules
> full of greek (and other alphabets) and super sub and whatever scripts?
>
> Actually I also don't like the schemes for datatypes either, hence I would
> like to reduce everything to fixed collection of type formers (we have
> done a fair bit of this using containers).
>
> So my target type theory is 0,1,2,Pi,Sigma,Id,U_n with eliminators. Ok we
> will need to consider extensions for induction recursion and HITs but they
> should also presented by a finite collection of constants with eliminators.
>
> I know there are some gaps in between what we like to do and what we know
> it is safe to do but I think we should be able to narrow this gap.
>
> Thorsten
So we have the same goal but not the same answer. ;-) Matter of taste. 
Because, for me, having just function symbols and rewrite rules is much 
more simpler and primitive than having inductive types, fixpoints and 
match's. For instance, in 2007, Denis Cousineau and Gilles Dowek proved 
that any pure type system can be encoded in lambda-pi modulo 
(type-level) rewriting. So, you may be interested in the development of 
Dedukti, a proof checker for lambda-pi modulo 
(https://www.rocq.inria.fr/deducteam/Dedukti/).

Frédéric.

>> They require work to be derived as
>> well, and the correctness proofs for them are quite similar to that for
>> sized types. This seems like a matter of preference. Obviously I'm not
>> neutral in this matter though.
>>
>> Best,
>>
>> Cody
>>
>>
>>
>>> Thorsten
>>>
>>>
>>>> Best,
>>>>
>>>> Cody
>>>>
>>>>
>>>>> V.
>>>>>
>>>>>
>>>>> On Jan 6, 2014, at 6:27 PM, Cody Roux <cody.roux at andrew.cmu.edu>
>>>>> wrote:
>>>>>
>>>>>> The thing about Coq is that it's very disturbing not to have a
>>>>>> Set-theoretic interpretation where Prop is the set of Booleans {True,
>>>>>> False}. Agda of course doesn't have these qualms, but the fact that
>>>>>> this
>>>>>> issue appears in Coq without use of anything fancy (impredicativity,
>>>>>> etc) makes me still a bit worried. In particular there should be a
>>>>>> Set-theoretic model for Agda where Empty -> Box and Box -are- equal:
>>>>>> with a sufficiently clever interpretation of inductives, I believe I
>>>>>> can
>>>>>> get [[Empty -> Box ]] = [[Box]] = { {} } (where {} is just the empty
>>>>>> set). Can someone with more Agda knowledge try to type the original
>>>>>> problematic term?
>>>>>>
>>>>>>
>>>>>> Hypothesis Heq : (False -> False) = True.
>>>>>>
>>>>>> Fixpoint contradiction (u : True) : False :=
>>>>>> contradiction (
>>>>>> match Heq in (_ = T) return T with
>>>>>> | eq_refl => fun f:False => match f with end
>>>>>> end
>>>>>> ).
>>>>>>
>>>>>>
>>>>>>
>>>>>> On 01/06/2014 06:12 PM, Altenkirch Thorsten wrote:
>>>>>>> Hi Maxime,
>>>>>>>
>>>>>>> your postulate seems correct since certainly Empty → Box and Box are
>>>>>>> isomorphic and hence equal as a consequence of univalence.
>>>>>>>
>>>>>>> However, I think the definition of loop looks suspicious in the
>>>>>>> presence
>>>>>>> of proof-relevant equality: if we replace rewrite by an explicit use
>>>>>>> of
>>>>>>> subst, loop isn't structural recursive anymore. Hence my diagnosis
>>>>>>> would
>>>>>>> be that rewrite is simply incompatible with univalence.
>>>>>>>
>>>>>>> Cheers,
>>>>>>> Thorsten
>>>>>>>
>>>>>>> On 06/01/2014 20:42, "Maxime Dénès" <mail at maximedenes.fr> wrote:
>>>>>>>
>>>>>>>> Bingo, Agda seems to have the same problem:
>>>>>>>>
>>>>>>>> module Termination where
>>>>>>>>
>>>>>>>> open import Relation.Binary.Core
>>>>>>>>
>>>>>>>> data Empty : Set where
>>>>>>>>
>>>>>>>> data Box : Set where
>>>>>>>> wrap : (Empty → Box) → Box
>>>>>>>>
>>>>>>>> postulate
>>>>>>>> iso : (Empty → Box) ≡ Box
>>>>>>>>
>>>>>>>> loop : Box -> Empty
>>>>>>>> loop (wrap x) rewrite iso = loop x
>>>>>>>>
>>>>>>>> gift : Empty → Box
>>>>>>>> gift ()
>>>>>>>>
>>>>>>>> bug : Empty
>>>>>>>> bug = loop (wrap gift)
>>>>>>>>
>>>>>>>> However, I may be missing something due to my ignorance of Agda. It
>>>>>>>> may
>>>>>>>> be well known that the axiom I introduced is inconsistent. Forgive
>>>>>>>> me if
>>>>>>>> it is the case.
>>>>>>>>
>>>>>>>> Maxime.
>>>>>>>>
>>>>>>>> On 01/06/2014 01:15 PM, Maxime Dénès wrote:
>>>>>>>>> The anti-extensionality bug is indeed related to termination. More
>>>>>>>>> precisely, it is the subterm relation used by the guard checker
>>>>>>>>> which
>>>>>>>>> is not defined quite the right way on dependent pattern matching.
>>>>>>>>>
>>>>>>>>> It is not too hard to fix (we have a patch), but doing so without
>>>>>>>>> ruling out any interesting legitimate example (dealing with
>>>>>>>>> recursion
>>>>>>>>> on dependently typed data structures) is more challenging.
>>>>>>>>>
>>>>>>>>> I am also curious as to whether Agda is impacted. Let's try it :)
>>>>>>>>>
>>>>>>>>> Maxime.
>>>>>>>>>
>>>>>>>>> On 01/06/2014 12:59 PM, Altenkirch Thorsten wrote:
>>>>>>>>>> Which bug was this?
>>>>>>>>>>
>>>>>>>>>> I only saw the one which allowed you to prove
>>>>>>>>>> anti-extensionality?
>>>>>>>>>> But
>>>>>>>>>> this wasn't related to termination, or?
>>>>>>>>>>
>>>>>>>>>> Thorsten
>>>>>>>>>>
>>>>>>>>>> On 06/01/2014 16:54, "Cody Roux" <cody.roux at andrew.cmu.edu>
>>>>>>>>>> wrote:
>>>>>>>>>>
>>>>>>>>>>> Nice summary!
>>>>>>>>>>>
>>>>>>>>>>>
>>>>>>>>>>> On 01/06/2014 08:49 AM, Altenkirch Thorsten wrote:
>>>>>>>>>>>> Agda enforces termination via a termination checker which is
>>>>>>>>>>>> more
>>>>>>>>>>>> flexible but I think less principled than Coq's approach.
>>>>>>>>>>> That's a bit scary given that there was an inconsistency found
>>>>>>>>>>> in
>>>>>>>>>>> the Coq termination checker just a couple of weeks ago :)
>>>>>>>>>>>
>>>>>>>>>>> BTW, has anyone tried reproducing the bug in Agda?
>>>>>>>>>>>
>>>>>>>>>>>
>>>>>>>>>>> Cody
>>>>>>>>>> This message and any attachment are intended solely for the
>>>>>>>>>> addressee
>>>>>>>>>> and may contain confidential information. If you have received
>>>>>>>>>> this
>>>>>>>>>> message in error, please send it back to me, and immediately
>>>>>>>>>> delete
>>>>>>>>>> it. Please do not use, copy or disclose the information contained
>>>>>>>>>> in
>>>>>>>>>> this message or in any attachment. Any views or opinions
>>>>>>>>>> expressed
>>>>>>>>>> by
>>>>>>>>>> the author of this email do not necessarily reflect the views of
>>>>>>>>>> the
>>>>>>>>>> University of Nottingham.
>>>>>>>>>>
>>>>>>>>>> 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.
>>>>>>>>>>
>>>>>>>>>>
>>>>>>>>>>
>>>>>>>>>>
>>>>>>>>> _______________________________________________
>>>>>>>>> Agda mailing list
>>>>>>>>> Agda at lists.chalmers.se
>>>>>>>>> https://lists.chalmers.se/mailman/listinfo/agda