• Andrei Paskevich's avatar
    verify termination (à la Fixpoint) of recursive logic definitions · f92739a1
    Andrei Paskevich authored
    the verification algorithm must always terminate and be reasonably
    performant in practice, but its worst-case complexity is unknown
    and probably exponential. What is quite easy when there is only
    one recursive definition, becomes difficult when there is a group
    of mutually recursive definitions. An educated discussion would
    be highly appreciated.
    
    BTW, I had to convert a couple of recursive "logic"s on integers
    into an abstract "logic" + axiom. Pretty much all of them supposed
    that the argument was non-negative, and thus were non-terminating!
    f92739a1
pretty.ml 18.9 KB