Email Gateway (Jul 24 2020 at 14:37): Email Gateway (Jul 24 2020 at 14:37):From: Ken Kubota <mail@kenkubota.de>
First, thank you very much for the extensive explanation, and the reference to Ballarin's paper at https://doi.org/10.1007/s10817-019-09537-9 <https://doi.org/10.1007/s10817-019-09537-9>, which I have read.
Let me focus on two points on how abstract algebra is implemented in Isabelle/HOL.
A. Using locales and meta-logical implication for expressing type dependencies
Best suited for comparison is the monoid definition
locale monoid =
fixes M and composition (infixl "·" 70) and unit ("1")
assumes composition_closed: "[ a ∈ M; b ∈ M ] ⇒ a · b ∈ M"
and unit_closed: "1 ∈ M"
and associative:"[ a ∈ M ; b ∈ M ; c ∈ M ] ⇒ (a · b) · c = a · (b · c)"
and left_unit:"a ∈ M ⇒ 1 · a = a"
and right_unit:"a ∈ M ⇒ a · 1 = a"
as presented by Ballarin (p. 3) and similar to that actually used in HOL-Algebra
https://isabelle.in.tum.de/library/HOL/HOL-Algebra/Group.html
since the group definition itself there has only an abbreviated definition as monoid + inverse element.
The dependencies (Isabelle: "fixes") are the same as in this expression of R0:
:= GrpIdO [λgτ .λlggg.[λeg.GrpIdyo](og)]
https://www.owlofminerva.net/files/formulae.pdf#page=362 <https://www.owlofminerva.net/files/formulae.pdf#page=362>
The variables bound by lambda are: g, l, e
meaning the set (carrier, type), the operation, and the identity element (unit),
and correspond to: M, composition (infixl "·" 70), and unit ("1") in this example.
The type dependency here is represented by g which occurs both at the type level and the term level (type abstraction): [λgτ .[λlggg.[λeg. ...]]]
Since type abstraction is not available in Isabelle/HOL, one cannot naturally express the closure of the operation with the typed expression lggg (l : g -> g -> g),
but one has to use the assumption composition_closed: "[ a ∈ M; b ∈ M ] ⇒ a · b ∈ M"
contrary to the concept of type theory to code such type assumptions syntactically as types.
Using the element relation of set theory (a ∈ M) or some alternative formulation (Ma) is what you usually want to avoid in type theory.
Moreover, since the symbol ⇒ is the meta-logical implication (‘meta-implication’) of Isabelle's meta-logic (and not the logical implication of the object logic Isabelle/HOL), it becomes clear that the formal system (simple or polymorphic type theory) itself is insufficient, but some extension, in this case Isabelle's meta-logic, is required for expressing this type restriction.
In summary:
At least some kind of extension is required, in this case Isabelle's meta-logic is employed
(using the ‘meta-implication’ as described on p. 4 of https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-130.pdf <https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-130.pdf>).
Even then – with the use of some extension (as a workaround) – the coding of the type restrictions is very clumsy in comparison to the natural expression using type abstraction and the substitution of types via lambda conversion (e.g., with N for the natural numbers you would have: [λgτ .[λlggg.[λeg. ...]]]N = [λlNNN.[λeN. ...]], i.e., the closure of the operation l and of the identity element e as syntactical prerequisites).
In other words, what could be easily and naturally represented with type abstraction within the formal language, in Isabelle/HOL also requires the meta-logic as an extension for implementing only a workaround, and moreover requires maybe some dependencies encoded in the "locales".
"Locales are extra-logical. The functors they represent are not encoded in Isabelle’s logic. Instead, whenever a locale is visited—that is, a context block entered—the locale is activated:
– The locale graph is traversed and all reachable locale instances are activated recursively.
– The body of the locale is added to the context, making its declarations available." (Ballarin's paper, p. 5)
"Locales provide means for structuring formal developments, but they do not change the underlying logic, so they do not increase expressiveness. This is a fundamental limitation. On the other hand, locales work on top of any logic provided there is substitution [6, Section 3.1], so they could be provided for a wide range of provers." (p. 26)
It seems that the substitution of types via lambda conversion (using type abstraction) here is replaced by locales.
B. Instantiation
Some substitution must take place in the step from the theorem of the uniqueness of the identity element in groups to that of a particular group.
How is this done in Isabelle/HOL?
Presumably this also requires Isabelle's meta-logic.
How can one obtain the fully expanded internal version of a statement as shown on p. 19 of Ballarin's paper?
Ken Kubota
https://doi.org/10.4444/100
Last updated: Apr 18 2024 at 20:16 UTC