CakeML/cakeml

better support for translating recursion through higher-order functions

Aperta

#9 aperta il 23 dic 2014

Vedi su GitHub
 (1 commento) (0 reazioni) (1 assegnatario)Standard ML (98 fork)auto 404
help wantedhigh effortmedium rewardtranslator

Metriche repository

Star
 (1169 stelle)
Metriche merge PR
 (Metriche PR in attesa)

Descrizione

The translator works on recursive functions that recurse as an argument to MAP (and maybe some other simple functions), but in general recursion as an argument to a higher-order function makes the translator fail when attempting to prove the certificate theorem using the induction theorem. A solution to the problem will probably require a more general form of certificate theorems (in particular, allowing arbitrary preconditions on arguments).

See this thread: https://lists.cakeml.org/private/dev/2014-December/000662.html

Guida contributor

Direzione di ricerca
Esamina l'uso del teorema del certificato e del teorema di induzione; studia come generalizzare i teoremi del certificato per consentire precondizioni arbitrarie sugli argomenti per funzioni ricorsive di ordine superiore.
Tech stack
Nessuno
Dominio
compilers
Tipo issue
Bug
DifficoltàQuanto dovrebbe essere impegnativa per un nuovo contributor.
3
Tempo stimatoTempo stimato per completare e verificare uno scope piccolo.
1-2 giorni
Stato attivitàQuanto è probabile che la issue sia ancora attiva e reviewable.
Datata
ChiarezzaQuanto chiaramente la issue descrive problema, scope e risultato atteso.
Chiara
Prerequisiti
Nessuno
Adatta ai principiantiQuanto la issue è adatta a contributor alla prima esperienza.
30