Compute with functions
In the last chapter, we’ve started working with Alt-Ergo.
We’ve learned how to state problems through symbols, axioms and goals.
We’ve expressed complex logical sentences through logical connectives and quantifiers.
We’ve started factoring our code with predicates: functions with
boolcodomain.
In this chapter, we’ll write more general functions. This will allow us to do several things.
Reason about abstract functions with any codomain.
Express explicit functions to factor our code.
Reason efficiently about associative and commutative symbols, thanks to Alt-Ergo built-in support for them.
This will be applied more generally in the next chapter, in which we’ll look at strategies to prove imperative programs.
Uninterpreted functions
Define abstract functions
In the previous chapter, we’ve introduced new “uninterpreted symbols”: typed variables which make the building blocks of our logical sentences.
We’ve introduced booleans (bool), integers (int), …
Similarly, we could have added real numbers (real), or our own types (we’ll discover how to do that in a following chapter).
At some point, we’ve also introduced the symbol of an uninterpreted function, from booleans to booleans. Have a look back at this example.
Example
logic f: bool -> bool
predicate f_is_constant =
forall x:bool. f(x) = x
predicate f_has_fixpoint =
exists x:bool. f(x) = x
predicate f_is_idempotent =
forall x:bool. f(f(x)) = f(x)
predicate f_is_involutive =
forall x:bool. f(f(x)) = x
goal g1:
f_is_constant ->
f_has_fixpoint and f_is_idempotent and f_is_involutive
goal g2:
f_is_involutive and f_has_fixpoint ->
f_is_constant
goal g3:
f_has_fixpoint ->
f_is_idempotent
More generally, it is possible to introduce uninterpreted functions from any basic type to any other, and they may have several arguments.
Here are a few examples.
Examples
logic f: int -> int
predicate f_even =
forall x:int. f(-x) = f(x)
predicate f_odd =
forall x:int. f(-x) = -f(x)
predicate f_null =
forall x:int. f(x) = 0
goal g1:
f_odd -> f(0) = 0
goal g2:
f_even and f_odd -> f_null
logic f: real, real -> real
axiom f_homogeneous:
forall x,y,lambda:real. lambda*f(x,y) = f(lambda*x,lambda*y)
goal g: 2.*f(2.,4.5) = f(4.,9.)
Notice the syntax: undefined functions can be introduced via the logic keyword, just like any other uninterpreted symbol.
Then only thing that changes is that we use a function type, written with a right arrow ->, the type of arguments being on the left (multiple arguments are separated by a comma ,), the type of the result being on the right.
Note that higher-order functions are not supported in Alt-Ergo’s native language. Functions cannot be used as arguments or output of other functions, and cannot be quantified upon.
In our examples, we’ve defined rather general properties on our functions. Obviously, you could use more axioms and hypotheses to define them completely.
Example
logic gate: bool, bool -> bool
axiom gTT: gate(true, true) = false
axiom gTF: gate(true, false) = true
axiom gFT: gate(false, true) = false
axiom gFF: gate(false, false) = true
goal gate_not_associative:
not(forall x,y,z:bool. gate(x,gate(y,z)) = gate(gate(x,y),z))
To end this section, we’ll try to define a more interesting function in an exercise about the Collatz conjecture (note that Alt-Ergo isn’t specialized in non-linear arithmetic – the goal of this exercise is solely to train yourself at writing properties about functions in Alt-Ergo). We’ll go back at this exercise in the next section.
Work with integers
Note
In order to state everything we need, we’re going to use more operators on integers. Here is a complete list.
Symbol |
Type |
Interpretation |
|---|---|---|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Remember than comparisons operators can be chained to write things such as 1 <= x <=4 ( \(x\) is in the closed interval \([1,4]\)).
Symbol |
Type |
Interpretation |
|---|---|---|
|
|
Addition |
|
|
Subtraction |
|
|
Unary negative |
|
|
Multiplication |
|
|
Quotient |
|
|
Remainder modulo |
Exercise
Before getting to Collatz conjecture, have a go with integer operators.
Complete the following code. Goals should prove what is described by their name.
predicate is_even(x:int) =
(* YOUR CODE HERE *)
predicate is_odd(x:int) =
(* YOUR CODE HERE *)
goal sum_of_evens_is_even:
(** YOUR CODE HERE
*)
goal sum_of_odds_is_even:
(** YOUR CODE HERE
*)
goal if_sum_is_odd__then_only_one_term_is_odd:
forall x,y:int. is_odd(x+y) ->
(* YOUR CODE HERE *)
goal if_product_is_odd__then_both_terms_are_odd:
(** YOUR CODE HERE
*)
goal double_plus_one_is_odd:
(** YOUR CODE HERE
*)
Solution
predicate is_even(x:int) =
x%2 = 0
predicate is_odd(x:int) =
x%2 = 1
goal sum_of_evens_is_even:
forall x,y:int. is_even(x) -> is_even(y) ->
is_even(x+y)
goal sum_of_odds_is_even:
forall x,y:int. is_odd(x) -> is_odd(y) ->
is_even(x+y)
goal if_sum_is_odd__then_only_one_term_is_odd:
forall x,y:int. is_odd(x+y) ->
(is_even(x) and is_odd(y)) or (is_odd(x) and is_even(y))
goal if_product_is_odd__then_both_terms_are_odd:
forall x,y:int. is_odd(x*y) ->
is_odd(x) and is_odd(y)
goal double_plus_one_is_odd:
forall x:int.
is_odd(2*x+1)
Exercise: Collatz conjecture
Now that you’ve worked a bit with integer properties, it’s time to work on Collatz conjecture. (Disclaimer: you’re only going to check that it holds for very small values…)
Exercise
Collatz conjecture is an open problem in mathematics which concerns a sequence defined by recursion as follow.
Let \(f:\mathbb{N}\to\mathbb{N}\) be the function such that \(f(n) = \frac{n}{2}\) when \(n\) is even and \(f(n) = 3*n+1\) when \(n\) is odd.
Let \(u:\mathbb{N}\to\mathbb{N}\) be a sequence such that for all \(n>0\), \(u(n) = f(u(n-1))\).
Collatz conjecture then states that no matter the initial value \(u(0)\), the sequence will reach the value \(1\).
In this exercise, we’re going to check that this property holds for a few initial values.
First, define the function \(f\) with logic and axiom.
Your symbol should correspond to the definition, and all goals should be Valid.
predicate is_even(x:int) = (x%2 = 0)
predicate is_odd(x:int) = (x%2 = 1)
(** YOUR CODE HERE
*)
goal g1: f(1) = 4
goal g2: f(2) = 1
goal g3: f(5) = 16
goal g4: f(8) = 4
Solution
You can create two axioms to handle both cases.
predicate is_even(x:int) = (x%2 = 0)
predicate is_odd(x:int) = (x%2 = 1)
logic f: int -> int
axiom f_even:
forall x:int. is_even(x) -> f(x) = x/2
axiom f_odd:
forall x:int. is_odd(x) -> f(x) = 3*x + 1
goal g1: f(1) = 4
goal g2: f(2) = 1
goal g3: f(5) = 16
goal g4: f(8) = 4
You now want to define the sequence \(u\). Complete the axiom u_step, which defines \(u\) by recursion.
predicate is_even(x:int) = (x%2 = 0)
predicate is_odd (x:int) = (x%2 = 1)
(** COPY HERE THE DEFINITION OF f FROM THE PREVIOUS EXERCISE
*)
logic u:int -> int
axiom u_step:
(** YOUR CODE HERE
*)
predicate collatz_holds_for(x:int) =
u(0)=x -> exists n:int. u(n)=1
goal g0: u(0) = 2 -> u(1) = 1
goal g1: u(0) = 3 -> u(2) = 5
goal g2: collatz_holds_for(2)
goal g3: collatz_holds_for(4)
Solution
There was one pitfall to avoid: the value \(u(n)\) is only defined by recursion through \(f\) when \(n>0\) !
(* Step function *)
predicate is_even(x:int) = (x%2 = 0)
predicate is_odd(x:int) = (x%2 = 1)
logic f:int -> int
axiom f_even:
forall x:int. is_even(x) -> f(x) = x/2
axiom f_odd:
forall x:int. is_odd(x) -> f(x) = 3*x + 1
(* Sequence defined by recursion *)
logic u:int -> int
axiom u_step:
forall n:int. n>0 ->
u(n) = f(u(n-1))
predicate collatz_holds_for(x:int) =
u(0)=x -> exists n:int. u(n)=1
goal g0: u(0) = 2 -> u(1) = 1
goal g1: u(0) = 3 -> u(2) = 5
goal g2: collatz_holds_for(2)
goal g3: collatz_holds_for(4)
You may notice that this code is very slow. While this is due in a large part to Alt-Ergo running with its in-browser version, there is another issue: defining functions with multiple axioms isn’t very direct, and creates a lot of work.
In the next section, we’re going to learn how to define explicit functions more directly.
Explicit functions
The function keyword
In the previous section (and in particular in the Collatz exercise), we’ve reasoned about functions in the following way.
First, introduce an abstract symbol to represent this function.
Then, add axioms to refine and restrict the definition of the function.
Finally, let Alt-Ergo prove properties and find out by itself which axioms should be used in which case.
This is great to prove general properties. However, for functions which we intend to define completely, this is both slow and hard to read.
A more direct method is to define functions explicitely with keyword function.
This allows Alt-Ergo to compute the results directly, rather than looking up multiple axioms to see what should be done.
We’ve actually already defined a specific kind of explicit function in the previous chapter, by using predicate !
Just like predicate, function can also be used to factor code, make it easier to read and to produce.
Example
predicate is_even(x:int) =
x%2 = 0
function is_even'(x:int):bool =
x%2 = 0
goal equiv_even_even':
forall x:int. is_even(x) = is_even'(x)
function mean(x:real, y:real):real =
(x+y)/2.
function square_dist(x1:real, y1:real, x2:real, y2:real):real =
(x1-x2)*(x1-x2) + (y1-y2)*(y1-y2)
Notice the syntax: function works just like predicate.
The only difference is that for function, we need to explicitely declare an output type (whereas for predicate, it was implicit and always bool.
Remember to use = before the definition of functions and predicates, unlike : which is used for abstract symbols (logic), axiom and goal.
Conditional expressions
In order to write more interesting functions, we need more vocabulary.
A simple and useful construct is if [...] then [...] else [...].
Examples
function abs(x:int):int =
if x>= 0 then x else -x
function activation(x:int):int =
if -1 <= x <= 1 then
x
else if x < -1 then
-1
else
1
goal commute:
forall x:int. abs(activation(x)) = activation(abs(x))
goal activation_idempotent:
forall x:int. activation(activation(x)) = activation(x)
function int_of_bit(b:bool):int =
if b then 1 else 0
(* Nybbles are half-octets *)
function int_of_nybble(b3:bool,b2:bool,b1:bool,b0:bool):int =
8*int_of_bit(b3) + 4*int_of_bit(b2) + 2*int_of_bit(b1) + int_of_bit(b0)
goal range:
forall b3,b2,b1,b0:bool. 0 <= int_of_nybble(b3,b2,b1,b0) < 16
Notice the syntax: you can simply write if <condition> then <expr_1> else <expr_2>, where <condition> has type <bool> and <expr_1> and <expr_2> have the same type.
Look back at the solution from the Collatz exercise.
(* Step function *)
predicate is_even(x:int) = (x%2 = 0)
predicate is_odd(x:int) = (x%2 = 1)
logic f:int -> int
axiom f_even:
forall x:int. is_even(x) -> f(x) = x/2
axiom f_odd:
forall x:int. is_odd(x) -> f(x) = 3*x + 1
(* Sequence defined by recursion *)
logic u:int -> int
axiom u_step:
forall n:int. n>0 ->
u(n) = f(u(n-1))
predicate collatz_holds_for(x:int) =
u(0)=x -> exists n:int. u(n)=1
goal g0: u(0) = 2 -> u(1) = 1
goal g1: u(0) = 3 -> u(2) = 5
goal g2: collatz_holds_for(2)
goal g3: collatz_holds_for(4)
With explicit functions, we can now write a much simpler definition !
Try both solutions, and check the number of steps performed by Alt-Ergo.
(* Step function *)
predicate is_even(x:int) = (x%2 = 0)
function f(x:int):int =
if is_even(x) then
x/2
else
3*x + 1
(* Sequence defined by recursion *)
logic u0:int
function u(n:int):int =
if n>0 then
f(u(n-1))
else
u0
predicate collatz_holds_for(x:int) =
u0 = x -> exists n:int. u(n)=1
goal g0: u0 = 2 -> u(1) = 1
goal g1: u0 = 3 -> u(2) = 5
goal g2: collatz_holds_for(2)
goal g3: collatz_holds_for(4)
goal g4: collatz_holds_for(5)
Explicit functions are a great help for g0 and g1, which only use computation.
However, they actually make Alt-Ergo’s job more difficult in the case of g2, g3 and g4, which include an existential quantifier.
Our code could still be improved. If we allow ourselves to modify our goal for an equivalent one, we could write the following program, which executes faster.
Let’s remove the existential quantifier, which creates a lot of work for Alt-Ergo: we will direct the search by using a recursive predicate. This hides the implementation of \(u\) altogether.
(* Step function *)
predicate is_even(x:int) = (x%2 = 0)
function f(x:int):int =
if is_even(x) then
x/2
else
3*x + 1
predicate collatz_holds_for(x:int) =
(x = 1) or collatz_holds_for(f(x))
goal g2: collatz_holds_for(2)
goal g3: collatz_holds_for(4)
goal g4: collatz_holds_for(5)
Associative and commutative symbols
We’ll end this chapter with a note on one of Alt-Ergo’s specialties: reasoning about associative and commutative (AC) symbols.
Imagine that you’re working on the following example, with an abstract operator which you know is associative and commutative.
logic op: int, int -> int
axiom op_commutative :
forall x,y:int. op(x,y) = op(y,x)
axiom op_associative :
forall x,y,z:int. op(x,op(y,z)) = op(op(x,y),z)
goal simplification_correct_0:
forall x,y:int.
op(op(x,y),op(y,x)) = op(x,op(x,op(y,y)))
goal simplification_correct_1:
forall x,y,z:int.
op(op(x,y),op(y,op(op(z,op(x,x)),z))) = op(x,op(x,op(x,op(y,op(y,op(z,z))))))
You can notice that Alt-Ergo is quite slow.
Indeed, it needs to instantiate the axioms op_commutative and op_associative every time it uses them !
Imagine writing a proof where you would write “by commutativity of op” and “by associativity of op” each and every single time you use this property…
Thankfully, Alt-Ergo has built-in reasoning for AC symbols, as they appear quite often in useful problems.
In order to tell Alt-Ergo that a symbol is associative and commutative, simply add the modifier ac between logic and the name of the operator when you define it. (No need to add specific axioms for commutativity and associativity).
Check the following example: proofs happen much quicker.
logic ac op: int, int -> int
goal simplification_correct_0:
forall x,y:int.
op(op(x,y),op(y,x)) = op(x,op(x,op(y,y)))
goal simplification_correct_1:
forall x,y,z:int.
op(op(x,y),op(y,op(op(z,op(x,x)),z))) = op(x,op(x,op(x,op(y,op(y,op(z,z))))))
You can also prove much more things. (Try removing ac and adding explicit axioms: you’ll probably get a timeout).
logic ac op: int, int -> int
goal simplification_correct_0:
forall x,y:int.
op(op(x,y),op(y,x)) = op(x,op(x,op(y,y)))
goal simplification_correct_1:
forall x,y,z:int.
op(op(x,y),op(y,op(op(z,op(x,x)),z))) = op(x,op(x,op(x,op(y,op(y,op(z,z))))))
function op_pow(x:int,n:int):int =
if n>1 then
op(x,op_pow(x,n-1))
else
x
goal simplification_correct_2:
forall x,y,z:int.
op(op(x,y),op(y,op(op(z,op(x,x)),z))) = op(op_pow(x,3),op(op_pow(y,2),op_pow(z,2)))
goal simplification_correct_3:
forall x,y:int. forall n,m:int. n>1 -> m>1 ->
op(x,op(op_pow(y,m),op(op_pow(x,n),y))) = op(op_pow(x,n+1),op_pow(y,m+1))