[isabelle] Representing type dependencies in Isabelle/HOL and in dependent type theory – Fwd: Standard group theory in Isabelle/HOL and in dependent type theory (using type abstraction)



As I do not expect any substantial new argument, let me shortly summarize my account on representing type dependencies in Isabelle/HOL and in dependent type theory.

While I have always emphasized that the logical foundation should be a further development of Q0, with expressiveness as the main criterion for the design (hence, Hilbert-style, use of the description operator, no implicit use of the Axiom of Choice),
	(Peter B. Andrews: A Formulation Based on Equality – https://owlofminerva.net/sep-q0 <https://owlofminerva.net/sep-q0>)
	(Andrew M. Pitts on HOL vs. Q0: “From a logical point of view, it would be better to have a simpler substitution primitive, such as ‘Rule R’ of Andrews’ logic Q0, and then to derive more complex rules from it.” – https://owlofminerva.net/files/fom_2018.pdf#page=6 <https://owlofminerva.net/files/fom_2018.pdf#page=6>)
	(Mike Gordon on the use of the epsilon operator in HOL: “It must be admitted that the ε-operator looks rather suspicious.” “The inclusion of ε-terms into HOL ‘builds in’ the Axiom of Choice [...].” – https://owlofminerva.net/files/fom_2018.pdf#page=9 <https://owlofminerva.net/files/fom_2018.pdf#page=9>)

it is also clear that for interactive theorem proving or automation, a natural deduction variant is required, and a meta-logic is desirable in order to symbolically represent metatheorems employing a symbol for derivability/provability.
	(Lawrence C. Paulson introducing ‘meta-implication’ – https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-130.pdf#page=5 <https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-130.pdf#page=5>)


The task of the meta-logic is exploring the properties of a given (object) logic, i.e., expressing metatheorems which are inexpressible within the object logic, and also the theorems of the logic themselves, which can be expressed in the form of a metatheorem.

However, concerning the use of the meta-logic in HOL-Algebra (group theory: abstract algebra), the case is entirely different.


Emulating type restrictions and type dependencies as set-theoretic conditionals in Isabelle's meta-logic is an attempt to enhance the given object logic, and clearly contrary to the approach of type theory, where such conditions are syntactically represented.
One may accept this as a preliminary workaround, but in general, representing these type restrictions and type dependencies is a matter of the underlying object logic (in this case type theory).
I have positively shown that group theory can be naturally expressed in type theory (using type abstraction) – https://www.owlofminerva.net/files/formulae.pdf#page=362 <https://www.owlofminerva.net/files/formulae.pdf#page=362>.


So as long as the object logic is insufficient, one may accept the auxiliary approach of using set-theoretic conditionals in the meta-logic as a workaround, which is obviously opposed to the very idea of type theory, in which these restrictions (e.g., the closure of the operation and of the unit in groups) are expressed syntactically as types within the object logic (and not as meta-logical implications in the meta-logic).

But one should be aware of the fact that this emulation is only a preliminary workaround, not a satisfying solution.

The deficits of the (current) HOL family are well known.
	(Freek Wiedijk on the (current) HOL family: “The HOL type system is too poor. As we already argued in the previous section, it is too weak to properly do abstract algebra.” – https://owlofminerva.net/files/fom_2018.pdf#page=10 <https://owlofminerva.net/files/fom_2018.pdf#page=10>)
	(John Harrison, Josef Urban, and Freek Wiedijk on the (current) HOL family: “Another limitation of the simple HOL type system is that there is no explicit quantifier over polymorphic type variables, which can make many standard results [...] awkward to express [...]. [...] For example, in one of the most impressive formalization efforts to date [Gonthier et al., 2013] the entire group theory framework is developed in terms of subsets of a single universe group, apparently to avoid the complications from groups with general and possibly heterogeneous types.” – https://owlofminerva.net/files/fom_2018.pdf#page=10 <https://owlofminerva.net/files/fom_2018.pdf#page=10>)


Using the enhanced expressive power gained from the meta-logic of a logical framework such as Isabelle for compensating the deficits of the object logic (with a deprecated type system) and, after that, defending the obviously impoverished type system, is unacceptable.


____________________________________________________

Ken Kubota
https://doi.org/10.4444/100



> Anfang der weitergeleiteten Nachricht:
> 
> Von: Ken Kubota <mail at kenkubota.de>
> Betreff: Standard group theory in Isabelle/HOL and in dependent type theory (using type abstraction)
> Datum: 24. Juli 2020 um 16:37:07 MESZ
> An: Manuel Eberl <eberlm at in.tum.de>
> Kopie: cl-isabelle-users <cl-isabelle-users at lists.cam.ac.uk>, "Prof. Kevin Buzzard" <k.buzzard at imperial.ac.uk>, "Prof. Lawrence C. Paulson" <lp15 at cam.ac.uk>
> 
> 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 <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:
> ## Group property identity element only (with identity element abstracted)
> 
> := GrpIdO [λgτ .[λlggg.[λeg.GrpIdyo](og)](og(ggg))]
> # wff 270 : [λg.[λl.[λe.GrpIdy]]]o\3(\4\4\3)τ := GrpIdO 
> 
> 	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:
> 1. Simple or polymorphic type theory (e.g., Q0, HOL, HOL4) alone is clearly insufficient for expressing abstract algebra (e.g., group theory).
> 2. 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>).
> 3. 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 <https://doi.org/10.4444/100>
> 
> 
> 
>> Am 24.07.2020 um 09:21 schrieb Manuel Eberl <eberlm at in.tum.de <mailto:eberlm at in.tum.de>>:
>> 
>> On 23/07/2020 23:24, Ken Kubota wrote:
>>> Let me ask directly. Is it possible to:
>>> 1. Prove a property in an abstract way for all groups (e.g., the
>>> uniqueness of the identity element),
>> 
>> Of course:
>> 
>> lemma (in monoid) one_unique:
>>  assumes "u ∈ carrier G"
>>    and "⋀x. x ∈ carrier G ⟹ u ⊗ x = x"
>>  shows "u = 𝟭"
>> 
>> What you cannot do (due to lack of type-level quantification) is write
>> down a statement like "there exists a group G such that …" without
>> fixing the type of G. But I've never seen that cause problems in practice.
>> 
>>> 2. and then, given a certain group, transfer (instantiate) this theorem
>>> for that particular group without having to carry out the proof again?
>>> If so, please provide a link.
>> 
>> All you have to prove is that the structure you're looking at is indeed
>> a monoid and then you get that theorem. For instance, HOL-Number_Theory
>> defines
>> 
>> definition residue_ring :: "int ⇒ int ring"
>>  where
>>    "residue_ring m =
>>      ⦇carrier = {0..m - 1},
>>       mult = λx y. (x * y) mod m,
>>       one = 1,
>>       zero = 0,
>>       add = λx y. (x + y) mod m⦈"
>> 
>> and then proves that this is a commutative ring for "m > 1". That gives
>> you for free that the additive and multiplicative subgroup are abelian
>> groups (and therefore monoids) and you can use the above fact. You can
>> also talk about subgroups of these groups and apply the result to them.
> 




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.