Domain-Specific Language to Encode Induction Heuristics

TL;DR

This paper introduces LiFtEr, a domain-specific language that enables expert Isabelle users to encode and systematically transfer their induction heuristics to less experienced users, improving inductive theorem proving.

Contribution

The paper presents LiFtEr, a novel language for encoding induction heuristics, facilitating systematic knowledge transfer among Isabelle users.

Findings

LiFtEr successfully encodes induction heuristics.

The interpreter verifies heuristic application in proofs.

Enhances knowledge sharing in inductive theorem proving.

Abstract

Proof assistants, such as Isabelle/HOL, offer tools to facilitate inductive theorem proving. Isabelle experts know how to use these tools effectively; however, they did not have a systematic way to encode their expertise. To address this problem, we present our domain-specific language, LiFtEr. LiFtEr allows experienced Isabelle users to encode their induction heuristics in a style independent of any problem domain. LiFtEr's interpreter mechanically checks if a given application of induction tool matches the heuristics specified by experienced users, thus systematically transferring experienced users' expertise to new Isabelle users.

Full text

††journal: PACMPL††journalvolume: 1††journalnumber: CONF††article: 1††journalyear: 2018††publicationmonth: 1††copyright: none

1. Introduction

A noteworthy approach for proof automation in proof assistants (PAs) is the so-called hammer tools (Blanchette et al., 2016). For example, sledgehammer (Blanchette et al., 2011) exports proof goals in Isabelle/HOL (Nipkow et al., 2002) to various external automated theorem provers (ATPs) to exploit the state-of-the-art backend provers; however, the discrepancies between the polymorphic higher-order logic of Isabelle/HOL and the monomorphic first-order logic of the backend provers severely impair sledgehammer’s performance when it comes to inductive theorem proving (ITP) 111Not to be confused with interactive theorem proving, which is a synonym of proof assistant (PA)..

This is unfortunate for two reasons. First, many Isabelle users chose Isabelle/HOL precisely because its higher-order logic is expressive enough to specify mathematical objects and procedures involving recursion. Second, induction lies at the heart of programming language semantics. For instance, induction is often necessary for reasoning about recursive data-structures, such as lists and trees, computer programs containing recursion and iteration (Bundy, 2001).

Ironically, the most well-known approach, called waterfall (Moore, 1973), for ITP was invented for a first-order logic, which cannot handle induction without jeopardizing the soundness by introducing induction axioms. Jiang et al. took a similar approach and ran multiple waterfalls (Jiang et al., 2018) to automate ITP in HOL light (Harrison, 1996). However, when deciding induction variables, they naively picked the first free variable with recursive type and left the selection of appropriate induction variables as future work. To determine induction variables automatically, we developed a proof strategy language PSL and its default proof strategy, try_hard (Nagashima and Kumar, 2017). PSL tries to identify useful arguments for the induct method by conducting a depth-first search. However, PSL fails to identify useful arguments when it cannot finish a proof.

2. Induction in Isabelle/HOL

Isabelle offers the induct proof method 222Proof methods are the Isar syntactic layer of LCF-style tactics. to handle inductive problems. For example, consider the following reverse functions, rev and itrev, from literature (Nipkow and Klein, 2014):

primrec rev::"’a list =>’a list" where "rev [] = []" | "rev (x # xs) = rev xs @ [x]" fun itrev::"’a list =>’a list =>’a list" where "itrev [] ys = ys" | "itrev (x#xs) ys = itrev xs (x#ys)"

where # is the list constructor, and @ appends two lists into one. One can prove the equivalence of these reverse functions in multiple ways using the induct method:

lemma prf1:"itrev xs ys = rev xs @ ys" apply(induct xs arbitrary: ys) by auto lemma prf2:"itrev xs ys = rev xs @ ys" apply(induct xs ys rule:itrev.induct) by auto

prf1 applies structural induction on xs while generalizing ys before applying induction by passing ys to the arbitrary field. On the other hand, prf2 applies functional induction on itrev by passing an auxiliary lemma, itrev.induct, to the rule field.

There are other lesser-known techniques to handle difficult inductive problems using the induct method, and sometimes users have to develop useful auxiliary lemmas manually; however, for most cases the problem of how to apply induction boils down to the the following three questions:

• •

On which terms do we apply induction?

• •

Which variables do we generalize?

• •

Which rule do we use for functional induction?

Isabelle experts often apply induction heuristics to answer such questions and decide what arguments to pass to the induct method; however, they did not have a systematic way to encode such heuristics, which made it difficult for new users to learn how to apply induction effectively.

