-
Notifications
You must be signed in to change notification settings - Fork 2
/
Copy pathDialCalculations
94 lines (51 loc) · 4.06 KB
/
DialCalculations
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
I want to list some problems that are small, but I think could lead to more interesting stuff, related to the dialectica constructions in my
phd thesis: "The Dialectica Categories", TR213 from Cambridge, https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-213.pdf, 1990.
(the thesis was submitted in 1988, examined in Jan 1989, corrections accepted in 1990)
There is an attempt at a "project" in ResearchGate https://www.researchgate.net/project/Dialectica-Categories-Applications,
but it is getting unwieldy.
I am trying to understand the connection between polynomials (in Category Theory) and the Dialectica construction.
Martin Hyland has some slides in https://www.dpmms.cam.ac.uk/~martin/Research/Slides/venice13.pdf about the relationship between type theory and dialectica.
(my own work has been on propositional and more recently first-order versions of the dialectica construction,
the connections between polynomials happen for dependent types versions of Dialectica, the doctoral work of Moss 2018 and van Glehn 2016)
Seam Moss gave a very clear talk about it in the second Polynomials workshop:
https://www.youtube.com/watch?v=tw08TmO0RRo&t=7190s
https://topos.site/p-func-workshop/slides/Moss.pdf
but there is more t say abut these cnnections, I believe.
Dialectica categories exist in two shapes (Dial and GDial--the simplified form that has morphisms like Chu spaces).
They also exist both in subobject form or as maps into a lineale L. These variations should give us at least 4 types.
but I only discussed 2 of them: Dial with subobjects, GDial with a lineale.
1. Can we check that Dial with a lineale and GDial with subjects work too?
===================================================================
A. Problems related to Lenses/Containers:
Bruno Gavranovic talked about how Lenses and Optics differe operationally
https://www.brunogavranovic.com/
DBLP https://dblp.org/pid/245/2917.html
Intercat talk: https://www.youtube.com/watch?v=3NdYughK68Y
Blog post:
https://www.youtube.com/watch?v=1NHBexWYgkU
Bruno on machine learning and Optics
https://www.youtube.com/watch?v=1NHBexWYgkU
Bruno also produced a bibliography of what he thinks one should read if interested in lenses:
https://github.com/bgavran/Lens_Resources
2. question: Using the definition of lenses in Bruno's talk, it seems we could do a Dialectica Lens category, by adding a relation to Bruno's objects.
Would this be useful? if so, for which applications?
=====================================================================
B. Problems with Games:
Jeremie Koenig gave a talk at ACL2021 which I thought was very insightful
https://www.youtube.com/watch?v=10u7hbEYcCk&t=3800s
slides: https://www.cl.cam.ac.uk/events/act2021/slides/ACT_2021_slides_71.pdf
his ACT paper: https://www.cl.cam.ac.uk/events/act2021/papers/ACT_2021_paper_71.pdf
Glynn Winskel gave a talk at the Topos Colloquium
https://www.youtube.com/watch?v=ywHNG6DYAGg
his paper https://blogs.ed.ac.uk/he-lab/2022/03/14/new-paper-making-concurrency-functional/
My own super games preprint https://drive.google.com/file/d/19wSFHBNdb-PQj2ZjM6oZtV6MVutpGIdn/view?usp=sharing
==========================================================================
C. Implementations of Dialectica:
Implementations can help us consolidate intuitions and also help us note where intuitions are a bit "shaky".
There is an implementation of Dialectica categories, coded in Agda by Harley Eades III, for the purpose of proving
cut-elimination for FILL (Full Intuitionistic Linear Logic). This is in https://github.com/heades/cut-fill-agda.
(see https://github.com/bond15/Dialectica for a newer Cubical Agda version that is under development)
There is also an old implementation of Chu Spaces Live (in Java) at http://boole.stanford.edu/live/ which Vaughan Pratt mantains
Eric Bond has an implementation of polynomials here https://github.com/bond15/Polynomials-Categorically
and is implementing Dialectica categories here https://github.com/bond15/Dialectica.
It would be nice to have something calculating Dialectica spaces in CatLab, to improve synergy with J. Baez project.