From 510623d57984f81105c621c898c60c79d3a32c0f Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Tue, 8 Sep 2015 17:08:06 -0700 Subject: Proof that Ackermann can be curried and that it is monotonic in both arguments. --- Test/dafny4/Ackermann.dfy | 235 ++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 235 insertions(+) create mode 100644 Test/dafny4/Ackermann.dfy (limited to 'Test/dafny4/Ackermann.dfy') diff --git a/Test/dafny4/Ackermann.dfy b/Test/dafny4/Ackermann.dfy new file mode 100644 index 00000000..7ab686e0 --- /dev/null +++ b/Test/dafny4/Ackermann.dfy @@ -0,0 +1,235 @@ +// RUN: %dafny /compile:3 /rprint:"%t.rprint" /autoTriggers:1 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +// Rustan Leino, 8 Sep 2015. +// This file proves that the Ackermann function is monotonic in each argument + +method Main() { + // Note, don't try much larger numbers unless you're prepared to wait! + print "Ack(3, 4) = ", Ack(3, 4), "\n"; +} + +// Here is the definition of the Ackermann function: +function method Ack(m: nat, n: nat): nat +{ + if m == 0 then + n + 1 + else if n == 0 then + Ack(m - 1, 1) + else + Ack(m - 1, Ack(m, n - 1)) +} + +// And here is the theorem that proves the desired result: +lemma AckermannIsMonotonic(m: nat, n: nat, m': nat, n': nat) + requires m <= m' && n <= n' + ensures Ack(m, n) <= Ack(m', n') +{ + // This is the proof. It calls two lemmas, stated and proved below. + MonotonicN(m, n, n'); + MonotonicM(m, n, m'); +} + +// -------------------------------------------------------- +// What follows are the supporting lemmas and their proofs. +// -------------------------------------------------------- + +// Proving that Ackermann is monotonic in its second argument is easy. +lemma MonotonicN(m: nat, n: nat, n': nat) + requires n <= n' + ensures Ack(m, n) <= Ack(m, n') +{ + // In fact, Dafny completes this proof automatically. +} + +// To prove the other direction, we consider an alternative formulation +// of the Ackermann function, namely a curried form: +function CurriedAckermann(m: int, n: int): int +{ + A(m)(n) +} + +function A(m: int): int -> int +{ + if m <= 0 then + n => n + 1 + else + n => Iter(A(m-1), n) +} + +function Iter(f: int -> int, n: int): int + requires IsTotal(f) + decreases n +{ + if n <= 0 then + f(1) + else + f(Iter(f, n-1)) +} + +// In the 3-part definition above, function Iter needs to know that it can +// apply its function parameter "f". Therefore, Iter's precondition says that +// "f" must be total. We define totality of "f" by saying that its precondition +// holds for any n and that it never reads the heap: +predicate IsTotal(f: int -> int) + reads f.reads +{ + forall n :: f.requires(n) && f.reads(n) == {} +} + +// Now, we can prove certain things about CurriedAckermann. The first thing we +// prove is that it gives the same result as the Ack function above. + +lemma CurriedIsTheSame(m: nat, n: nat) + ensures CurriedAckermann(m, n) == Ack(m, n) +{ + // The proof considers 3 cases, following the 3 cases in the definition of Ack + if m == 0 { + // trivial + } else if n == 0 { + // trivial + } else { + // we help Dafny out with the following lemma: + assert A(m)(n) == A(m-1)(Iter(A(m-1), n-1)); + } +} + +// Monotonicity in the first argument of Ackermann now follows from the fact that, +// for m <= m', A(m) is a function that is always below A(m') +lemma MonotonicM(m: nat, n: nat, m': nat) + requires m <= m' + ensures Ack(m, n) <= Ack(m', n) +{ + CurriedIsTheSame(m, n); + CurriedIsTheSame(m', n); + ABelow(m, m'); +} + +// We must now prove ABelow. To do that, we will prove some properties of A and of +// Iter. Let us define the three properties we will reason about. + +// The first property is a relation on functions. It is the property that above was referred +// to as "f is a function that is always below g". The lemma ABelow(m, m') used above establishes +// FunctionBelow(A(m), A(m')). +predicate FunctionBelow(f: int -> int, g: int -> int) + requires IsTotal(f) && IsTotal(g) +{ + forall n :: f(n) <= g(n) +} + +// The next property says that a function is monotonic. +predicate FunctionMonotonic(f: int -> int) + requires IsTotal(f) +{ + forall n,n' :: n <= n' ==> f(n) <= f(n') +} + +// The third property says that a function's return value is strictly greater than its argument. +predicate Expanding(f: int -> int) + requires IsTotal(f) +{ + forall n :: n < f(n) +} + +// We will prove that A(_) satisfies the properties FunctionBelow, FunctionMonotonic, and +// FunctionExpanding. But first we prove three properties of Iter. + +// Provided that "f" is monotonic and expanding, Iter(f, _) is monotonic. +lemma IterIsMonotonicN(f: int -> int, n: int, n': int) + requires IsTotal(f) && Expanding(f) && FunctionMonotonic(f) && n <= n' + ensures Iter(f, n) <= Iter(f, n') +{ + // This proof is a simple induction over n' and Dafny completes the proof automatically. +} + +// Next, we prove that Iter(_, n) is monotonic. That is, given functions "f" and "g" +// such that FunctionBelow(f, g), we have Iter(f, n) <= Iter(g, n). The lemma requires +// "f" to be monotonic, but we don't have to state the same property for g. +lemma IterIsMonotonicF(f: int -> int, g: int -> int, n: int) + requires IsTotal(f) && IsTotal(g) && FunctionMonotonic(f) && FunctionBelow(f, g) + ensures Iter(f, n) <= Iter(g, n) +{ + // This proof is a simple induction over n and Dafny completes the proof automatically. +} + +// Finally, we shows that for any expanding function "f", Iter(f, _) is also expanding. +lemma IterExpanding(f: int -> int, n: int) + requires IsTotal(f) && Expanding(f) + ensures n < Iter(f, n) +{ + // Here, too, the proof is a simple induction of n and Dafny completes it automatically. +} + +// We complete the proof by showing that A(_) has the three properties we need. + +// Of the three properties we prove about A(_), we start by showing that A(m) returns a +// function that is expanding. +lemma AExp(m: int) + ensures Expanding(A(m)) +{ + if m <= 0 { + // trivial + } else { + // This branch of the proof follows from the fact that Iter(A(m-1), _) is expanding. + forall n { + // The following lemma requires A(m-1) to be expanding, which is something that + // following from our induction hypothesis. + IterExpanding(A(m-1), n); + } + } +} + +// Next, we show that A(m) returns a monotonic function. +lemma Am(m: int) + ensures FunctionMonotonic(A(m)) +{ + if m <= 0 { + // trivial + } else { + // We make use of the fact that A(m-1) is expanding: + AExp(m-1); + // and the fact that Iter(A(m-1), _) is monotonic: + forall n,n' | n <= n' { + // The following lemma requires A(m-1) to be expanding and monotonic. + // The former comes from the invocation of AExp(m-1) above, and the + // latter comes from our induction hypothesis. + IterIsMonotonicN(A(m-1), n, n'); + } + } +} + +// Our final property about A, which is the lemma we had used above to prove +// that Ackermann is monotonic in its first argument, is stated and proved here: +lemma ABelow(m: int, m': int) + requires m <= m' + ensures FunctionBelow(A(m), A(m')) +{ + if m' <= 0 { + // trivial + } else if m <= 0 { + forall n { + calc { + A(m)(n); + == + n + 1; + <= { AExp(m'-1); IterExpanding(A(m'-1), n); } + Iter(A(m'-1), n); + == + A(m')(n); + } + } + } else { + forall n { + calc { + A(m)(n); + == + Iter(A(m-1), n); + <= { Am(m-1); ABelow(m-1, m'-1); + IterIsMonotonicF(A(m-1), A(m'-1), n); } + Iter(A(m'-1), n); + == + A(m')(n); + } + } + } +} -- cgit v1.2.3