Congruence Closure in Intensional Type Theory
Congruence closure procedures are used extensively in automated reasoning and are a core component of most satisfiability modulo theories solvers. However, no known congruence closure algorithms can support any of the expressive logics based on intensiona
- PDF / 811,416 Bytes
- 17 Pages / 439.37 x 666.142 pts Page_size
- 83 Downloads / 194 Views
Stanford University, Stanford, USA [email protected] Microsoft Research, Redmond, USA [email protected]
Abstract. Congruence closure procedures are used extensively in automated reasoning and are a core component of most satisfiability modulo theories solvers. However, no known congruence closure algorithms can support any of the expressive logics based on intensional type theory (ITT), which form the basis of many interactive theorem provers. The main source of expressiveness in these logics is dependent types, and yet existing congruence closure procedures found in interactive theorem provers based on ITT do not handle dependent types at all and only work on the simply-typed subsets of the logics. Here we present an efficient and proof-producing congruence closure procedure that applies to every function in ITT no matter how many dependencies exist among its arguments, and that only relies on the commonly assumed uniqueness of identity proofs axiom. We demonstrate its usefulness by solving interesting verification problems involving functions with dependent types.
1
Introduction
Congruence closure procedures are used extensively in automated reasoning, since almost all proofs in both program verification and formalized mathematics require reasoning about equalities [23]. The algorithm constitutes a fundamental component of most satisfiability modulo theories (SMT) solvers [4,20]; it is often distinguished as the “core theory solver”, and is responsible for communicating literal assignments to the underlying SAT solver and equalities to the other “satellite solvers” [10,20]. However, no known congruence closure algorithms can support any of the expressive logics based on intensional type theory (ITT). Yet despite the lack of an algorithm for congruence closure, the benefits that ITTs confer in terms of expressiveness, elegance, and trustworthiness have proved substantial enough that different flavors of ITT form the basis of many interactive theorem provers, such as Coq [8], Lean [21], and Matita [2], and also several emerging programming languages, such as Agda [5], Epigram [16], and Idris [6]. Many of the most striking successes in both certified programming and formalized mathematics have been in variants of ITT, such as the development of a fully-certified compiler for most of the C language [14] and the formalization of the odd-order theorem [11]. There are currently two main workarounds for the lack of a congruence closure algorithm for ITT, and for the lack of robust theorem proving tools for ITT c Springer International Publishing Switzerland 2016 N. Olivetti and A. Tiwari (Eds.): IJCAR 2016, LNAI 9706, pp. 99–115, 2016. DOI: 10.1007/978-3-319-40229-1 8
100
D. Selsam and L. de Moura
more generally. One option is to rely much more on manual proving. Although many impressive projects have been formalized with little to no automation, this approach is not very attractive since the cost of manual proving can be tremendous. We believe that as long as extensive manual proving is a central part of writing
Data Loading...