3. LiFtEr: Language to Encode Induction Heuristics

We address this problem with our domain-specific language, LiFtEr. LiFtEr allows experienced Isabelle users to encode their induction heuristics in a style independent of problem domains. LiFtEr’s interpreter mechanically checks if a given application of induction is compatible with the induction heuristics written by experienced users.

We designed LiFtEr to encode induction heuristics as assertions on invocations of the induct method in Isabelle. An assertion written in LiFtEr takes a triple of a proof goal at hand, its underlying proof state, and the arguments passed to the induct method to prove the goal. When one applies a LiFtEr assertion to an invocation of the induct method, LiFtEr’s interpreter returns a boolean value as the result of the assertion applied to the triple.

The goal of a LiFtEr programmer is to write assertions that implement reliable heuristics. A heuristic encoded as a LiFtEr assertion is reliable when it satisfies the following two properties: first, the LiFtEr interpreter is likely to evaluate the assertion to true when the arguments of the induct method are appropriate for the given proof goal. Second, the interpreter is likely to evaluate the assertion to false when the arguments are inappropriate for the goal.

4. LiFtEr through an Example

The following is an example assertion written in LiFtEr:

Some_Rule (Rule 1, True) Imply Some_Rule (Rule 1, Some_Trm (Trm 1, Some_Trm_Occ_Of (Trm_Occ 1, Trm 1, (Rule 1 Is_Rule_Of Trm_Occ 1) And Is_Recursive_Cnst (Trm_Occ 1) And (All_Ind (Trm 2, (Some_Trm_Occ_Of (Trm_Occ 2, Trm 2, Some_Numb (Numb 1, Is_Nth_Arg_Of (Trm_Occ 2, Numb 1, Trm_Occ 1) And (Trm 2 Is_Nth_Ind Numb 1)))))))));

where functions starting with the string Some are existential quantifiers, while those starting with All are universal quantifiers. Quantifiers ending with Trm describe sub-terms appearing in the proof goal at hand, whereas those ending with Trm_Occ describe sub-term occurrences of such sub-terms. It is important to distinguish terms and term occurrences because the induct method in Isabelle/HOL only allows its users to specify induction terms but it does not allow us to specify on which occurrences of such terms we intend to apply induction. Quantifiers ending with Rule describe auxiliary lemmas passed to the rule field in the induct method, while those ending with Ind describe induction terms specified in a given invocation of the induct method.

Is_Rule_Of, Is_Recursive_Cnst, Is_Nth_Ind, and Is_Nth_Arg_Of are atomic assertions. For example, Rule n Is_Rule_Of Trm_Occ m returns true if Rule n was derived by Isabelle automatically at the time of defining the term that has an occurrence, Trm_Occ m. And Trm n Is_Nth_Ind Numb m checks if Trm n is the (Numb m)th induction term in the given invocation of the induct method. Importantly, some atomic assertions check not only the syntactic structure of the given proof goal and the arguments of the induct method, but they also investigate the semantics of terms or types appearing in the goal. For example, Is_Recursive_Cnst checks if a given constant is defined recursively or not, by looking up the definition of the constant stored in the proof state. As a whole this example assertion checks if the following holds:

if there exists a rule, Rule 1, in the rule field of the induct method, then there exists a term Trm 1 with an occurrence Trm_Occ 1, such that Rule 1 is derived by Isabelle when defining Trm 1, where Trm 1 is defined recursively, and for all induction terms Trm 2, there exists an occurrence Trm_Occ 2 of Trm 2 such that, there exists a number Numb 1, such that Trm_Occ 2 is the (Numb 1)th argument of Trm_Occ 1 and that Trm 2 is the (Numb 1)th induction term passed to the induct method 333 Note that 1 in Numb 1 is merely the identifier of this variable, and the value of Numb 1 can be a number that is not $1$..

This assertion is useful when judging invocations of the induct method with an argument to the rule field. For example, LiFtEr can confirm that prf2 is promising based on this assertion because there is an argument, itrev.induct, in the rule field, where itrev is defined recursively, and the occurrence of its related term, itrev, in the proof goal takes all the induction terms, xs and ys, as its arguments in the same order.

5. Discussion and Future Work

We presented LiFtEr and its example assertion. LiFtEr is a domain-specific language in the sense that we developed LiFtEr to encode induction heuristics; however, heuristics written in LiFtEr are usually not specific to any problem domain, because LiFtEr’s language construct is not specific to any variables names, types, or constants. This absence encourages LiFtEr users to encode heuristics that are not specific to any problem domains but are applicable to many domains.

