[isabelle] Natural expression of group theory – Re: abelian_group

For a natural expression of group theory type abstraction should be implemented, as suggested by Mike Gordon:

"[…] 'second order' λ-terms like λ𝛼. λx:𝛼. x, perhaps such terms should be included in the HOL logic." [Gordon, 2001, p. 22]

With type abstraction the mechanism of lambda notation can be used to _syntactically_ express the dependencies (here between the term and the type level), which follows the very idea of type theory.

See also:
	https://sourceforge.net/p/hol/mailman/message/35458077/ (section 5)

For a demonstration of an implementation (PDF) run
	make group.r0.out.pdf && open -a Preview $_
	make xor_group.r0.out.pdf && open -a Preview $_

For a demonstration of an implementation (HTML) run
	make group.r0.out.html && open -a Safari $_
	make xor_group.r0.out.html && open -a Safari $_

on a Mac after downloading the software (license restrictions apply) at
PDF generation requires Pandoc with LaTeX installed, and HTML view will cause a call to mathjax.org as the JavaScript display engine for mathematics.

Kind regards,

Ken Kubota


Ken Kubota

> Am 12.04.2019 um 18:20 schrieb Manuel Eberl <eberlm at in.tum.de>:
> HOL-Algebra is a bit messy. A big part of that, I think, comes from
> quirks of Isabelle/HOL itself.
> My guess would be that one can write groups either additively (G, +, 0)
> or multiplicatively (G, *, 1). Of course, more abstract syntax (G, ∘, e)
> is also possible. There are various conventions about when to use which
> notation – in particular, I think the convention is that if you use "+",
> the group is always commutative (i.e. abelian).
> In HOL-Algebra, groups are /always/ written multiplicatively. There is
> no other way. When you have a ring, you can write "+" for addition, but
> that is not formally associated to any group. The additive group of the
> ring has all its properties stated w.r.t. the "*" of "add_monoid R".
> "abelian_group" is apparently some kind of attempt to have an abelian
> group that is written additively. Due to the fact that the "+" operator
> is defined for the ring record, this requires us to use a ring record
> even though there is (in general) no multiplication operation. We also
> don't have any locale assumption that this "ring record" is an actual
> ring (i.e. fulfils the ring axioms). Just the addition operation in it
> is required to form an abelian group.
> As for why this strange "abelian_group" locale exists, I cannot say. One
> would have to examine where it is used and what for.
> I agree that it's all very confusing. Maybe it is simply the case that
> this ad-hoc "single-inheritance record" "locale with structure
> parameters" is just fraught with problems. But as far as I know, it's
> the only way we have in Isabelle to do abstract algebra, and I don't
> know of a better one. Unless we can find a way to emulate the more
> modular typeclass/implicit parameter approach and elaborators that
> systems like Coq and Lean have.
> Manuel
> On 12/04/2019 17:01, Lawrence Paulson wrote:
>> A notable peculiarity of Algebra is its locale abelian_group, which is based on comm_group (groups with commutative multiplication) but with the weird twist of requiring a ring; it appears to be, in reality, the specification that a ring’s addition operator is commutative. Except that all rings have this property, and the very existence of this locale is confusing. Does anybody know any more about this?
>> Larry
>> record 'a ring = "'a monoid" +
>>  zero :: 'a ("𝟬ı")
>>  add :: "['a, 'a] ⇒ 'a" (infixl "⊕ı" 65)
>> abbreviation
>>  add_monoid :: "('a, 'm) ring_scheme ⇒ ('a, 'm) monoid_scheme"
>>  where "add_monoid R ≡ ⦇ carrier = carrier R, mult = add R, one = zero R, … = (undefined :: 'm) ⦈"
>> locale abelian_monoid =
>>  fixes G (structure)
>>  assumes a_comm_monoid:
>>     "comm_monoid (add_monoid G)"
>> locale abelian_group = abelian_monoid +
>>  assumes a_comm_group:
>>     "comm_group (add_monoid G)"

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