Functions & Induction in Athena: Part 1
Tannr October 15, 2022 [Tutorials] #Proofs #Athena #Functional Programming #InductionIntroduction
This tutorial provides a hands-on introduction to the Athena programming language. Athena is more than a programming language, though. It is also:
- A proof language. I.e., it can be used to express logical proofs. A proof's execution completely successfully if and only if the proof is valid. Proofs in Athena are written in a natural deduction style, which closely resembles the intuitive style of "proofs on paper".
- A proof assistant. I.e., a proof developer can write custom tactics/automated proof procedures, lending itself well to automation. Further, it has built-in integrations to standard external SMT solvers & automated theorem provers.
Tutorial Goals & Pre-requisites
Proof development, much like software development, is an iterative process. The goal of this tutorial is not only to show how to use basic features of Athena to express functions and proofs, but to demonstrate how Athena can help proof engineers through the process of proof discovery, incremental proof development, as well as presentation.
This tutorial does not assume any prior experience with the Athena language, though it does assume that the reader understands a select set of basic topics in discrete mathematics, such as induction, set theory, and logic. This tutorial also assumes that the reader has experience with at least one programming language.
I highly suggest that readers follow along by writing and running each example. The quickest way to do this is to simply open the Athena Playground in a separate browser window and create a new file to get started. You'll also find the code for this tutorial under the "tutorials" tab in the playground.
For local installations, please read Athena's installation instructions.
A Functional Program
Our goal today is to prove a particular property about factorials.
Recall that the factorial of some number $n$ is written as $n!$ and is defined like so:
$n! = n \times (n - 1) \times (n - 2) \times ... \times 2 \times 1$
Sequences & Recurrence Relations
The factorial function defines a recurrence relation. A recurrence relation is a special kind of relation that defines rules for generating sequence... a sequence is a function for which the domain is a consecutive subset of integers (such as ${0, 1, 2, 3, 4}$). Oftentimes, the domain of a sequence is referred to as the "index set". A sequence of values is analogous to "array" structure provided by many programming languages.
A recurrence relation maps the first $k$ elements of the index set to fixed values. It defines all other values in terms of one or more previously-occurring values in the sequence. The definition of the factorial function as a recurrence relation looks like this:
$F_{0} = 1$
$F_{1} = 1$
$F_{n} = n * F_{n-1} \ \ \ for \ n \gt 1$
The Factorial in Athena
Because Athena provides capabilities to write both programs and proofs, let's begin by writing a simple functional program that computes the factorial of some number.
define [- <] := [minus less?]
define factorial := lambda (n) (
check {
(n < 1) => 1
| else => (times (factorial(n - 1)) n)
}
)
(eval factorial(5))
A few observations can be made about the above code.
First, we can bind a function to a name using the define keyword.
Second, functions can be defined via the lambda keyword, followed by parenthesized named parameters (n in this case) and then a parenthesized body: lambda (params) (body).
Third, if/else statements can be expressed in Athena with check statements. check statements have the following structure check { condition => result1 | else => result 2}.
Functions to Proofs
Now that we've defined a procedure to compute a factorial, it'd be useful if we could prove some properties about it.
For example, we know intuitively that $5! \gt 4!$. In fact, we know that for any number greater than 1, factorial n < factorial n + 1.
To prove this, we first need to axiomatize our factorial function.
Axiomatic Factorial
Let's begin by defining a module for our work. Modules allow us to encapsulate all of our definitions, axioms, and proofs into a nicely packaged theory.
We will also include as a dependency a built-in Athena module that provides an axiomatic definition of the natural numbers as well as axiomatic definitions & theorems for addition, multiplication, subtraction, and the "less-than" relation (i.e., the definition of the < as well as the <= symbol).
load "nat-less"
module Factorial {
}
Next, let's declare a function symbol, factorial whose domain and co-domain are both the natural numbers (denoted by N). We'll also give it
load "nat-less"
module Factorial {
declare factorial: [N] -> N
}
Let's run this to ensure that the module is successfully defined. When you run this, you will notice significantly more output than when we defined factorial with a lambda expression. This output is coming from the nat-less file and describes the theorems & definitions contained therein.
You should see the following lines at the end of the output:
New symbol Factorial.factorial declared.
Module Factorial defined.
Equational Axioms
Let's now write some equational axioms. Recall that we have already defined a recurrence relation for the factorial function. All we need to do is translate that relation to Athena.
As a reminder, this is the recurrence relation we're using:
$F_{0} = 1$
$F_{n} = n * F_{n-1} \ \ \ for \ n \gt 1$
We can specify this in athena with a list of equational axioms:
define [< * one zero <=] := [N.< N.* (S N.zero) N.zero N.<= ]
assert fact-def := [
(factorial zero = one)
(factorial one = one)
(forall ?n:N . factorial S n = S n * factorial n)
]
We can make this even prettier as well by removing the quantifier of the last rule, as well as the explicit ?n:N declaration (which indicates that n is a free variable representing some element in the set of natural numbers N).
The former is achieved by the assert* directive, which automatically universally quantifies the free variables we use in our sentences. We also go ahead and define some variable names to use later in proofs for convenience:
define [n m k] := [?n:N ?m:N ?k:N]
assert* fact-def := [
(factorial zero = one)
(factorial one = one)
(factorial S n = S n * factorial n)
]
Remember that we loaded in a module at the top of the file with load "nat-less". This module brings into scope a formal definition of the natural numbers, as well as formal definitions of < and <=. We will be using the definition of <= from that module by referencing it directly: N.Less=.<=-def. For convenience, let's just bind the axiomatic definitions to a simpler name, local to our module: define [lte-def] := N.Less=.<=-def.
Testing
Now that we have an initial axiomatic definition, we should spend a few minutes writing some simple tests to make sure we're on the right tack.
Our factorial function is defined using natural numbers N. N is an inductively defined set: datatype N := zero | (S N). You may recognize this definition as the so-called Peano representation of natural numbers.
Larger numbers are harder to read and write directly. Six, for example, looks like this: (S (S (S (S (S (S zero)))))). It'd be much more convenient if we could write factorial 6 in our test case instead of (factorial (S (S (S (S (S (S zero))))))). Similarly, we would like to view the output of a factorial evaluation as a standard integer rather than a long list of S's.
To convert any integer inputs to N in our factorial function, we can revise our declaration like so: declare factorial: [N] -> N [[int->nat]]. The list of options that appear after the function signature can include a variety of ways, including adding aliases, setting precedence level, and more.
The way we actually test our axiomatized function is by using Athena's built-in eval utility, which, given a term, will continually rewrite the term based on axioms in the assumption base about that term. Since we will be evaluating the factorial function over N, let's make eval transform its output from N to integers whenever an eval execution results in term of sort N.
(transform-output eval [nat->int])
The entire module should now look something like this (observe the test using eval at the bottom):
load "nat-less"
module Factorial {
declare factorial: [N] -> N [factorial [int->nat]]
define [< * one zero <=] := [N.< N.* (S N.zero) N.zero N.<= ]
define [n m k] := [?n:N ?m:N ?k:N]
define [lte-def] := N.Less=.<=-def
assert* fact-def := [
(factorial zero = one)
(factorial one = one)
(factorial S n = S n * factorial n)
]
(eval factorial 5) # 120
}
If you run this, you'll notice that Athena outputs a message saying "Module Factorial was not successfully defined." and it will also print 120, indicating the result of computing $5!$.
A Proof About Factorials
With our factorial algorithm now axiomatized, we can now prove properties about the result(s) of its execution.
Mathematical Induction
The proof technique we will use is induction over the natural numbers.
A proof by induction roughly has two parts:
- Proof of the base case
- Proof that $P(a_{n}) \to P(a_{n+1})$ for some property $P$ over a sequence $a$.
Our Goal
Let's define our proof goal. As mentioned earlier in this tutorial, we want to prove that, for all natural numbers, $F_{n} < F_{n+1}$ where $F$ is the factorial function.
Let's write that in Athena:
define theorem := (forall n . factorial n <= factorial S n)
Incremental Proof Development with "Stubs"
Oftentimes, writing proofs is a gradual and creative process. Like in software development, proof development is often made easier by the ability to incrementally build towards the final deliverable, with the ability to check one's work along the way. For example, I use the Rust language on a daily basis, and when I'm building out a new module or interface, I'll often add stubs to my functions so that I can focus on the type signatures of the interface without the compiler scolding me:
The todo!() macro comes in really handy in these situations.
Athena provides a similar mechanism for "stubbing" portions of a proof so that we can get the structure right before moving on.
Before we jump right into Athena, let's first understand the base case and inductive step less formally:
$ Let \ P_{n} = 1 \lt n \to F_{n-1} \lt F_{n}$
$ Goal: \forall n \in \N \ | P_{n}$
$ Proof: By \ induction \ over \ n$
$ Base \ case: n = 0 \ and \ P_{0} $
$ Inductive \ step: Assume \ F_{n} < F_{n + 1}.\\ \ \ \ \ \ \ \ \ Prove \ that \ F_{n-1} \lt F_{n} \to F_{n} \lt F_{n + 1}$
Let's define this in Athena using Athena's by-induction proof method.
by-induction theorem {
zero => ...
| (S zero) => ...
| (n as (S m)) => ,..
}
The body of by-induction expects zero as the base case because the natural numbers N are inductively defined, with zero as the base constructor.
When we induct over the property (forall n . factorial n <= factorial S n ), this property is instantiated with the base case into a zero-order proposition where n is substituted for the base element: factorial zero <= factorial S zero.
Notice that our proof by induction skeleton uses two base cases. This is because two out of our three axioms about factorial have, on the right side of the =, non-reducible ground terms. So they are already fully reduced or normalized.
Let's fill this skeleton in and, while we're at it, let's use Athena's !force method to "stub" our proof of each case:
by-induction theorem {
zero => (!force (factorial zero <= factorial S zero))
| (S zero) => (!force (factorial S zero <= factorial S S zero))
| (n as (S m)) => (!force (factorial S m <= factorial S S m))
}
This is the skeleton of our inductive proof. Now's a perfect time to perform a sanity check to ensure that we've correctly defined the conclusion for both base cases and the inductive step.
This is why the proof method !force is so useful: we can check that our definition of the base case(s) and inductive step are correct early on, rather than waiting until we've provided complete derivations of all conclusions, only to discover we were working towards the wrong goal the whole time.
If you've followed along, you should see the following at the end of Athena's output:
Theorem: (forall ?n:N
(N.<= (Factorial.factorial ?n:N)
(Factorial.factorial (S ?n:N))))
Module Factorial defined.
This is exactly what our sentence theorem expresses. The only differences being that Athena's output is in prefix notation, outputs the module names associated with function symbols, and annotates variables such as n with its Sort (analogous to a "type").
Proving the Base Cases
Proving that factorial zero <= factorial S zero amounts to proving that they are equal (which is trivial since we have two axioms that say they are equal). After we prove they're equal, all we have to do is derive the <= relation from the = relation.
zero => (!chain-> [
(factorial zero)
= one [fact-def]
= (factorial one) [fact-def]
==> ((factorial zero) <= (factorial one)) [lte-def]
])
This proof uses a mixture of equational and implication chaining to derive the desired conclusion.
This particular chained deduction is saying: factorial zero equals one by definition of the factorial function. Further, one equals factorial one by definition of the factorial function. The factorial that factorial zero equals factorial one implies that factorial zero is less than or equal to factorial one by definition of the less-than-or-equal-to relation (which is defined in the nat-less file we loaded in from Athena's standard library at the top of our factorial file).
The second base case is similarly proved with chaining, though we have to take a few more steps.
We know that the factorial of 2 must be greater than the factorial of 1, since our axioms tell us that factorial 2 would be equal to 2 * factorial 1 which is 2. Since one is less than two, and since the factorial of one is one and the factorial of two is two, it trivially follows that factorial one is less than factorial two. Finally, we know that for any two numbers $x$ and $y$, if $x \lt y$ then we can confidently claim that $x \le y$ as well.
This is exactly what we will formalize using the same chain-> method. We'll also add a definition of two for convenience at the top of the Factorial module: define two := (S one).
(S zero) => (!chain-> [
(factorial two)
= (two * (factorial one)) [fact-def]
= (two * one)
= two
==> (one < two)
==> (factorial one < factorial two)
==> (factorial one <= factorial two) [lte-def]
])
Notice that not every step in the proof requires that we provide explicit justification. Athena is pretty effective at identifying justifications that already exist in the assumption base. Proof-via-chaining can be used for far more sophisticated deductions and provides mechanisms for a variety of advanced justifications. In a future tutorial, we will discuss chaining in greater depth, including such topics as when explicit justifiers are required, what kinds of justifiers are available for use, and how to order the steps in a proof chain.
With the second base case successfully derived, the entire factorial file should look like this:
load "nat-less"
(transform-output eval [nat->int])
module Factorial {
declare factorial: [N] -> N [factorial [int->nat]]
define [< * one zero <=] := [N.< N.* (S N.zero) N.zero N.<= ]
define [n m k] := [?n:N ?m:N ?k:N]
define two := (S one)
assert* fact-def := [
(factorial zero = one)
(factorial one = one)
(factorial S n = S n * factorial n)
]
(eval factorial 5) # 120
define [lte-def] := N.Less=.<=-def
define theorem := (forall n . factorial n N.<= factorial S n)
by-induction theorem {
zero => (!chain-> [
(factorial zero)
= one [fact-def]
= (factorial one) [fact-def]
==> ((factorial zero) <= (factorial one)) [lte-def]
])
| (S zero) => (!chain-> [
(factorial two)
= (two * (factorial one)) [fact-def]
= (two * one)
= two
==> (one < two)
==> (factorial one < factorial two)
==> (factorial one <= factorial two) [lte-def]
])
| (n as (S m)) => (!force (factorial S m <= factorial S S m))
}
}
Proving the Inductive Step
Now let's move onto the inductive step.
Remember that the inductive step of a proof by induction assumes the inductive hypothesis and then derives the desired conclusion.
So what is the inductive hypothesis? For any property we are proving with induction, $P(n)$, our inductive hypothesis states that $P(n - 1)$ holds.
In our case, we are attempting to prove that factorial S m <= factorial S S m. Our inductive hypothesis is therefore factorial m <= factorial S m. Athena automatically inserts the hypothesis into the inductive step's assumption base.
This makes it very easy to verify that the hypothesis is indeed what we believe it to be. We can do this in Athena by using the claim method, which derives a sentence if and only if that sentence is already in the assumption base.
(n as (S m)) => conclude goal := (factorial S m <= factorial S S m)
let {
ih := (factorial m <= factorial S m);
_ := (!claim ih)
}
(!force goal)
If we add the let block between the definition of the goal and the call to force and run Athena, we should see a successful output. This indicates that the inductive hypothesis we wrote is in the assumption base after all (if you need more convincing, try changing the inductive hypothesis sentence around and re-running Athena).
To prove the inductive step, we will utilize a powerful proof technique: reductio ad absurdum! This is otherwise known as proof by contradiction.
Luckily, there's a method for that.
Athena's proof-by-contradiction method takes two arguments: a sentence we wish to prove (the goal) and a deduction of the form: ~ goal ==> false. How do we derive false? Well, we can use Athena's absurd method which takes a sentence and its negation and - if both are in the assumption base (i.e., both a sentence and its negation have already been established as proven theorems or axioms) - inserts false into the assumption base.
Let's sketch this out:
conclude goal := (factorial S m <= factorial S S m)
(!by-contradiction goal
assume contra := (~ goal)
(!force false)
)
Now we just have to replace that call to force with a proof that the negation of the goal leads to a contradiction.
If we assume ~ goal, we are assuming that factorial S m <= factorial S S m is not true. I hope we can all agree, as well, that if not (x <= y) then y < x. A proof of this property can be found in the nat-less file we imported in the beginning. Specifically, it is defined in a module contained within the N module called Less= and the name of the property is trichotomy1. So, we can use that property to derive the sentence factorial S S m < factorial S m:
(!by-contradiction goal
assume contra := (~ goal)
let {
ssm_lt_sm := (!chain-> [
contra
==> (factorial S S m < factorial S m) [N.Less=.trichotomy1]
==> (((S S m) * factorial S m) < factorial S m ) [fact-def]
])
}
Notice that the conclusion of this proof chain is S S m * factorial S m < factorial S m. The reason we factor out the S S m and then define the left hand of the inequality with multiplication is because it makes deriving the final contradiction easier. Essentially, we know that for any number n greater than or equal to 1, n * m < m is definitely not true: the product of n and m is equal to m if n is 1, and is greater than m otherwise. We can formalize this property: forall n m . ~ (S n * m < m). Let's use this factorial to derive the negation of the sentence ssm_lt_sm which we just proved. We will add it as a second derivation within the let block. Remember to add a semiconol after the first derivation (in let blocks, each arm except the last one must be terminated with a semicolon)
let {
ssm_lt_sm :=
(!chain-> [
contra
==> (factorial S S m < factorial S m) [N.Less=.trichotomy1]
==> (((S S m) * factorial S m) < factorial S m ) [fact-def]
]);
neg_ssm_lt_sm := (!chain-> [
ssm_lt_sm
==> (~ (S S m) * (factorial S m) < factorial S m) [(forall ?x ?y . ~ (S ?x * ?y < ?y))]
])
}
The evaluation of this proof does not succeed: Athena tells us that going from ssm_lt_sm to its negation is unsuccessful. The reason for this is that the sentence we use as justification is not in the assumption base. Having said that, it does follow from the axioms & theorems proven about multiplication in the standard library.
It looks like we need to prove this lemma before we can make further progress with our proof of the induction step. Instead of proving it ourselves, let's just define it above our entire inductive proof and ask Athena to prove it for us. This is far more convenient than taking the time to prove a property that we only need as a justifier in the proof we actually care about.
define num_times_x_gt_x := (forall n m . ~ (S n * m < m))
(!prove num_times_x_gt_x (ab))
Athena's prove method takes two arguments: a sentence we wish to prove and a list of assumptions that can be used in the proof. We pass the entire contents of the assumption base, since it contains all the axioms about N. The procedure ab in Athena returns all theorems and axioms in the assumption base at the location where it is called.
We can also refactor the second chaining proof to look a bit nicer:
neg_ssm_lt_sm := (!chain-> [
ssm_lt_sm
==> (~ ssm_lt_sm) [num_times_x_gt_x]
])
With ssm_lt_sm and its negation both derived, we can use absurd to complete this proof: (!absurd neg_ssm_lt_sm ssm_lt_sm).
The final contents of the Factorial module should look like this:
load "nat-less"
(transform-output eval [nat->int])
module Factorial {
declare factorial: [N] -> N [factorial [int->nat]]
define [< * one zero <=] := [N.< N.* (S N.zero) N.zero N.<= ]
define [n m k] := [?n:N ?m:N ?k:N]
define two := (S one)
assert* fact-def := [
(factorial zero = one)
(factorial one = one)
(factorial S n = S n * factorial n)
]
(eval factorial 5) # 120
define num_times_x_gt_x := (forall n m . ~ (S n * m < m))
(!prove num_times_x_gt_x (ab))
define [lte-def] := N.Less=.<=-def
define theorem := (forall n . factorial n N.<= factorial S n)
by-induction theorem {
zero => (!chain-> [
(factorial zero)
= one [fact-def]
= (factorial one) [fact-def]
==> ((factorial zero) <= (factorial one)) [lte-def]
])
| (S zero) => (!chain-> [
(factorial two)
= (two * (factorial one)) [fact-def]
= (two * one)
= two
==> (one < two)
==> (factorial one < factorial two)
==> (factorial one <= factorial two) [lte-def]
])
| (n as (S m)) => conclude goal := (factorial S m <= factorial S S m)
let {
ih := (factorial m <= factorial S m);
_ := (!claim ih)
}
(!by-contradiction goal
assume contra := (~ goal)
let {
ssm_lt_sm := (!chain-> [
contra
==> (factorial S S m < factorial S m) [N.Less=.trichotomy1]
==> (((S S m) * factorial S m) < factorial S m ) [fact-def]
]);
neg_ssm_lt_sm := (!chain-> [
ssm_lt_sm
==> (~ ssm_lt_sm) [num_times_x_gt_x]
])
}
(!absurd neg_ssm_lt_sm ssm_lt_sm)
)
}
}
Thus, our proof is complete!
If you encountered any issues while following along, or if you've noticed a mistake, please feel free to open an issue on the GitHub repository associated with this tutorial.
Alternative solutions are also welcome, so feel free to show off your creativity by forking the repo & adding your solution to the mix.
Until next time!
QED