[Agda] Re: How can I prove associativity of vectors?

Andrea Vezzosi sanzhiyan at gmail.com
Wed Dec 17 17:26:53 CET 2014


Right, but how are these enforced?

Is the user required to provide a formal proof? Is there some modular
criterion, or do the proofs need to be done for the whole rewriting
system at once?

On Wed, Dec 17, 2014 at 4:43 PM, Frédéric Blanqui
<frederic.blanqui at inria.fr> wrote:
> Termination and confluence.
>
> Le 17/12/2014 16:34, Andrea Vezzosi a écrit :
>
>> Hi,
>>
>> What kind of restrictions do these systems impose on the rewrite rules
>> to keep equality checking decidable?
>>
>> Best,
>> Andrea
>>
>> On Wed, Dec 17, 2014 at 4:21 PM, Frédéric Blanqui
>> <frederic.blanqui at inria.fr> wrote:
>>>
>>> Hello.
>>>
>>> Another alternative is to extend the congruence on types while keeping it
>>> decidable. For instance, it is possible to extend it with the equation
>>> (x+y)+z = x+(y+z) on ℕ, which is an inductive consequence of the
>>> definition
>>> of +. This is done for instance in:
>>>
>>> - http://dedukti.gforge.inria.fr/ is a proof-checker for LF where the
>>> congruence on types includes non only beta-reduction but also
>>> user-defined
>>> rewrite rules, of which (x+y)+z -> x+(y+z) on ℕ is a particular case.
>>> Type-level rewriting is very powerful since it allows to encode any
>>> functional pure type systems (PTS) in LF + user-defined rewrite rules.
>>>
>>> - http://pierre-yves.strub.nu/coqmt/ is an extension of Coq where the
>>> congruence on types in some context Gamma is extended with all the
>>> propositional consequences one can deduce from Gamma modulo some
>>> decidable
>>> theory like linear arithmetic, of which (x+y)+z = x+(y+z) on ℕ is a
>>> particular case.
>>>
>>> Best regards,
>>>
>>> Frédéric.
>>>
>>> Le 17/12/2014 16:00, Jon Sterling a écrit :
>>>
>>>> Sergei,
>>>>
>>>> On Wed, Dec 17, 2014, at 01:28 AM, Sergei Meshveliani wrote:
>>>>>
>>>>> On Wed, 2014-12-17 at 12:02 +0900, Kenichi Asai wrote:
>>>>>>
>>>>>> Thank you for the messages!  I could now implement it in two ways.
>>>>>>
>>>>>>>    * Use Data.Vec.Equality rather than PropositionalEquality.
>>>>>>
>>>>>> [..]
>>>>>>>
>>>>>>>    * Use Relation.Binary.HeterogeneousEquality rather than
>>>>>>>      PropositionalEquality.
>>>>>>
>>>>>> [..]
>>>>>> assoc : ∀ {l m n} → (l1 : Vec ℕ l) → (l2 : Vec ℕ m) → (l3 : Vec ℕ n) →
>>>>>>           (l1 ++ l2) ++ l3 ≅ l1 ++ (l2 ++ l3)
>>>>>> assoc [] l2 l3 = refl
>>>>>> assoc (x ∷ l1) l2 l3 = cong (λ l → x ∷ l) (assoc l1 l2 l3)
>>>>>>
>>>>>> but it did not work, because cong appears to assume that two sides of
>>>>>> ≅ has the same type.  Why is it so?  I think it is more natural that
>>>>>> cong etc. in HeterogeneousEquality module are defined for
>>>>>> heterogeneous
>>>>>> types.
>>>>>> [..]
>>>>>
>>>>>
>>>>> People,
>>>>> this whole feature looks like a point of disagreement of Agda to
>>>>> mathematics.
>>>>>
>>>>> In both areas, a domain can depend on a value, and can be treated as a
>>>>> value (to a certain extent).
>>>>>
>>>>> A mathematical computation and discourse can be as follows.
>>>>>
>>>>>     For all  k : Nat  define an additive semigroup on  (Vec Nat k)
>>>>>     with respect to the pointwise addition  _+l_  on vectors.
>>>>>
>>>>>     Put      Vec1 = Vec Nat (m + n),   Vec2 = Vec Nat (m + n),
>>>>>     and let  v  \in Vec1,              v' \in Vec2.
>>>>>
>>>>>     Let us prove  m + n == n + m.
>>>>>     ...
>>>>>     All right, proved.
>>>>>
>>>>>     Hence,  v and v'  belong to the _same_ domain  Vec1,  and to the
>>>>> same
>>>>>     additive semigroup H1. Hence it has sense the computation
>>>>>
>>>>>       _+1_ = Semigroup._*_ H1;
>>>>>       u    = v +1 v';
>>>>>
>>>>>     and so on.
>>>>>
>>>>> This discourse uses that _identity_ of domains respects the equality
>>>>> _==_  on parameter values.
>>>>>
>>>>> And in a dependently typed language, one has:
>>>>>
>>>>>     m + n == m + n  proved,  and still  v and v'  are of different
>>>>>     types (domains), and cannot be added by the semigroup operation
>>>>> _+1_.
>>>>>
>>>> With regard to this comment:
>>>>
>>>>> In mathematics, the domain membership relation  v \in V(p)  can often
>>>>> be
>>>>> proved or computed. And in a dependently typed language, the relation
>>>>> v : V(p)  has somewhat a different nature, this is not of  (Rel _),  it
>>>>> is a language construct.
>>>>>
>>>>> I do not expect that this difference can be eliminated by some kind of
>>>>> refining a language design.
>>>>
>>>> It may be a digression from the point of this thread, but I'll note that
>>>> this is not an "essential" property of type theory. Type theories based
>>>> on Martin-Löf's 1986 logical framework presentation, such as the theory
>>>> underlying Agda, typically do not have a judgement "M in A" which means
>>>> "M is a member of domain A" but rather they have a proofhood judgement,
>>>> "M is a proof of A". In order for it to be meaningful, this judgement
>>>> must be analytic, so it cannot be proved, it can only be "known".
>>>>
>>>> But other type theories, such as Computational Type Theory (Nuprl) which
>>>> expands on Martin-Löf's polymorphic type theory from the early 80s, do
>>>> not internally have a judgement like Agda's but instead have a judgement
>>>> "A ext M" which means "M is a witness for A" or "M is a realizer for A".
>>>> And this judgement behaves more like the domain membership relation
>>>> you're talking about, and it can be proved in the logical framework.
>>>>
>>>> Common practice in the modern intensional LF presentation of type theory
>>>> (see Nordström for some examples, also Sambin, though their approaches
>>>> differ) is to overlay a "subset theory" on top of the theory.
>>>>
>>>>> And what a programmer has to do?
>>>>>
>>>>> May be, one needs in each case to implement a certain appropriate
>>>>> natural isomorpsims. In our example, this is  f : Vec2 -> Vec1,
>>>>> and to apply   v +1 (f v')  rather than  (v +1 v').
>>>>> -- ?
>>>>>
>>>>> Am I missing something?
>>>>>
>>>>> Regards,
>>>>>
>>>>> ------
>>>>> Sergei
>>>>
>>>> Kind regards,
>>>> Jon
>>>>
>>>>>
>>>>>
>>>>>
>>>>>
>>>>>
>>>>> _______________________________________________
>>>>> Agda mailing list
>>>>> Agda at lists.chalmers.se
>>>>> https://lists.chalmers.se/mailman/listinfo/agda
>>>>
>>>> _______________________________________________
>>>> Agda mailing list
>>>> Agda at lists.chalmers.se
>>>> https://lists.chalmers.se/mailman/listinfo/agda
>>>
>>>
>>> _______________________________________________
>>> Agda mailing list
>>> Agda at lists.chalmers.se
>>> https://lists.chalmers.se/mailman/listinfo/agda
>
>


More information about the Agda mailing list