Mathematical knowledge is publicly available in dozens of di erent formats and languages, ranging from informal (e.g. Wikipedia) to formal corpora (e.g., Mizar). Despite an enormous amount of overlap between these corpora, few machine-actionable connections exist. We speak of alignment if the same concept occurs in di erent libraries, possibly with slightly di erent names, notations, or formal de nitions. Leveraging these alignments would create a huge potential for knowledge sharing and transfer, e.g., integrating theorem provers or reusing services across systems. Formally describing and verifying alignments is extremely expensive, as it typically requires not only aligning two concepts but whole libraries together with their foundations, or may even be impossible in case of alignments between semi-formal or informal concepts. Therefore, we introduce a lightweight approach that focuses on identifying the alignments while abstracting from formal de nitions. Notably, this is already su cient for many practically valuable applications. We present a classi cation of alignments and design a simple format for describing alignments as well as an infrastructure for sharing them. We propose these as a centralized standard for the community to collect and curate alignments from the di erent kinds of mathematical corpora, including proof assistant libraries, computer algebra and programming language algorithms, and semi-formal libraries.
Motivation and Related Work The sciences are increasingly collecting and curating their knowledge systematically in machine-processable corpora. For example, in biology many important corpora take the form of ontologies, e.g., as collected on BioPortal. These corpora typically overlap substantially, and much recent work has focused on integrating them. A central problem here is to nd alignments: pairs (a1; a2) of identi ers from di erent corpora that describe the same concept.
For ontologies, this problem has been relatively well-studied under the heading ontology matching [ESC07]. The situation in mathematics is somewhat special because mathematical knowledge involves rigorous notations, de nitions, and properties, and attempts to capture it fully lead to very diverse corpora. Logical corpora have been developed in proof assistants and feature machineunderstandable theorems and proofs. Computational corpora have been developed in computer algebra systems and feature executable de nitions and constructions. And narrative corpora have been developed in wikis and related tools featuring human-oriented semi-formal descriptions. For each kind, there are multiple large corpora, often the result of dozens of person-years of investment.
Alignments between computational corpora occur in bridges between the run time systems of programming languages. Alignments between logical and computational corpora are used in proof assistants with code generation such as Isabelle [WPN08] and Coq [Coq15]. Here functions de ned in the logic are aligned with their implementations in the programming language in order to generate fast executable code from formalizations.
Wiedijk [Wie06] explored a single theorem (and its proof) across 17 proof assistants implicitly providing alignments between the concepts present in the theorem's statement and proof. However, nding alignments has proved extremely di cult in general. There are three reasons for this: the conceptual di erences between the three kinds of corpora; the di erences between the underlying formal languages and tools; and the di erences between the organization of the knowledge in the corpora.
The dominant methods for integrating logical corpora so far have focused on truth-preserving translations between the underlying knowledge representation languages. For example, [KS10] translates from Isabelle/HOL to Isabelle/ZF. [KW10] translates from HOL Light to Coq, [OS06] to Isabelle/HOL, and [NSM01] to Nuprl. Older versions of Matita [ACTZ06] were able to read Coq compiled theory les. [CHK+11] build a library of translations between di erent logics.
However, most translations are not alignment-aware, i.e., it is not guaranteed that a1 will be translated to a2 even if the alignment is known. This is because a1 and a2 may be subtly incompatible so that a direct translation may even lead to inconsistency or ill-typed results. [OS06] was | to the authors knowledge | the rst that could be parametrized by a set of alignments. The OpenTheory framework [Hur09] provides a number of higher-order logic concept alignments. In [KR16], the second and fourth author discuss the corpus integration problem and conclude that alignments are of utmost practical importance. Indeed, corpus integration can succeed with only alignment data even if no logic translation is possible. Conversely, logic translations contribute little to corpus integration without alignment data.
An alignment does not need to be perfect to be useful. In some HOL proof assistants real numbers are de ned using Cauchy sequences, while in some Dedekind cuts are used. The two structures undoubtedly share all the real number properties. However, if we look at the implications of the de nitions themselves, the former implies that there is a canonical Cauchy sequence for each number. Despite this minor di erence, we can use such an alignment in a logical translation [KK13]. In fact there is a whole spectrum of perfectness of alignments. An alignment can indeed be perfect when the de nitions of two concepts are the same in a logical corpus. Aligning functions that have the same speci cations, but di fer only in the complexity is particularily useful in computational corpora, for example interfacing languages. Finally, concepts may be just similar. In set theory zero is de ned as the empty set, while in many other foundations is it a constructor of an inductive type. Only a quarter of the properties of the empty set are the same as those of explicitly de ned zero.
Many practical services are enabled even by such imperfect alignments. Statistical analogies extracted from large formal libraries combined with imperfect alignments can be used to create new conjectures to automatically explore a logical corpus [GKU16]. Automated reasoning services can use the libraries of alignments to provide more precise proof recommendations [GK15]. Further ideas include searching for a single query expression in multiple corpora at once [AGC+04,KR14].
Due to the size of the involved corpora, it is desirable to nd alignments automatically. Recently, the rst author has developed heuristic methods for automatically nding alignments [GK14] targeted at integrating logical corpora [KK13] including HOL Light, HOL4, and Isabelle/HOL discovering 398 pairs of isomorphic concepts. Consistent name hashing combined with statement normalization was used to discover 39 symbols with equivalent de nitions [KU15] in the Flyspeck development [H+15]. Ginev built a library of about 50,000 alignments between narrative corpora including Wikipedia, Wolfram Mathworld, PlanetMath and SMGloM [GC14].
Contribution and Overview Our contribution is two-fold. First, we present a phenomenological study of alignments between mathematical corpora in Section 2. Most importantly, we collect the various subtle reasons why an alignment may be imperfect because not all properties of the aligned symbols transfer exactly.
Our standardization includes a standardization of forming MMT URIs [RK13] for a number of a major logical corpora in Section 3. These assign a canonical URI to every symbol in a way that is unique across corpora and across logics. We use these URIs to give several examples from logical corpora in Section 4. The examples focus on logical corpora, but our results carry over to other kinds of corpora as well.
Second, we propose a standard for storing and sharing alignments. Most corpora are developed and maintained by separate, often disjoint communities. That makes it di cult for researchers to utilize alignments because no central repository exists for jointly building a large collection of alignments. We have started such a central repository | it is public, and we invite all researchers to contribute their alignments. We seeded our repository with the alignment sets mentioned above. Moreover, we are hosting a web-server that allows for conveniently querying for all symbols aligned with a given symbol. We describe this standard and infrastructure in Section 5. 2
Let us assume two corpora C1; C2 with underlying foundational logics F1; F2. We examine examples for how two concepts ai from Ci can be aligned. Perfect Alignment If a1 and a2 are logically equivalent modulo a translation ' that is xed in the context, we speak of a perfect alignment. More precisely, all formal properties (type, de nition, axioms) of a1 carry over to a2 and vice versa. Typical examples are primitive types and their associated operations. Consider:
then translations between C1 and C2 can simply interchange a1 and a2.
The above example is deceptively simple for two reasons. Firstly, it hides the problem that F1 and F2 do not necessarily share the symbol Type. Therefore, we need to assume that there are symbols Type1 and Type2, which have been already aligned (perfectly). Such alignments are crucial for all fundamental constructors that occur in the types and characteristic theorems of the symbols we want to align such as Type, !, bool, ^, etc. These alignments can be handled with the same methodology as discussed here. Therefore, here and below, we assume we have such alignments and simply use the same fundamental constructors for F1 and F2.
Secondly, it ignores that we usually only want certain formal properties to carry over, namely those in the interface theory in the sense of [KR16]. For example, in Section 4 we give many perfect alignments between symbols that use di erent but interface-equivalent de nitions.
Alignment up to Argument Order Two function symbols can be perfectly aligned except that their arguments must be reordered when translating.
The most common example is function composition, whose arguments may be given in application order (f g) or in diagram order (f ; g). Another example is given contains1 : (T : Type) ! SubSet T ! T ! bool in2 : (T : Type) ! T ! SubSet T ! bool Here the expressions contains1(T; A; x) and in2(T; x; A) are aligned. Alignment up to Determined Arguments The perfect alignment of two function symbols may be broken because they have di erent types even though they agree in most of their properties. This often occurs when F1 uses a more ne-granular type system than F2, which requires additional arguments.
Examples are untyped and typed (polymorphic, homogeneous) equality: The former is binary, while the latter is ternary eq1 : Set ! Set ! bool
eq2 : (T : Type) ! T ! T ! bool: The types can be aligned, if we apply '(Set) to eq2. Similar examples arise between simply- and dependently-typed foundations, where symbols in the latter take additional arguments.
These additional arguments are uniquely determined by the values of the other arguments, and a translation from C1 to C2 can drop them, whereas the reverse translations must infer them { but F1 usually has functionality for that.
The additional arguments can also be proofs, used for example to represent partial functions as total functions, such as a binary and a ternary division operator div1 : Real ! Real ! Real
div2 : Real ! (d : Real) ! ` d 6= 0 ! Real Here inferring the third argument is undecidable, and it is unique only in the presence of proof irrelevance.
Alignment up to Totality of Functions The functions a1 and a2 can be aligned everywhere where both are de ned. This often happens since it is often convenient to represent partial functions as total ones by assigning values to all arguments. The most common example is division. div1 might both have the type Real ! Real ! Real with x div1 0 unde ned and x div2 0 = 0.
Here a translation from C1 to C2 can always replace div1 with div2. The reverse translation can usually replace div2 with div1 but not always. In translationworthy data-expressions, it is typically sound; in formulas, it can easily be unsound because theorems about div2 might not require the restriction to non-zero denominators.
Alignment for Certain Arguments Two function symbols may be aligned only for certain arguments. This occurs if a1 has a smaller domain than a2.
The most fundamental case is the function type constructor ! itself. For example, !1 may be rst-order in F1 and !2 higher-order in F2. Thus, a translation from C1 to C2 can replace !1 with !2, whereas the reverse translation must be partial.
Another important class of examples is given by subtyping (or the lack thereof). For example, we could have plus1 : Nat ! Nat ! Nat
plus2 : Real ! Real ! Real:
Another way for a1 to have a smaller domain is to take less arguments. For example, we might have ln1 : Real ! Real
log2 : Real ! Real ! Real where ln2(x) can be translated to log2(e; x).
Alignment up to Associativity An associative binary function (either logically associative or notationally right- or left-associative) can be de ned as a exary function, i.e., a function taking an arbitrarily long sequence of arguments. In this case, translations must fold or unfold the argument sequence. For example plus1 : Nat ! Nat ! Nat plus2 : List Nat ! Nat: Contextual alignments Two symbols may be aligned only in certain contexts. For example, the complex numbers are represented as pairs of real numbers in some proof assistant libraries and as an inductive data type in others. Then only selected occurrences of pairs of real numbers can be aligned with the complex numbers. Alignment with a Set of Declarations Here a single declaration in C1 is aligned with a set of declarations in C2. An example is a conjunction a1 in C1 of axioms aligned with a set of single axioms in C2. More generally, the conjunction of a set of C1-statements may be equivalent to the conjunction of a set of C2-statements.
Here translations are much more involved and may require aggregation or projection operators.
Alignment between the Internal and External Perspective on Theories Logical theories can be represented in two ways. We de ne them only by example. We speak of the internal perspective if we use a theory like
theory Magma1 = fu1 : Type; 1 : u1 ! u1 ! u1g and of the external perspective if we use operations like
Magma2 : Type; u2 : Magma2 ! Type; 2 : (G : Magma) ! u2 G ! u2 G ! u2 G Here we have non-trivial, systematical translation from C1 to C2; a reverse may also be possible, depending on the details of F1.
Corpus-Foundation Alignment Orthogonal to all of the above, we have to consider alignments, where a symbol is primitive in one system but de ned in another. More concretely, a1 can be built-into F1 whereas a2 is de ned in F2. This is common for corpora based on signi cantly di erent foundations, as each foundation is likely to select di erent primitives. Therefore, it mostly occurs for the most basic concepts. For example, the boolean connectives, integers and strings are de ned in some systems but primitive in others, as in some foundations they may not be easy to de ne.
The corpus-foundation alignments can be reduced to previously considered cases if we follow the \foundations-as-theories" approach [KR16], where the foundations themselves are represented in an appropriate logical framework. Then a1 is simply an identi er in the corpus of foundations of the framework F1. Opaque Alignments The above alignments focused on logical corpora, partially because logical corpora allow for precise and mechanizable treatment of logical equivalence. Indeed, alignments from a logical into a computational or narrative corpus tend to be opaque: Whether and in what way the aligned symbols correspond to each other is not (or not easily) machine-understandable. For example, if a2 refers to a function in a programming language library, that functions speci cation may be implicit or given only informally. Even worse, if a2 is a wiki article, it may be subject to constant revision.
Nonetheless, such alignments are immensely useful in practice and should not be discarded. Therefore, we speak of opaque alignments if a2 refers to a symbol whose semantics is unclear to machines.
An essential requirement for relating logical corpora is standardizing the identi ers so that each identi er in the corpus can be uniquely referenced. It is desirable to use a uniform naming schema so that the syntax and semantics of identi ers can be understood and implemented as generically as possible. Therefore, we use MMT URIs [RK13], which have been speci cally designed for that purpose. 3.1
Syntax MMT URIs are triples of the form
The namespace part is a URI that serve as globally unique root identi ers of corpora (e.g., http://mathhub.info/MyLogic/MyLibray). It is not necessary (although often useful) for namespaces to also be URLs, i.e., a reference to a physical location. But even if they are URLs, we do not specify what resource dereferencing should return. Note that because MMT URIs use ? as a separator, MODULE ? SYMBOL is the query part of the URI, which makes it easy to implement dereferencing in practice.
The module and symbol parts of an MMT URI are logically meaningful names de ned in the corpus: The module is the container (e.g., a signature, functor, theory, class, etc.) and the symbol is a name inside the module (of a type, constant, axiom, theorem etc.). Both module and symbol name may consist of multiple /-separated segments to allow for nested modules and quali ed symbol names.
MMT URIs allow arbitrary Unicode characters. However, ? and =, which MMT URIs use as delimiters, as well as any character not legal in URIs must be escaped using the %-encoding. We refer to RFC 3986/7 for details.
Both the corpus itself and the system with which it was processed may be subject to change. Therefore, it may be useful to record a version in an MMT URI. However, most developers take care to avoid semantically critical changes at least to the widely used parts of their corpora. Since those parts are also the most interesting ones for integration, we omit issues of versioning here and simply remark that the version can be recorded as a part of the root namespace. Formation Principles The precise formation of MMT URIs may depend subtly on the foundational logic underlying the corpus. In the sequel, we identify some general principles that allow stating the formation rules concisely.
The most important physical structure of a corpus is usually a directory tree, whose leaves are les containing modules. In this case, the following principles are typical options to de ne namespaces: { at structure: All modules use the same namespace as the root namespace of the corpus regardless of their physical location in the corpus. This naming schema is most well-known from SML. { directory-based structure: The namespace of a module is formed by concatenating the root namespace with the path to the directory containing it. There are two subcases regarding the treatment of the le name: les-as-modules: The le contains exactly one module. The name of the module may be given explicit ly in the le or may be implicit. Either way, the name of the module must be the same as the le name without the le name extension. Files as explicitly named modules is most wellknown as the convention of Java. irrelevant le names: The le name is irrelevant, i.e., the grouping of modules into les within the same directory is arbitrary. In particular, a le can contain multiple modules. { le-based structure: The namespace of a module is formed by concatenating the root namespace of the corpus with the path to the le containing it. 3.2
Using the principles de ned above, we describe the MMT URI formation principles for some important proof assistants. In all cases, we also assign MMT URIs for the underlying foundations in order to refer to built-in concepts.
PVS [ORS92] uses directory-based namespaces with irrelevant le names. We propose the following root URIs for some important PVS-related corpora: { the PVS foundation: http://pvs.csl.sri.com/foundation { the standard library that is shipped with PVS: http://pvs.csl.sri.com/Prelude { the NASA corpus: http://shemesh.larc.nasa.gov/fm/ftp/larc/PVS-library
Within a PVS corpus, the top-level modules are theories and (co)datatype declarations. The only possible nesting between them is that theories may contain (co)datatype declarations. Consequently, the module names have at most two segments. If a module is a (co)datatype, its symbols are the constructors, testers, etc. These are not hierarchical. If a module is a theory, its symbols are all declarations declared in it. These are not hierarchical. However, if a symbol name N is declared multiple times in the same module (due to overloading), we use two-level names of the form N=i where i numbers all declarations of N in that module (starting from 1).
Coq [Coq15] uses directory-based namespaces with les as implicitly named modules. We propose the following root URIs: { the Coq foundation: https://coq.inria.fr/foundation { the standard library shipped with Coq: https://coq.inria.fr/theories { the Coq contributions: https://coq.inria.fr/contribs { the Mathematical Components corpus (including SSRe ect): http://ssr.msr-inria.inria.fr/math-comp
Coq modules can be nested. Besides the module name given implicitly by the le, Coq les can contain modules and module types. Symbols are all declarations inside a module. Their names can be hierarchic due to generative functor instantiation.
Matita uses the same URIs as Coq except for not allowing nested modules. We suggest the following root URIs: { the Matita foundation: http://matita.cs.unibo.it/foundation { the Matita standard library: http://matita.cs.unibo.it/library
Mizar uses a at namespace. We propose the following root URIs: { the Mizar foundation: http://mizar.org/foundation { the Mizar Mathematical Library (MML): http://mizar.org/library
The Mizar modules are the articles. The name of a module is the name of the article without the le name extension. There is no nesting of modules. The Mizar symbols are all the declarations inside an article. Their names are obtained through a heavily idiosyncratic naming schema that includes generating unique names by numbering the declarations of the same kind in each article. For example, the MMT URI of conjunction is http://mizar.org/corpus?XBOOLEAN0?K4
HOL Light does not have an obvious MMT URI formation principle because it does not maintain all its identi ers itself | instead it relies on the OCaml toplevel to store the assigned values. There are three kinds of HOL Light symbols: types, constants, and theorems; only the former two are visible to the HOL Light kernel. For each type or constant, we use the name visible to the HOL Light kernel. For each theorem, we use the OCaml binding name. OCaml toplevel symbols may be grouped into OCaml modules. This feature is seldom used, as it only a ects theorem names: the kernel is also not aware of the OCaml module in which the de nitions of constants or types are introduced.
This has the e ect that di erent HOL Light les can be incompatible with each other. There are two reasons for this incompatibility: First, toplevel symbols may be overwritten by others, which means that the original ones are no longer accessible and a formalization might fail. This happens for example in case of the OCaml basic output function open in which gets overwritten by a theorem with the same name. Second, the loading of a le may change the state of HOL Light kernel or packages to one that is no longer compatible with another le [Wie09]. For example the theories complexnumbers.ml and complexes.ml both introduce the type complex but with di erent de nitions.
Thus, HOL Light's names do not uniquely identify symbols. Therefore, we use directory-based namespaces with les-as-modules. For constants and types introduced by a module we add the pre xes const/ and type/ respectively. If a le contains OCaml modules, we use their names to form multi-segment module names. Accordingly, if symbols result from OCaml structures, we form multisegment symbol names. This has the e ect that HOL Light URIs are formed in exactly the same way as for Coq.
We propose the following root URIs: { the HOL Light foundation and the library shipped with it:
http://github.com/jrh13/hol-light { the Formal Proof of Kepler formalization [H+15]: http://github.com/flyspeck/flyspeck
For example, the Flyspeck theorem well defined unordered pair is assigned the URI: http://github.com/flyspeck/flyspeck?text_formalization/ packing/marchal3?Marchal_cells_3.well_defined_unordered_pair.
HOL4 internal module names correspond to names of les, however the names of types and constants are not associated with the modules. Furthermore, the names of constants and types are separate. To avoid ambiguity we use the same module names as for HOL Light. We propose the following root URIs: { the HOL4 foundation and the library shipped with it: https://hol-theorem-prover.org
Isabelle is a logical framework: Its distribution includes a number of object logics, and each Isabelle theory uses an object logic (or declares a new one). Isabelle uses les as explicitly named modules. However, it disregards the directory structure: The system makes sure that two modules with same name cannot be loaded in the same session even if they are stored in di erent directories. But as di erent object logics and di erent developments often declare incompatible notions, we still use directory-based namespaces to make sure all theories have unique namespaces.
Isabelle allows several module mechanisms including locales and type classes [HW06]. Therefore, we form nested module names by concatenating theory and locale/type class names. We propose the following root URIs: { Isabelle foundation and distributed libraries: http://isabelle.in.tum.de/ { the Archive of Formal Proofs: http://afp.sf.net/ { the TLA+ logic: http://tla.msr-inria.inria.fr/
For example the type of streams is represented by the URI: http://isabelle.in.tum.de/?HOL/corpus/Stream?stream 4
Using the MMT URIs de ned in Sect. 3, we give a detailed presentation of alignments across proof assistants for three representative concepts. We also include some alignments to programming languages, which are relevant for code generation. In all cases, we will see how big the di erences between the details are across the logical corpora even though most of the alignments are in fact perfect.
Cartesian Product In constructive type theory, there are two common ways of expressing the non-dependent Cartesian product. First, if the foundation has inductive types such as the Calculus of Inductive Constructions, it can be an inductive type with one binary constructor. Second, if the foundation has a dependent sum type, Cartesian products can be the non-dependent special case. The rst two symbols below use the former, the last one the latter approach: { http://coq.inria.fr/theories?Init/Datatypes?prod.ind { http://matita.cs.unibo.it/?datatypes/constructors?Prod.ind { http://isabelle.in.tum.de/?CTT/CTT?times
In higher-order logic, the only way to introduce types is by using the typedef construction, which constructs a new type that is isomorphic to a certain subtype of an existing type. In particular, most HOL systems introduce the Cartesian product A B by using an appropriate unary predicate on A ! B ! bool: { http://github.com/jrh13/hol-light?pair/type?prod { http://hol-theorem-prover.org/?pair/type?prod { http://isabelle.in.tum.de/?HOL/Product?prod
In PVS, the product type constructor is part of the system itself: { http://pvs.csl.sri.com/foundation?PVS?tuple_tp
In set theory, it is also possible to restrict dependent sum types to obtain the Cartesian product. This is used in Isabelle/ZF. In Mizar the Cartesian product is de ned implicitly as a rst order functor, which involves discharging the wellde nedness condition. Therefore, we give the URIs of both the de nition and the generated functor.
{ http://isabelle.in.tum.de/?ZF/ZF?cart_prod { http://mizar.org/library/?ZFMISC_1?K2 (de ned by http://mizar.org/library/?ZFMISC_1?def_2)
Finally, Cartesian products appear in most programming languages and we list here a number of constructions that can be aligned: { http://caml.inria.fr/?core?* { http://haskell.org/?core?, { http://scala-lang.org/?core?, { http://cppreference.com/?std?pair
Informal sources that can be aligned are e.g.: { https://en.wikipedia.org/wiki/Cartesian_product { https://en.wikipedia.org/wiki/Product_type { http://mathworld.wolfram.com/CartesianProduct.html Addition In constructive type theory, addition of natural numbers is typically de ned as a xed points of certain equations.
{ http://coq.inria.fr/theories?Init/Nat?add { http://matita.cs.unibo.it/?nat/plus?plus
Higher-order logic proof assistants usually use high-level constructions for primitive recursion. Interestingly, here the alignment is very obvious at this high-level even though the elaboration into core language features may result in very di erent-looking, but logically equivalent de nitions. This is how addition is implemented in HOL Light and HOL4. Isabelle/HOL uses a similar construction but inside a type class for commutative monoids with di erence. { http://github.com/jrh13/hol-light?arith/const?+ { http://hol-theorem-prover.org/?arithmetic/const?+ { http://isabelle.in.tum.de/?HOL/Nat?plus_nat_inst.plus_nat
In set theory, de ning addition is surprisingly the least straightforward: In Isabelle/ZF, addition uses the primrec construction together with a coercion from non naturals to naturals. PVS de nes a general addition on number elds, which all the concrete number spaces (reals, integers, etc.) inherit. In Mizar, it is the restriction of complex addition to natural numbers. Mizar's complex addition itself is built from the real number addition, which in turn is built from positive real addition, rational addition, and ordinal addition. So in principle it would be possible to align with Mizar's ordinal addition.
{ http://pvs.csl.sri.com/Prelude?number_fields?+ { http://isabelle.in.tum.de/?ZF/Arith?add { http://mizar.org/library/?NAT_1?K2
Most programming languages do not implement arbitrary precision natural numbers. However, it is possible to nd partial mappings, which are in fact already used by e cient code generation [HN10] for Isabelle/HOL natural numbers and the representation of Coq natural numbers by its extended bytecode machine [AGST10].
{ http://caml.inria.fr/?Big_Int?add_big_int { http://haskell.org/?core?+ { http://www.smlnj.org/?IntInf?+ Concatenation of Lists In constructive type theory (e.g. for Matita, Coq), the append operation on lists can again be de ned as a xed point. In higher-order logic, append for polymorphic lists can be de ned by primitive recursion, as done by HOL Light and HOL4. Isabelle/HOL slightly di ers from these two because it uses lists that were built with the co-datatype package [B+14]. { http://coq.inria.fr/theories?Init/Datatypes?app { http://github.com/jrh13/hol-light?lists/const?APPEND { http://hol-theorem-prover.org/?list/const?APPEND { http://isabelle.in.tum.de/?HOL/List?append
In set theory, PVS and Isabelle/ZF also use primitive recursion for monomorphic lists. In Mizar, lists are represented by nite sequences, which are functions from a nite subset of natural numbers (one-based FINSEQ and zero-based XFINSEQ) with append provided.
{ http://pvs.csl.sri.com/Prelude?list_props?append { http://isabelle.in.tum.de/?ZF/List_ZF?app { http://mizar.org/library/?ORDINAL4/K1
Concatenation of lists is also common in programming languages. { http://caml.inria.fr/?core?@ http://haskell.org/?core?++ { http://scala-lang.org/?core?++ 5
Based on the observations of the previous sections, we now de ne a standard for alignments that covers the practically relevant examples. We use the following formal grammar for collections of alignments:
Collection NSDef Alignment Comment ::= ::= ::= ::= (NSDef j Alignment j Comment) namespace String URI URI URI (String = "String") // String Here NSDef de nes abbreviations for CURIEs (as de ned by the W3C), which allows shortening URIs with the same long namespaces. An alignment is just a pair of URIs with a list of key-value pairs, which allows adding author/source, certainty scores, translation instructions, etc.
We also standardize some special keys and possible values that are important for practical applications. As a guiding criterion for de ning these keys, we use how and in which directions expressions with head symbols s1 or s2 can be translated.
The simplest case is the following: De nition 1. A simple alignment between symbols s1 and s2 uses the key direction with the possible values forward, backward, and both. It induces the translation that replaces every occurrence of s1 with s2, or of s2 with s1 according to the value of the key.
This subsumes perfect alignments (where the direction is both) and several unidirectional cases: alignment up to totality of functions or up to associativity, and alignment for certain arguments. The absence of this key indicates alignments where no translation is possible, in particular opaque alignments.
The following case covers alignments up to argument order or determined arguments: De nition 2. An argument alignment uses the key arguments whose value A is of the form (i; j) where i and j are natural numbers.
It induces the translation of s1(x1; : : : ; xm) to s2(y1; : : : ; yn) where yj is the recursive translation of xi if (i; j) is among the pairs in A and inferred from the context if there is no i for which (i; j) is in A.
Example 1. We obtain the following argument alignments for some of the examples from Section 2:
Nat1 Nat2 direction = "both" eq1 eq2 arguments = "(1; 2)(2; 3)" contains1 in2 arguments = "(1; 1)(2; 3)(3; 2)"
We have implemented alignments in the MMT system [Rab13]. Moreover, we have created a public repository3 and seeded it with a number of alignments including the ones mentioned in this paper. The MMT system can be used to read and serve all these alignments, implement the transitive closure, and (if possible) translate expressions according to alignments.
As an example service, we have added alignment support to the MMT web browser: Figure 1 shows a screenshot from browsing the HOL Light library, in particular a snapshot of the pairs module. The symbol prod is aligned with several formal and informal sources, which can be shown and navigated to by rightclicking the symbol in an expression (here in the type of the symbol ABS prod). 3 https://gl.mathhub.info/alignments/Public
Fig. 1. The MMT Server Showing Formal and Informal Alignments 6
We have motivated and proposed a standard for aligning mathematical corpora. We presented examples of alignments between logical, computational, and semiformal corpora and classi ed the di erent examples. The presented MMT-based system for sharing such alignments has been preloaded with thousands of alignments between the various kinds of concepts, including proof assistant types and constants, programming language (including computer algebra) algorithms, and semi-formal descriptions.
Future work includes extending the automated discovery of alignments [GK14] to foundations other than HOL. Our main focus was on the logical corpora, but we expect to be able to nd much more opaque alignments. We invite the community to use the service. Finally we plan to integrate the use of the alignments database in the various mathematical knowledge management systems. Acknowledgements We acknowledge nancial support from the German Science Foundation (DFG) under grants KO 2428/13-1 and RA-1872/3-1 and the Austrian Science Fund (FWF) grant P26201.