Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] ML style "functors" for Isabelle theories?


view this post on Zulip Email Gateway (Jul 20 2020 at 06:17):

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}}

view this post on Zulip Email Gateway (Jul 21 2020 at 20:27):

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

view this post on Zulip Email Gateway (Jul 21 2020 at 22:37):

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: Dec 05 2021 at 23:19 UTC