[Agda] Inteligenta tipa kontrolilo?

[David Raymond Christiansen]

On 04/18/2016 08:22 AM, Serge Leblanc wrote:
> On 04/17/2016 01:00 AM, David Christiansen wrote:
>>> Kial la tipa kontrolilo ne uzas mian antaŭan pruvon 'incX≡' por unuaigi
>>> la tipon ⟨ incΩ (y + x) (suc″ (x , y)) ⟩ kun ⟨ suc x , y ⟩ ?
>> La unuaigilo ne povas uzi pruvojn, ĉar ĝi devus provi ĉiujn pruvojn en
>> la tuta sistemo antaŭ ĝi povus malakcepti programon. Se oni volus havi
>> sistemon en kio la tipkontrolproblemo decideblas, oni devus rekte uzi
>> pruvobjektojn.
>
> Mi supozas ke vi volis paroli pri 'validokonservado' anstataŭ 'decideblo'.
> Efektive, la validokonservado fiaskos se oni aldonas al la tipkontrolilo
> nekonsekvencajn asertojn. Sed, programisto responsas pri tio!
>
> I assume that you wanted to talk about 'inconsistency' instead of
> 'decidability'.
> Indeed, the consistency fail if one adds inconsistencies assertions to
> the type checking. But, the programmer is responsible for this!

No, I wanted to talk about "decidability of the type checking problem" - 
sorry if my Esperanto was not sufficiently good to express that. 
Shouldn't it be "la decidebleco de la tipkontrolproblemo"?

Anyway, if the definitional equality of the type theory is extended 
every time you prove a lemma stating an equality, then the type checking 
problem becomes an arbitrary proof search problem. Otherwise, it is only 
justified in saying "no" when it has a proof in hand that two things 
_cannot_ be equal, because otherwise there might be a proof that it just 
hasn't found. And we know something about consistent formal systems with 
regards to being able to prove all true statements! Thus, in type 
theories like Agda, one must explicitly refer to equality proofs in 
other terms to invoke them.

>>> Ĉu ekzistas metodo por fari tion?
>> Novaj versioj de Agda havas REWRITE-regulojn, sed ĝi estas iomete
>> danĝera. Provu anstataŭe uzi rewrite-sintakson je la maldekstra sido,
>> laŭ:
>> http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.PatternMatching
>>
>
> La dokumento estas ege konciza pri la danĝera REWRITE-regulo :
> http://agda.readthedocs.org/en/latest/language/rewriting.html
> Kie mi trovos pli informojn pri tiu nova regulo ?
>
> The document is very brief about the dangerous Rewrite
> rule:http://agda.readthedocs.org/en/latest/language/rewriting.html
> Where will I find more information about this new rule?

Try the release notes: 
https://github.com/agda/agda/blob/master/CHANGELOG#L1493-L1533

> Sinceran dankon!

Nedankinde :-)

/David