Einführung Kündigung als Voraussetzung in Leon/Stainless

Question

ich Beweis bin versucht, dass die Bewertung des nicht typisierten Lambda-Kalkül nach folgenden Funktion:

def eval(t: Term): Option[Term] = t match { 
    case App(t1, t2) => eval(t1) match { 
     case Some(Abs(x, body)) => eval(t2) match { 
     case Some(v2) => eval(subst(x, v2, body)) 
     case None() => None[Term]() 
     } 
     case _ => None[Term]() // stuck 
    } 
    case _ => Some(t) // Abs or Var, already a value 
    } 

gibt entweder keine oder einen Wert. Ich wurde jedoch darauf hingewiesen, dass diese Funktion möglicherweise nicht beendet wird. Meine Frage ist, wie kann man in Leon/Stainless einführen, dass eine Funktion beendet werden muss?

Answer 1

Ich bin mir nicht bewusst über eine Möglichkeit, eine Vorbedingung einzuführen, die ausdrücklich besagt "diese Funktion beendet (bei den angegebenen Argumenten)". Sie sollten versuchen, ein höheres Prädikat zu finden, das dem entspricht. In Ihrem Fall wird das nicht funktionieren, weil Sie kein berechenbares Prädikat angeben können, das bestimmt, ob ein Ausdruck im nicht typisierten Lambda-Kalkül eine normale Form hat.

Nicht alles ist jedoch verloren: Der übliche Ansatz ist hier ein zusätzliches "Brennstoff" -Argument des Typs BigInt einzuführen. Es stellt die maximale Anzahl der auszuführenden Reduktionsschritte dar. In jedem Schritt dekrementieren Sie den Kraftstoff um eins. Wenn der Kraftstoff Null ist, brechen Sie die Rekursion ab und geben None zurück. Dies wird trivial Ihre Funktion beenden.

Sie müssen jedoch immer einen "groß genug" Kraftstoff liefern. Normalerweise ist der Treibstoff ein Parameter und das Lemma hat eine Vorbedingung, dass eval(fuel, t) = Some(u).