CakeML/cakeml

better support for translating recursion through higher-order functions

Ouverte

#9 ouverte le 23 déc. 2014

Voir sur GitHub
 (1 commentaire) (0 réaction) (1 personne assignée)Standard ML (98 forks)auto 404
help wantedhigh effortmedium rewardtranslator

Métriques du dépôt

Stars
 (1 169 étoiles)
Métriques de merge PR
 (Métriques PR en attente)

Description

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

Guide contributeur

Direction de recherche
Examinez l'utilisation du théorème de certificat et du théorème d'induction ; étudiez comment généraliser les théorèmes de certificat pour permettre des préconditions arbitraires sur les arguments pour les fonctions récursives d'ordre supérieur.
Stack technique
Aucun
Domaine
compilers
Type d'issue
Bug
DifficultéDifficulté estimée pour un nouveau contributeur, de 1 pour un très petit changement à 5 pour un travail expert.
3
Temps estiméFourchette de temps approximative pour investiguer, implémenter, tester et préparer une pull request.
1-2 jours
Statut d'activitéDisponibilité apparente de l'issue : fraîche, active, ancienne, bloquée ou en attente d'un mainteneur.
Ancienne
ClartéClarté avec laquelle l'issue explique le changement attendu, les critères d'acceptation et la prochaine étape.
Claire
Prérequis
Aucun
Accessibilité débutantScore de 1 à 100 estimant l'accessibilité de cette issue pour un premier contributeur.
30