=Paper=
{{Paper
|id=Vol-1955/staf-ds-2017-6
|storemode=property
|title=On the Foundation of Isabelle/HOL
|pdfUrl=https://ceur-ws.org/Vol-1955/staf-ds-2017-6.pdf
|volume=Vol-1955
|authors=Arve Gengelbach
}}
==On the Foundation of Isabelle/HOL==
https://ceur-ws.org/Vol-1955/staf-ds-2017-6.pdf
On the Foundation of Isabelle/HOL ?
Arve Gengelbach
arve.gengelbach@it.uu.se
Dept. of Information Technology, Uppsala University, Sweden
Abstract. Interactive theorem provers are used to allow formalisation
of mathematical proofs into theories, written in a precise language of
definitions and proofs. Such a theory is step-wise extended by constant
instance definitions and type definitions and contains proofs of theorems
that use these definitions. If at any point a theory is inconsistent, i.e. ev-
ery formula is deducible, the formalisation effort was futile. We set out to
extend the existing foundational work on the model-theoretic and proof-
theoretic foundation of such definitional theories, as used in the theorem
prover Isabelle/HOL. For this logical system we study semantics that
entail completeness and soundness, which are the properties that link
the model-theoretic and the proof-theoretic perspectives. We formalize
the obtained results in the theorem prover Isabelle/HOL to strengthen
the confidence in correctness of our work.
1 Problem
Interactive theorem provers support a user proving theorems in different log-
ics. Well-known provers are based on higher-order logic or on constructive type
theory. Especially for technical proofs, in addition to pen-and-paper proofs, the-
orem provers provide an appealing framework for formalisation. Not only is a
formalisation interesting from a theoretic point of view but it also is practi-
cally applicable: For example Isabelle allows to export code (via so called code
generators [4]) whose behaviour is proven to match the abstract-level specifi-
cation by abstract-level theorems. It has been applied for different verification
efforts, exemplarily the verification of the single processor behaviour of the seL4
microkernel [5].
All verification efforts are of little use if the theoretical foundation of the
framework is poorly understood. At its core Isabelle/HOL consists of a minimal
theory with a mechanism to extend a theory by definitions of constants and
types. These theories are called definitional theories [10]. If both the smallest
theory – called minimal theory – and the extension mechanism are properly de-
signed the system will disallow that any statement is derivable. For the minimal
theory we require its consistency and the consistency of any theory extension,
i.e. from a theory a proof of False is not possible or equivalently some statements
are not derivable. Furthermore we require theory extension to be proof-theoretic
?
The author is expected to graduate from PhD studies in 2020.
conservative (also syntactically conservative) [12, p. 41], viz. for a theory T and
an extension T 0 , any formula in the language of T which is provable from the
extension T 0 is also provable from the smaller theory T . This syntactic conser-
vativity implies consistency of all theory extensions. An extension by definitions
shall be syntactic, that is defined terms in a formula of an extended theory can
be replaced by their defining terms and regarded as formulas of smaller theories.
This so-called realizability together with syntactic conservativity are summarized
as meta-safe extensions [13].
In meta-safe theory extensions, definitions can be unfolded and understood
as syntactic abbreviations. In the context of theorem provers this is interest-
ing as theorems of meta-safe theory extensions can be expressed and proven
equivalently in a smaller theory for a possible benefit of reduction of complexity.
Despite regarding a theory and syntactic deducibility of formulae according to
deduction rules, its models and evaluation of formulae in a model offer another
method of study. A model defines what is valid, i.e. what evaluates to True,
especially a model of a theory is a model that at least renders all axioms of the
theory valid. A model of a smaller theory T in a signature Σ can be extended to
a model of a larger theory, with a larger signature such that all valid formulae of
the smaller model are valid in the larger model. This allows us to regard a dual
notion of proof-theoretic conservativity, called model-theoretic conservativity: A
theory extension T ⊆ T 0 is model-theoretic conservative if each model M for T
can be extended to a model M for T 0 (i.e. M0 models T 0 and M and M0 agree
on the interpretations of terms over the signature Σ).
Both the semantic and the syntactic perspective of a deduction system can
be combined: If for a theory any deducible formula implies its validity in any of
the theory’s models, the system is called sound ; the converse is called complete.
In a sound and complete system model-theoretic conservativity implies proof-
theoretic conservativity.
Isabelle/HOL implements higher-order logic with rank-1-polymorphism and
ad hoc overloading. That is, for a constant several definitions for different non-
overlapping polymorphic types (i.e. non-unifying types) can be provided. An
example illustrates these features. We define a type α lists and constant instances
map, that applies a given function to every item in a given structure, for lists
and for sets. We assume that sets have been defined. Lists shall be defined
inductively as either the empty list [ ] or as x : xs with a head x of type α
and a tail xs of type α list. We extend this theory by an operation on lists:
map(α→β)→α list→β list . On empty lists this is defined as map(f, [ ]) ≡ [ ] and
map(f, x : xs) ≡ f (x) : map(f, xs) for non-empty lists. We introduce a constant
instance for sets map(α→β)→α set→β set by defining map(f, A) ≡ f (A). By these
definitions lists and sets are not instances of one another and the definitions are
not circular.
A mechanism of theory extension has to prevent overlapping definitions for
the same constant and also prevent the introduction of circular dependencies. An
example [6] illustrates the danger. Let cα be a declared polymorphic constant.
Let τ ≡ {True, cbool } define a type and then cbool ≡ ¬(∀xτ , yτ : xτ = yτ ) define
the constant instance. Assume that cbool = True, which by the definition of
τ is equivalent to τ ≡ {True}. The formula ∀xτ , yτ : xτ = yτ holds (i.e. is
True) as it states that τ is a singleton, and thus cbool = False. Summarised,
cbool = True ⇔ cbool = False proves this theory inconsistent. Note that a declared
constant cα can be used prior to definition of any of its instances. In [6] the
authors propose a mechanism for extension of definitional theories that disallows
circularities and makes the extension consistent.
To achieve a solid theoretical foundation for Isabelle/HOL we investigate if
the definitional mechanism introduced in [6] makes theory extension
proof-theoretic and model-theoretic conservative. The HOL system is
not complete with respect to standard semantics by an argument that bases on
Gödels incompleteness theorem [10, Section 2.4.5], which motivates the study of
different semantics that render the system sound and complete.
2 Related work
The documentation of the HOL system logic [10] defines and discusses the foun-
dation of the HOL deduction system. Exemplary is the proof that the HOL
system possesses a standard model for the extension mechanism: Extension by
type and constant instance specification. Isabelle/HOL extends this mechanism
and allows several definitions of instances for a constant and constants that need
not be defined for all types.
Wenzel [13] defines safe extension of theories by constant instances, where
constant instances are defined at once and extensions by type definitions and
constant instance definitions can not be mixed.
Obua [11] discovers that checking conservative overloading in a logic HOLCO
is not semi-decidable and furthermore discusses that the term rewriting system
for definitions needs to be terminating for a theory to be consistent. Our initially
given example shows the weak point: Inconsistency can be introduced by the
interplay of type definitions and constant instance definitions, which had not
been considered.
Kunčar and Popescu in [6] introduce a decidable dependency relation for def-
initional theories of HOL and thereby define well-formed definitional theories.
The type substitutive transitive closure of the dependency relation of these the-
ories is terminating, i.e. does not contain cycles. To ease the understanding we
give a simplified definition: A term and either a constant instance or a type are
in the type substitutive closure of the dependency relation ↓+ , if the definition
of the constant instance or type is necessary to evaluate the term. In addition
they prove consistency of these theories by new semantics.
In [7] each definitional HOL theory is proven syntactically consistent. In
a purely syntactic manner definitions can be understood as abbreviations and
thus unfolded in the introduced deduction system HOLC. The system adds type
comprehensions to translate type definitions from Isabelle/HOL into HOLC and
get consistency of Isabelle/HOL by a consistency result in HOLC.
In a draft [8] the authors prove the syntactic conservativity of definitional the-
ories as extensions of the minimal theory MIN. Constant instances get translated
to their respective instance of the definitional term and the types are replaced
in a more complex manner. This conservativity result implies consistency of any
theory, by the consistency of the minimal theory.
Andrews introduces a formulation of higher-order logic Q0 (also known as
simple type theory) [1, Chapter 5], that introduces the logical operators as con-
stants based on equality and has one deduction rule for substitution of equal
terms. The system Q0 is sound and complete for a non-standard semantics, that
is for types α and β the domain of interpretation of functions Dα→β is relaxed
such that it can be a proper subset of all possible values Dα → Dβ . In contrast
to HOL, Q0 does not support polymorphic constant definitions.
Geuvers and Nederpelt [9] and Geuvers [3] discuss properties of Calculus of
Constructions extended λC with definitions and primitive notions. This flavour
of typed lambda calculus with definitions, called λD0 allows non-polymorphic
definitions that are acyclic by design. Similarly to the intend in Isabelle/HOL,
definitions in λD0 are abbreviations, i.e. syntactical and can be unfolded. An ex-
tension λD additionally introduces primitive definitions, i.e. axioms. The authors
discuss properties relating to conservativity and realizability, e.g. [9, Lem 10.4.1],[3,
Lem 3.10, Lem 3.18]. The developed framework is very general and as examples
for the expressiveness different logics are encoded in λD [9] and they give further
evolved examples. Feasibility and decidability play an important role as λD is
based on type theory.
3 Proposed solution
We propose a generalisation of [6] that equates to a notion of model-theoretic con-
servativity of an arbitrary extension of well-formed definitional theories. As ini-
tially discussed, model-theoretic implies proof-theoretic conservativity if sound-
ness and completeness holds for the deduction system. We investigate whether
semantics based on the ideas of [1] are sound and complete, especially the re-
laxation of the requirement on domains of functions. We expect the soundness
result to be straight-forward, as opposed to the completeness proof, that we in-
tend to approach by constructing a model for a consistent set of formulae [1].
Thus, we obtain an – opposed to [8] – relative proof-theoretic conservativity from
the model-theoretic result by completeness and soundness of the proof-system.
4 Preliminary work
We have worked on model-theoretic conservativity that is based on a non-
standard model definition and we have proven the following statement.
Let D be a well-formed definitional theory with a model M. Let
D0 be a well-formed definitional theory that extends D. Then
there exists a model M0 of D0 , such that M and M0 agree on
the interpretations of all terms that do not contain any instances
of the terms defined by S(D0 , D).
The mentioned theory S(D0 , D) is the biggest subset of D0 such that each of the
defining terms in that set transitively uses an instance of the definitions that
were added through the extension by D0 \ D. The theories D0 \ D and S(D0 , D)
are equal if the terms added to D to obtain D0 do not change the interpretation
of the terms defined in D.
Our result [2] extends and generalises [6], as model-theoretic conservativity
implies the consistency of definitional theories. Furthermore, we are working on
the completeness proof that makes the proof-system complete with respect to
non-standard semantics.
5 Expected contributions
We expect to contribute to the understanding of higher-order logic as imple-
mented in Isabelle/HOL by
– the earlier sketched result on model-theoretic conservativity,
– a soundness and a completeness result with respect to non-standard se-
mantics together with proof-theoretic conservativity (implied by the model-
theoretic conservativity), and
– formalisations in Isabelle/HOL of the two expected theoretic contributions.
6 Plan for evaluation and validation
As typical for theoretic work, our results are validated by the scientific commu-
nity, e.g. by peer review. Furthermore we want to validate all obtained abstract
level pen-and-paper proofs by a theorem prover. The formalisation additionally
strengthens the results of a pen-and-paper proof and can reveal mistakes.
7 Current status
The work on model-theoretic conservativity is accepted for publication. Until
the end of this year we intend to complete the work on the soundness and
completeness proof, so that it can become part of the author’s licentiate thesis.
The formalisation is foreseen in 2018 for the time after the licentiate. Being at
an early stage in the PhD studies with planned graduation in 2020, the plan is
subject to changes.
References
1. P. B. Andrews. An Introduction to Mathematical Logic and Type Theory: To Truth
through Proof. Number 27 in Applied logic series. Kluwer Academic Publishers,
Dordrecht ; Boston, 2nd ed edition, 2002.
2. A. Gengelbach and T. Weber. Model-theoretic Conservative Extension of Defini-
tional Theories. Draft.
3. H. Geuvers. Properties of a Lambda Calculus with Definitions. 2014.
4. F. Haftmann and T. Nipkow. Code Generation via Higher-Order Rewrite Systems.
In SpringerLink, pages 103–117. Springer, Berlin, Heidelberg, Apr. 2010.
5. G. Klein, J. Andronick, K. Elphinstone, G. Heiser, D. Cock, P. Derrin, D. Elkaduwe,
K. Engelhardt, R. Kolanski, M. Norrish, T. Sewell, H. Tuch, and S. Winwood. seL4:
Formal Verification of an Operating-system Kernel. Commun. ACM, 53(6):107–
115, June 2010.
6. O. Kunčar and A. Popescu. A Consistent Foundation for Isabelle/HOL. In C. Ur-
ban and X. Zhang, editors, Interactive Theorem Proving, number 9236 in Lecture
Notes in Computer Science, pages 234–252. Springer International Publishing, Aug.
2015.
7. O. Kunčar and A. Popescu. Comprehending Isabelle/HOL’s Consistency. In
H. Yang, editor, Programming Languages and Systems - 26th European Sympo-
sium on Programming, ESOP 2017, Held as Part of the European Joint Confer-
ences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April
22-29, 2017, Proceedings, volume 10201 of Lecture Notes in Computer Science,
pages 724–749. Springer, 2017.
8. O. Kunčar and A. Popescu. Safety and Conservativity of Definitions in HOL and
Isabelle/HOL. Technical report, 2017.
9. R. P. Nederpelt and H. Geuvers. Type Theory and Formal Proof: An Introduction.
Cambridge University Press, Cambridge ; New York, 2014.
10. M. Norrish and K. Slind. The HOL System LOGIC, Nov. 2014.
11. S. Obua. Checking Conservativity of Overloaded Definitions in Higher-Order Logic.
In Term Rewriting and Applications, pages 212–226. Springer Berlin Heidelberg,
Aug. 2006.
12. J. R. Shoenfield. Mathematical Logic. A.K. Peters, Natick, Mass, 1967.
13. M. Wenzel. Type classes and overloading in higher-order logic. In E. L. Gunter
and A. Felty, editors, Theorem Proving in Higher Order Logics, number 1275 in
Lecture Notes in Computer Science, pages 307–322. Springer Berlin Heidelberg,
Aug. 1997.