[Agda] Re: How can I prove associativity of vectors?
Frédéric Blanqui
frederic.blanqui at inria.fr
Wed Dec 17 17:55:17 CET 2014
Hi.
Le 17/12/2014 17:26, Andrea Vezzosi a écrit :
> Right, but how are these enforced?
In CoqMT, there is no rewrite rule, just decision procedures for some
theories.
In Dedukti, there is currently nothing enforcing termination nor
confluence. :-( But there are various criteria (e.g. the technique of
size annotations used in Agda can be extended to rewriting) and tools
for this:
- There are the termination provers Wanda, THOR or HOT (see
http://termination-portal.org/wiki/Termination_Competition), but they
currently handle simply typed rewrite systems only.
- There are also various confluence provers (see
http://coco.nue.riec.tohoku.ac.jp/) but they do not handle higher-order
rewrite systems I think. But, if you already have termination,
confluence reduces to local confluence, which can then be decided by
checking that two critical pairs have the same normal form. In case your
system is not confluent, you may need to complete it by new rules, but
this process may not end (see Knuth-Bendix completion). For this
purpose, there are also a number of tools like Waldmeister or mkbTT but
they do not handle higher-order rewrite systems.
> Is the user required to provide a formal proof?
Some of the results of the above tools can be certified by using for
instance TTT2 or Rainbow.
> Is there some modular
> criterion, or do the proofs need to be done for the whole rewriting
> system at once?
It depends on the criteria... but, yes, many of them are (mostly)
modular. Note however that, in general, termination is NOT modular: if
R1 and R2 are two DISJOINT terminating systems then it might be the case
that R1 U R2 does not terminate (see Toyama 1987).
Best regards,
Frédéric.
> 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