sbv-13.6: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving.
Copyright(c) Levent Erkok
LicenseBSD3
Maintainererkokl@gmail.com
Stabilityexperimental
Safe HaskellNone
LanguageHaskell2010

Documentation.SBV.Examples.TP.Ackermann

Description

Proving the relationship between Ackermann's original 3-argument function (1928) and the Ackermann-Péter function (1935).

Ackermann's original function was a 3-argument function designed to demonstrate a total computable function that is not primitive recursive. The third argument generalizes the operation: ack 0 n a = n + a (addition), and higher levels correspond to multiplication, exponentiation, etc.

Rózsa Péter simplified this to a 2-argument function in 1935, which is what most people today call "the Ackermann function."

This example is inspired by: https://github.com/imandra-ai/imandrax-examples/blob/main/src/ackermann.iml

Note: This proof was developed by Claude (Anthropic's AI assistant) with minimal user prompting and guidance.

Synopsis

Ackermann's original 3-argument function (1928)

ack :: SInteger -> SInteger -> SInteger -> SInteger Source #

Ackermann's original 3-argument function (1928). This is the lesser-known original version, not the commonly referenced Ackermann-Péter function. The third argument a generalizes the operation at each level.

Ackermann-Péter function (1935)

pet :: SInteger -> SInteger -> SInteger Source #

The Ackermann-Péter function (1935), commonly known as "the Ackermann function." This is Rózsa Péter's simplified 2-argument version of Ackermann's original function.

Correctness

ack_2_2_4 :: TP (Proof (Forall "m" Integer -> SBool)) Source #

Prove that ack m 2 2 = 4 for all m >= 0.

>>> runTP ack_2_2_4
Inductive lemma (strong): ack_2_2_4
  Step: Measure is non-negative         Q.E.D.
  Step: 1 (2 way case split)
    Step: 1.1                           Q.E.D.
    Step: 1.2.1                         Q.E.D.
    Step: 1.2.2                         Q.E.D.
    Step: 1.2.3                         Q.E.D.
    Step: 1.2.4                         Q.E.D.
    Step: 1.Completeness                Q.E.D.
  Result:                               Q.E.D.
[Proven] ack_2_2_4 :: Ɐm ∷ Integer → Bool

ack_psd :: TP (Proof (Forall "m" Integer -> Forall "n" Integer -> Forall "a" Integer -> SBool)) Source #

Prove that ack is non-negative when all arguments are non-negative. We use strong induction on the lexicographic measure (m, n).

>>> runTP ack_psd
Inductive lemma (strong): ack_psd
  Step: Measure is non-negative         Q.E.D.
  Step: 1 (4 way case split)
    Step: 1.1                           Q.E.D.
    Step: 1.2                           Q.E.D.
    Step: 1.3                           Q.E.D.
    Step: 1.4.1                         Q.E.D.
    Step: 1.4.2                         Q.E.D.
    Step: 1.4.3                         Q.E.D.
    Step: 1.Completeness                Q.E.D.
  Result:                               Q.E.D.
[Proven] ack_psd :: Ɐm ∷ Integer → Ɐn ∷ Integer → Ɐa ∷ Integer → Bool

pet_psd :: TP (Proof (Forall "m" Integer -> Forall "n" Integer -> SBool)) Source #

Prove that pet is non-negative when both arguments are non-negative. We use strong induction on the lexicographic measure (m, n).

>>> runTPWith cvc5 pet_psd
Inductive lemma (strong): pet_psd
  Step: Measure is non-negative         Q.E.D.
  Step: 1 (3 way case split)
    Step: 1.1                           Q.E.D.
    Step: 1.2.1                         Q.E.D.
    Step: 1.2.2                         Q.E.D.
    Step: 1.2.3                         Q.E.D.
    Step: 1.3.1                         Q.E.D.
    Step: 1.3.2                         Q.E.D.
    Step: 1.3.3                         Q.E.D.
    Step: 1.Completeness                Q.E.D.
  Result:                               Q.E.D.
[Proven] pet_psd :: Ɐm ∷ Integer → Ɐn ∷ Integer → Bool

petAck :: TP (Proof (Forall "m" Integer -> Forall "n" Integer -> SBool)) Source #

The main theorem, relating pet and ack: pet m n + 3 = ack (m-1) (n+3) 2 for m > 0 and n >= 0.

>>> runTPWith cvc5 petAck
Inductive lemma (strong): ack_2_2_4
  Step: Measure is non-negative         Q.E.D.
  Step: 1 (2 way case split)
    Step: 1.1                           Q.E.D.
    Step: 1.2.1                         Q.E.D.
    Step: 1.2.2                         Q.E.D.
    Step: 1.2.3                         Q.E.D.
    Step: 1.2.4                         Q.E.D.
    Step: 1.Completeness                Q.E.D.
  Result:                               Q.E.D.
Inductive lemma (strong): pet_psd
  Step: Measure is non-negative         Q.E.D.
  Step: 1 (3 way case split)
    Step: 1.1                           Q.E.D.
    Step: 1.2.1                         Q.E.D.
    Step: 1.2.2                         Q.E.D.
    Step: 1.2.3                         Q.E.D.
    Step: 1.3.1                         Q.E.D.
    Step: 1.3.2                         Q.E.D.
    Step: 1.3.3                         Q.E.D.
    Step: 1.Completeness                Q.E.D.
  Result:                               Q.E.D.
Inductive lemma (strong): petAck
  Step: Measure is non-negative         Q.E.D.
  Step: 1 (4 way case split)
    Step: 1.1                           Q.E.D.
    Step: 1.2.1                         Q.E.D.
    Step: 1.2.2                         Q.E.D.
    Step: 1.2.3                         Q.E.D.
    Step: 1.3.1                         Q.E.D.
    Step: 1.3.2                         Q.E.D.
    Step: 1.3.3                         Q.E.D.
    Step: 1.3.4                         Q.E.D.
    Step: 1.3.5                         Q.E.D.
    Step: 1.4.1                         Q.E.D.
    Step: 1.4.2                         Q.E.D.
    Step: 1.4.3                         Q.E.D.
    Step: 1.4.4                         Q.E.D.
    Step: 1.4.5                         Q.E.D.
    Step: 1.Completeness                Q.E.D.
  Result:                               Q.E.D.
[Proven] petAck :: Ɐm ∷ Integer → Ɐn ∷ Integer → Bool