CakeML/cakeml

better support for translating recursion through higher-order functions

Offen

#9 geöffnet am 23.12.2014

Auf GitHub ansehen
 (1 Kommentar) (0 Reaktionen) (1 zugewiesene Person)Standard ML (98 Forks)auto 404
help wantedhigh effortmedium rewardtranslator

Repository-Metriken

Stars
 (1.169 Sterne)
PR-Merge-Metriken
 (PR-Metriken ausstehend)

Beschreibung

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

Contributor Guide

Research-Richtung
Untersuchen Sie die Verwendung des Zertifikatstheorems und des Induktionstheorems; erforschen Sie, wie Zertifikatstheoreme verallgemeinert werden können, um beliebige Vorbedingungen für Argumente von rekursiven Funktionen höherer Ordnung zu erlauben.
Tech Stack
Keine
Domain
compilers
Issue Type
Fehler
SchwierigkeitGeschätzte Implementierungsschwierigkeit für neue Contributors, von 1 für sehr kleine Änderungen bis 5 für Expertenarbeit.
3
Geschätzte ZeitEin grober Zeitrahmen, um zu recherchieren, zu implementieren, zu testen und einen Pull Request vorzubereiten.
1-2 Tage
AktivitätsstatusWie verfügbar das Issue gerade wirkt: frisch, aktiv, stale, blockiert oder wartet auf Maintainer-Input.
Veraltet
KlarheitWie klar das Issue die erwartete Änderung, Akzeptanzkriterien und den nächsten Schritt erklärt.
Klar
Voraussetzungen
Keine
EinsteigerfreundlichkeitEin Score von 1 bis 100, der schätzt, wie zugänglich dieses Issue für First-Time Contributors ist.
30