[Agda] Checking termination is not sufficiently exploratory.

[Serge Leblanc]

When the termination checking fails you can complete it again on a
normalized part of the program. Then the speed is completely preserved
because we will rarely need normalization passe . Therefore, normalized
parts could be stored and used during coding generation.

Kiam la sintaksa finiĝokontrolo fiaskas oni povas denove plenumi ĝin sur
normalita parto de la programo. Tiam la rapideco estas tute konservita
pro oni malofte bezonos nomaladan fazon. Sekve, normalitaj partoj povus
esti konservi kaj uzitaj dum la kodokonstuado.

On 2018-07-31 03:19, Jason -Zhong Sheng- Hu wrote:
>
> I am wondering if there is any implementation of dependent type theory
> performs normalization before termination checking?
>
>
> It sounds theoretical doable, but somehow termination checking is
> commonly syntactical, like agda and coq. However, those who care about
> compilation performance might not be too happy about it.
>
>
> I am wondering if there is an example makes normalization here looks
> non-trivial?
>
>

-- 
Serge Leblanc
------------------------------------------------------------------------
gpg --search-keys 0x67B17A3F
Fingerprint = 2B2D AC93 8620 43D3 D2C2 C2D3 B67C F631 67B1 7A3F
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180731/65eb2df1/attachment.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 195 bytes
Desc: OpenPGP digital signature
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180731/65eb2df1/attachment.sig>