>> Hello, everyone. Welcome to this presentation.
My name is Antoine Defourne.
Today, we'll present a joint work with
Petar Vukmirovic about bringing
higher-order automations to TLAPS.
Let's start with some context.
I want to make clear that I will not talk
about TLC and others in this talk.
I will only be concerned with TLAPS and proofs,
and also we ignore [inaudible] problems
because there are not so much used in practice for TLAPS.
So problem I'm concerned with is a cluster
of theorems for TLAPS which are not
handled very well currently by the backend solvers
because they are more second-order problems
which cannot be handled by first-order backends.
So I want to extend TLAPS with a new higher order backend solver,
and for this I chose Zipperposition.
So let me explain quickly how TLAPS
works for those of you who never used TLAPS.
So the two disabled to pass a module of
theorems and proof scripts, and from
this pulse generator number of
proof obligations which correspond to proof steps in the script.
Each proof obligation is then sent to a backend solver,
to all of the backend solvers of TLAPS
after been encoded in the respective input languages.
Whenever a solver answer that's the proof of obligation is valid,
it is trusted by TLAPS,
ends with proof of obligation is considered valid.
So there are several backends available: Isabelle, Zenon,
a few SMT solvers and PTL for the temporal reasoning parts.
To illustrate my problem,
let's start on the formula, a definition.
So I want to define the sum operator in TLAPS,
and I want to do it by recursion.
So in this expression,
there are two parameters of natural numbers are n, n of series s.
For n, I can just represent it using the natural number of TLA+,
but for s, I have a choice.
I can use a TLA+ function or an operator.
So I chose of an operator for this,
for the sake of illustration,
because that will make the sum operator
parameterized by another operator, so it will be second-order.
Here's a definition.
There is a difficulty with
this definition because TLA+ doesn't allow
to define recursive operators, only recursive functions.
So this is why I have to do it in two steps like this.
Now, another issue with this definition is that when a definition,
a recursive function, is defined like this,
it's actually a choose expression behind the scenes.
So sumRec must be read as some function f,
but some f, sorry, such that f is a function of that,
that matches the recursive definition if it exists.
If such function doesn't exist,
then the deficient can't be used.
So the user must prove by
itself that such a function exists
before the deficient can be used for anything.
Fortunately, the standard distribution of
TLAPS provide the module to do just that.
If we follow a simple pattern of theorems,
we can recover the basic facts and
basic properties of Sum quickly.
So it works like this:
First, I have to prove that you'll have
SumDefConclusion which I won't explain,
but it states in some way that
the function f that matches the recursive definition does exist.
You see here if it's a theorem
has to be prioritized by an operator S.
This is the Assume New S part.
I'm skipping the proof,
but just know that this is solved by TLAPS without problem.
Now, the theorem I'm interested in is SumDef.
SumDef states that the sum operator for argument n
and S is defined by the recursive definition that I intended.
So this is a statement that I would like to
use instead of the actual definition of operator
whenever I need to have to use the Sum definition.
In principle, SumDef is just a reformulation of SumDefConclusion.
So its proof is just one line here.
It works by invoking SumDefConclusion
as a remark and expand some definition.
Now, unfortunately, this proof phase
TLAPS is not able to proof this one.
To understand why, let's look at SumDefConclusion.
So I already pointed out that SumDefConclusion
is parameterized by an operator S.
In logical terms, that means
SumDefConclusion is the statement that is
quantified over on operator S.
For SumDef, this quantified lemma
has to be instantiated with an operator S.
So we can see that it's not first-order instantiation here,
it's second-order instantiation.
Where most of the backend solvers of TLAPS are able to to
handle first-order instantiation because
they are first-order logic.
Isabelle is the only backend that can do that.
So that makes the proof very fragile.
Because Isabelle is not able to prove this one,
TLAPS cannot do anything more as a proof phase.
We can state in general what
problems are not going to be handled well by TLAPS.
Every time a lemma that is parametized
by an operator is invoked in
a proof and lemma has to be used,
so to be instantiated with an operator,
this is a second-order problem,
so we can't use the first-order back-end, at all, for those.
As a special case,
we can see primitive constructs
like set comprehension for example,
but also, choose expression functions and so on.
Has second-order constructs with
not axios but axiom schemas parameterized by an operator,
predicate P in that case.
Those axiom schemas needs to be instantiated for the encoding.
Of course, these are common constructs.
For the first-order encodings,
we have to know them in some way.
Currently, this is done by
eliminating those problematic constructs.
So here, you can see one example,
just to give you the ID.
If I want to eliminate a set comprehension for these predicates,
I can start by every word and writing
it as a second-order application.
With one argument being the base set,
but the other one will be the predicates, so predicate P.
Then what I need to do is to replace
this application by another application when you declare operator,
which is specialized for this predicate.
I also need to provide the axiom,
the instance of the axiom schema
for set comprehension for that predicate, and that's it.
For our complications,
when some local variables are involved, see that example.
We need to make some arrangement.
Provide C as a parameter,
but if this is something that we are able to
do in cases such as this one,
because we know the axiom schemas behind the construct.
Now, if I don't want to do
this rather technical elimination procedure,
I can just encode the problem into
higher order logic and send the higher-order problem to a solver,
which is able to endure higher-order logic.
We chose Zipperposition to make this experiment.
Zipperposition is a first-order superposition solver
which was extended to higher order logic recently.
To give you more context,
this is part of a project called Matryoshka,
and supervised by Jasmin Blanchette,
which is about extending solver from first-order to
higher order logic in ways that preserve the good properties.
Zipperposition just won the
CASC competition last year in the THF division.
THF is a component of the HTTP standard language for problems,
and it covers higher-order logic.
We did the implementation,
we implemented it at the module,
so an export from TLA plus to THF.
The important aspect of this is
that we don't need to eliminate the higher-order features anymore.
We can translate the problem more directly than before.
Using Zipperposition, we were able to
solve the sum examples rather easily.
Now, there are still some work to do.
Our priority right now is to make
this new Zipperposition back-end
as efficient as the first-order back-ends of TLA plus.
The first-order of encodings are well optimized by now,
especially the [inaudible] encoding.
We could test with one Sum example,
but to evaluate it at a larger base of examples,
we still have work to do.
The next step would be to mix
higher-order reasoning with theories, especially, arithmetic.
Here, the problem is that Zipperposition
is extended to higher order logic,
but this extension is not compatible
With special of reasoning like arithmetic.
We cannot use the backend for application
that mix higher order with arithmetic for example.
We need to find a solution for that yet.
Then the next step,
maybe more longer term objective,
would be to attempt
an encoding based on sets as predicates principle.
The idea for this encoding is that we can encode
sets as predicates which are satisfied by
elements of that set, and those elements only.
Set membership is encoded as
a functional application in higher order logic very simply.
Here, you can find some examples
very easy to understand how this works.
The interest of that encoding will be that we don't need to declare
many new operators and axioms in
the resulting file because
each sets can just be represented by the lambda term.
That is all. Okay. This is the end of the talk.
Thank you for your attention.
If you have any question,
I'm ready to answer them now.