Email Gateway (Aug 23 2022 at 09:21): Email Gateway (Aug 23 2022 at 09:21):From: "Dr. Brendan Patrick Mahony" <mahonybp@tpg.com.au>
Isabelle’s mathematical structuring facilities, classes and locales, have well known scopes that preclude some otherwise attractive modelling approaches.
For example, the AFP has three approaches to category theory that model a category’s carrier classes of objects and arrows as types.
https://www.isa-afp.org/browser_info/current/AFP/Category/document.pdf <https://www.isa-afp.org/browser_info/current/AFP/Category/document.pdf>
https://www.isa-afp.org/entries/Category2.html <https://www.isa-afp.org/entries/Category2.html>
https://www.isa-afp.org/entries/Category3.html
Besides the pure mathematical constraints this places of the classes of category instances (much of which is I guess inherent to the use of HOL), this also brings a degree of applied mathematical pain in that it would frequently be convenient in a practical reasoning sense to model objects and arrows as classes of types, so as to make use of a type overloaded arrow composition operator and enjoy all the reasoning safety benefits of HOL strong typing.
This can of course be done for any desired category, some examples
Set:
class cat_obj = small
typedef
('a, 'b) cat_arrow = "{ f :: ('a::cat_obj) ⇒ ('b::cat_obj). True}"
by (auto)
definition
cat_compose :: "('a::cat_obj, 'b::cat_obj) cat_arrow ⇒ ('b, 'c::cat_obj) cat_arrow ⇒ ('a, 'c) cat_arrow"
where
"cat_compose f g = Abs_cat_arrow ((Rep_cat_arrow g) ∘ (Rep_cat_arrow f))"
definition
cat_id :: "('a::cat_obj, 'a) cat_arrow"
where
"cat_id = Abs_cat_arrow id"
lemma cat_left_id:
"cat_compose cat_id a = a"
by (auto simp add: cat_compose_def cat_id_def Abs_cat_arrow_inverse Rep_cat_arrow_inverse)
lemma cat_right_id:
"cat_compose a cat_id = a"
by (auto simp add: cat_compose_def cat_id_def Abs_cat_arrow_inverse Rep_cat_arrow_inverse)
lemma cat_comp_assoc:
"cat_compose (cat_compose a b) c = cat_compose a (cat_compose b c)"
by (auto simp add: cat_compose_def cat_id_def Abs_cat_arrow_inverse Rep_cat_arrow_inverse comp_assoc)
Grp:
class cat_obj = group_add
typedef (overloaded)
('a, 'b) cat_arrow = "{ f :: ('a::cat_obj) ⇒ ('b::cat_obj). (∀ a b. f (a + b) = f a + f b) }"
apply (rule_tac x = "(λ a. 0)" in exI)
apply (auto)
done
definition
cat_compose :: "('a::cat_obj, 'b::cat_obj) cat_arrow ⇒ ('b, 'c::cat_obj) cat_arrow ⇒ ('a, 'c) cat_arrow"
where
"cat_compose f g = Abs_cat_arrow ((Rep_cat_arrow g) ∘ (Rep_cat_arrow f))"
lemma cat_compose_wf:
assumes
a1: "f ∈ { f :: ('b::cat_obj) ⇒ ('c::cat_obj). (∀ a b. f (a + b) = f a + f b) }" and
a2: "g ∈ { f :: ('a::cat_obj) ⇒ ('b::cat_obj). (∀ a b. f (a + b) = f a + f b) }"
shows
"f ∘ g ∈ { f :: ('a::cat_obj) ⇒ ('c::cat_obj). (∀ a b. f (a + b) = f a + f b) }"
using assms
by (auto)
definition
cat_id :: "('a::cat_obj, 'a) cat_arrow"
where
"cat_id = Abs_cat_arrow id"
lemma cat_left_id:
"cat_compose cat_id a = a"
by (auto simp add: cat_compose_def cat_id_def Abs_cat_arrow_inverse Rep_cat_arrow_inverse)
lemma cat_right_id:
"cat_compose a cat_id = a"
by (auto simp add: cat_compose_def cat_id_def Abs_cat_arrow_inverse Rep_cat_arrow_inverse)
lemma cat_comp_assoc:
"cat_compose (cat_compose a b) c = cat_compose a (cat_compose b c)"
by (auto simp add: cat_compose_def cat_id_def Rep_cat_arrow_inverse comp_assoc
Abs_cat_arrow_inverse [OF cat_compose_wf [OF Rep_cat_arrow Rep_cat_arrow]])
This is nice for “using" these categories in modelling efforts, but not so nice for doing category “theory” and in particular developing a class of category operators and associated properties that are shared by all by all instances. You know, the sort of instancing power offered by classes and locales.
My naive solution is to define an axiomatised “signature” theory for category theory and do all the abstract (repeatable) reasoning there.
theory Category_Sig
imports
Main
begin
class
cat_obj
typedecl
('a, 'b) cat_arrow
consts
cat_compose :: "('a::cat_obj, 'b::cat_obj) cat_arrow ⇒ ('b, 'c::cat_obj) cat_arrow ⇒ ('a, 'c) cat_arrow"
consts
cat_id :: "('a::cat_obj, 'a) cat_arrow"
axiomatization where
cat_left_id: "cat_compose cat_id a = a" and
cat_right_id: "cat_compose a cat_id = a" and
cat_comp_assoc: "cat_compose (cat_compose a b) c = cat_compose a (cat_compose b c)"
context
begin
notation
cat_compose (infixr "∘⇩♭" 55)
notation
cat_id ("ι⇩♭")
qualified lemma inv_uniq:
assumes
a1: "f ∘⇩♭ g = cat_id" and
a2: "h ∘⇩♭ f = cat_id"
shows
"g = h"
proof -
have
"g = ι⇩♭ ∘⇩♭ g"
by (rule cat_left_id [symmetric])
also have "…
= (h ∘⇩♭ f) ∘⇩♭ g"
by (simp add: a2)
also have "…
= h ∘⇩♭ (f ∘⇩♭ g)"
by (simp add: cat_comp_assoc)
also have "…
= h ∘⇩♭ ι⇩♭"
by (simp add: a1)
also have "…
= h"
by (rule cat_right_id)
finally show
"g = h"
by (this)
qed
end
end
Then I can use textual replacement to make copies of the signature theory and "drop in” the appropriate definitions to replace the axiomatisations, global replace the \<flat> subscript, etc … to get the desired instance theories.
Any pointers to more sophisticated approaches? (Should note that categories are not my actual algebraic target here, just a convenient and easily understood example)
It seems to suggest to me that it would be nice to have a theory “functor” facility analogous to the structure “functor" facility of standard ML.
Does anyone have any pointers to (Isabelle) work in this direction?
I noted with interest an MMT/LF paper in the recent LFMTP workshop that seemed to be suggesting something similar, but I think a bit more general
@inproceedings{Roux:2020a,
Author = {Navid Roux and Florian Rabe},
Booktitle = {Logical Frameworks and Meta Languages: Theory and Practice},
Title = {Diagram Operators in a Logical Framework},
Year = {2020}}
Email Gateway (Aug 23 2022 at 09:22):From: Mikhail Chekhov <mikhail.chekhov.w@gmail.com>
Dear Brendan Patrick Mahony/All,
I would like to make a side remark for your question.
At one point, I did think about developing an infrastructure for the
definition of generic 'meta-theories' by using implicit quantification over
types modelled via the use of the schematic type variables (see
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2019-September/msg00095.html
and,
more importantly, the reply). For this to work, one would need to write
Isabelle/ML infrastructure that can generate an 'instance' of (for example)
category theory on demand for a given set of constants like group,
group_hom, etc. This is certainly possible (see the screenshot and please
ignore all aspects not directly related to the software infrastructure that
the screenshot is meant to demonstrate), but, for me, the amount of effort
required seemed to be unsurmountable. The advantage of this approach is
that it does not require any new axioms to be added to Isabelle/HOL.
Since then, I have converged on the idea that it is best to use an
extension of HOL (e.g. ZFC in HOL or HOTG) and allow the 'meta-theory' and
the 'object-theory' to coexist using only the standard techniques. In the
context of such extensions, this means that the 'object-theory' will be
limited to some reasonably small set (e.g. V(ω+ω)). Of course, once such
theory is developed, one might be able to develop an infrastructure for the
translation of concepts across isomorphisms, under the limitation of size
only (I am not certain how easy and well automated this could become). I
have been doing some work in this direction for a certain time. The
foundational part of my development is available here:
https://gitlab.com/user9716869/czh_foundations (more applied concepts are
still in a very transient state and not available publicly). However, most
likely, this work will be superseded by HOTG that is being developed by
Alexander Krauss, Kevin Kappelmann and Joshua Chen (see
https://bitbucket.org/cezaryka/tyset/src).
Kind Regards,
Mikhail Chekhov
MCATS.png
Email Gateway (Aug 23 2022 at 09:22):From: Mikhail Chekhov <mikhail.chekhov.w@gmail.com>
Dear All,
I forgot to provide references for my previous post in this thread. It was
not my intention to put an emphasis on the references, as they contain
well-known foundational material, but I do feel awkward for omitting them
from my post and feel the need to correct this.
Last updated: Nov 21 2024 at 12:39 UTC