Veried Representations of Landau's \Grundlagen" in the Family and in the Calculus of Constructions
Ferruccio Guidi, Mura Anteo Zamboni · 2015
ion λC CC unrestricted (◻,◻) (◻T ,◻T ) (◻T ,◻P ) (◻P ,◻T ) (◻P ,◻P ) (◻,⋆) (◻T ,Type) (◻T ,Prop) (◻P ,Type) (◻P ,Prop) (⋆,◻) (Type,◻T ) (Type,◻P ) (Prop,◻T ) (Prop,◻P ) (⋆,⋆) (Type,Type) (Type,Prop) (Prop,Type) (Prop,Prop) restricted (⋆,◻) (Type,◻P ) (Prop,◻P ) (⋆,⋆) (Type,Type) (Type,Prop) (Prop,Type) (Prop,Prop) Note: we assume (Type ∶ ◻T ) and (Prop ∶ ◻P ). Fig. 18. The categories of abstractions in the CC-GdA. λProlog programming language of the discussed validation procedure for λδ version 3, processes this representation of the λδ-GdA without errors or warnings. The whole source code of Helena 0.8.2 amounts to 350 KiB including comments. The λProlog implementation of the mere validation procedure is 50 clauses long. On our hardware, a 3 GHz Intel processor (1.3 MHz bus, 12 MB cache) with 10K rpm (3 Gb/s SATA) hard drives, we measured the execution times of Figure 16 concerning Helena (processing the QE-GdA), and Coq (processing the CC-GdA). We stress that the CC-GdA is a faithful presentation of the corrected QE-GdA in that the QE-GdA is αδη-equivalent to the CC-GdA, once abstractions and function types are replaced by the corresponding unified binding constructions. Automath η-equivalence solves the incompatibilities between Aut-QE and CC, δ-equivalence is introduced for convenience, and α-equivalence is necessary because of different naming conventions in the QE-GdA and in Coq. Figure 17 shows the first ten constants of the Grundlagen as they appear in the QE-GdA and in the CC-GdA. The reader sees both definitions and axioms. Our work shows that CC is an upper-bound system for validating the CC-GdA, but we may ask whether a subsystem can be used as well. The mechanical inspection of the abstractions occurring in the λδ-GdA shows the situation of Figure 18, from which we argue that validation really needs the full power of CC, including the impredicative Π’s of category (◻,⋆) according to the classification in [Bar93]. On the other hand, if we follow Automath’s perspective and we present block openers as λ-abstractions, we see that the λδ-GdA is valid in Λ∞ + λP . This system only allows predicative constructions [Gui09b], and is located in the middle of the diagonal connecting λP and λC in the λ-Cube [KLN01]. That is, in the center of its right face. In particular, we note that the λ-abstractions of category (◻,⋆) are much less expressive than the corresponding Π-abstractions. Our translation of the QE-GdA into CC and the one of [Bro11] are similar in concept. Both need dynamic analysis to disambiguate some unified binders occurring in the text, and rely on verifying the text in a suitable type theory for this task. However, we see some important differences. Firstly, Brown’s automated procedure for solving type inconsistencies applies 25 ∀-introductions to the text, whereas we apply just 21 ∀-introductions by hand. In this respect, our translated text is more faithful to the original than Brown’s one. Secondly, Brown relies on Contextual Pure Type Systems, whose verification algorithm is based on type checking. On the contrary we rely on λδ version 3, whose verification algorithm is theoretically faster being based on validation. Unfortunately we cannot compare the two verification algorithms at the moment because our verifier is written in Caml while Journal of Formalized Reasoning Vol. 8, No. 1, 2015. Landau’s “Grundlagen” in the Calculus of Constructions ⋅ 113 Brown’s one is written in Lisp. As a minor remark, we note that Brown translates Automath definitions to Coq by duplicating their context on their type and body. On the contrary, we avoid this duplication by using type-annotated terms. Thus, our translated text is even more faithful to the original than Brown’s one. On the other hand, Brown removes the (many) unnecessary context items from the translated text, while we leave this optimization for the future. Thus, Coq 8.4.3 verifies his translated text 18% faster than ours on our hardware. As of now, the CC-GdA is a user-level script consisting of a flat sequence of lines, each declaring or defining a constant of the QE-GdA in the syntax of CC. In order to be usable as a background for formalized mathematics, this script must be improved by making the original structure of the Grundlagen explicit. In particular, we would like to see definitions and propositions typeset with domain-specific mathematical notation. Proofs should appear in a domain-specific language as well, and the whole matter should be organized in different files respecting the system of chapters and sections that we see in [Lan65]. Such a step will require to operate manually of the λδ-GdA with the help of a dedicated technology supervising crucial aspects of the work. For instance, defining and inserting notations, or applying semantics-preserving changes. The QE-GdA, the λδ-GdA and the CC-GdA, as well as Helena 0.8.2, are available at λδ Web site: .