To the best of our knowledge, LiFtEr is the first domain-specific language that allows us to encode induction heuristics as programs. We released a working prototype of the LiFtEr interpreter and six example assertions at GitHub (Nagashima et al., 2019). And a more comprehensive explanation of LiFtEr’s grammar is provided in our paper draft (Nagashima, 2019). We continue writing assertions in LiFtEr and use them as a feature extractor that distills the essence of promising applications of induction from existing large proof corpora, such as the Archive of Formal Proofs (Klein et al., 2004), so that we can fully automate ITP using supervised machine learning in future.

Acknowledgements.

This work was supported by the European Regional Development Fund under the project AI & Reasoning (reg. no.CZ.02.1.01/0.0/0.0/15_003/0000466).

Reference

• (1)
• Blanchette et al. (2016)

Jasmin Blanchette, Cezary Kaliszyk, Lawrence Paulson, and Josef Urban. 2016.

Hammering towards QED.

Journal of Formalized Reasoning 9, 1 (2016), 101–148.

https://doi.org/10.6092/issn.1972-5787/4593

• Blanchette et al. (2011)

Jasmin Christian Blanchette, Sascha Böhme, and Lawrence C. Paulson. 2011.

Extending Sledgehammer with SMT Solvers. In Automated Deduction - CADE-23 - 23rd International Conference on Automated Deduction, Wroclaw, Poland, July 31 - August 5, 2011. Proceedings (Lecture Notes in Computer Science), Nikolaj Bjørner and Viorica Sofronie-Stokkermans (Eds.), Vol. 6803. Springer, 116–130.

https://doi.org/10.1007/978-3-642-22438-6

• Bundy (2001)

Alan Bundy. 2001.

The Automation of Proof by Mathematical Induction.

In Handbook of Automated Reasoning (in 2 volumes), John Alan Robinson and Andrei Voronkov (Eds.). Elsevier and MIT Press, 845–911.

• Harrison (1996)

John Harrison. 1996.

HOL Light: A Tutorial Introduction. In Formal Methods in Computer-Aided Design, First International Conference, FMCAD ’96, Palo Alto, California, USA, November 6-8, 1996, Proceedings (Lecture Notes in Computer Science), Mandayam K. Srivas and Albert John Camilleri (Eds.), Vol. 1166. Springer, 265–269.

https://doi.org/10.1007/BFb0031814

• Jiang et al. (2018)

Yaqing Jiang, Petros Papapanagiotou, and Jacques D. Fleuriot. 2018.

Machine Learning for Inductive Theorem Proving. In Artificial Intelligence and Symbolic Computation - 13th International Conference, AISC 2018, Suzhou, China, September 16-19, 2018, Proceedings (Lecture Notes in Computer Science), Jacques D. Fleuriot, Dongming Wang, and Jacques Calmet (Eds.), Vol. 11110. Springer, 87–103.

https://doi.org/10.1007/978-3-319-99957-9_6

• Klein et al. (2004)

Gerwin Klein, Tobias Nipkow, Larry Paulson, and Rene Thiemann. 2004.

.

https://www.isa-afp.org/

• Moore (1973)

J. Strother Moore. 1973.

Computational logic : structure sharing and proof of program properties.

Ph.D. Dissertation. University of Edinburgh, UK.

http://hdl.handle.net/1842/2245

• Nagashima (2019)

Yutaka Nagashima. 2019.

LiFtEr: Language to Encode Induction Heuristics for Isabelle/HOL.

arXiv:1906.08084

• Nagashima et al. (2019)

Yutaka Nagashima et al. 2019.

data61/PSL.

https://github.com/data61/PSL/releases/tag/v0.1.3-alpha

• Nagashima and Kumar (2017)

Yutaka Nagashima and Ramana Kumar. 2017.

A Proof Strategy Language and Proof Script Generation for Isabelle/HOL. In Automated Deduction - CADE 26 - 26th International Conference on Automated Deduction, Gothenburg, Sweden, August 6-11, 2017, Proceedings (Lecture Notes in Computer Science), Leonardo de Moura (Ed.), Vol. 10395. Springer, 528–545.

https://doi.org/10.1007/978-3-319-63046-5_32

• Nipkow and Klein (2014)

Tobias Nipkow and Gerwin Klein. 2014.

Concrete Semantics - With Isabelle/HOL.

Springer.

https://doi.org/10.1007/978-3-319-10542-0

• Nipkow et al. (2002)

Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. 2002.

Isabelle/HOL - a proof assistant for higher-order logic. Lecture Notes in Computer Science, Vol. 2283.

Springer.