[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