CakeML/cakeml
better support for translating recursion through higher-order functions
オープン
#9 opened on 2014/12/23
help wantedhigh effortmedium rewardtranslator
Repository metrics
- Stars
- (1,169 個のスター)
- PR merge metrics
- (PR metrics pending)
説明
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