Higher-order Automation In TLAPS - Antoine Defourné and Petar Vukmirovic

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.

01:06 - 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.

02:10 - 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.

03:01 - 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.

03:53 - 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.

04:53 - 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.

05:46 - 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.

07:12 - 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.

08:25 - 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.

09:02 - 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.

10:13 - 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.

11:01 - 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.

11:52 - 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.

12:46 - 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.

14:02 - If you have any question, I’m ready to answer them now. .