search

abau / co4

COmplexity COncerned COnstraint COmpiler
GNU General Public License v3.0
2 stars 3 forks source link

abstract evaluation introduces non-termination (could be improved by incremental solving) #45

Closed jwaldmann closed 11 years ago

jwaldmann commented 11 years ago

the concrete program is terminating (for all arguments) but the abstract program (currently) is not.

with incremental feasibility checking, abstract evaluation should detect that "case u of True ..." cannot happen in the inner call.

constraint k u = case u of
            False -> k
            True -> constraint (not k) False

https://github.com/apunktbau/co4/blob/f5b8b0d9e3d3b018d7f437be5514ac5fc7b1aeaf/CO4/Test/Termination1.hs#L25

abau commented 11 years ago

seems to be fixed