|
|
Logic for Children - Workshop at UniLog 2018 (Vichy)
Official pages (at uni-log.org):
http://www.uni-log.org/start6.html
http://www.uni-log.org/wk6-CHI.html
http://www.uni-log.org/registration6.html
The workshop will happen during the "congress" (jun 21-26), not during the "school" (jun 16-20).
This page is uglier than the official one but we can update it more easily.
Quick index:
1. First description
2. A second description
3. A video
4. Presentations
5. Keynote speakers
6. Other people / related work / resources
7. λ-calculus, type theories and proof assistants
8. Our next step: getting more submissions
9. If you would like to help us
10. On funding
11. How to contact us
1. Our first
description of what the workshop is about (from the official page):
When we explain a theorem to children - in the strict sense of
the term - we focus on concrete examples, and we avoid generalizations, abstract
structures and infinite objects.
When we present something to "children", in a wider sense of the
term that means "people without mathematical maturity", or even
"people without expertise in a certain area", we usually do
something similar: we start from a few motivating examples, and then
we generalize.
One of the aims of this workshop is to discuss techniques for particularization and generalization. Particularization is
easy; substituing variables in a general statement is often enough
to do the job. Generalization is much harder, and one way to
visualize how it works is to regard particularization as a
projection: a coil projects a circle-like shadow on the ground, and
we can ask for ways to "lift" pieces of that circle to the coil
continously. Projections lose dimensions and may collapse
things that were originally different; liftings try to
reconstruct the missing information in a sensible way. There may be
several different liftings for a certain part of the circle, or
none. Finding good generalizations is somehow like finding good
liftings.
The second of our aims is to discuss diagrams. For example,
in Category Theory statements, definitions and proofs can be often
expressed as diagrams, and if we start with a general diagram and
particularize it we get a second diagram with the same shape as the
first one, and that second diagram can be used as a version "for
children" of the general statement and proof. Diagrams were for a
long time considered second-class entities in CT literature ([2]
discusses some of the reasons), and were omitted; readers who think
very visually would feel that part of the work involved in
understanding CT papers and books would be to reconstruct the
"missing" diagrams from algebraic statements. Particular cases, even
when they were the motivation for the general definition, are also
treated as somewhat second-class - and this inspires a possible
meaning for what can call "Category Theory for Children": to start
from the diagrams for particular cases, and then "lift" them to the
general case. Note that this can be done outside Category Theory
too; [1] is a good example.
Our third aim is to discuss models. A standard example is
that every topological space is a Heyting Algebra, and so a model
for Intuitionistic Predicate Logic, and this lets us explain visually some
features of IPL. Something similar can be done for some modal and
paraconsistent logics; we believe that the figures for that should
be considered more important, and be more well-known.
References:
[1]: Jamnik, Mateja: Mathematical Reasoning with Diagrams: From Intuition to Automation.
CSLI, 2001.
[2]: Krömer, Ralf: Tool and Object: A History and Philosophy of Category Theory.
Birkhäuser, 2007.
2. A
second description of what the workshop is about (used in a call for
help):
Hi list,
we - me and Fernando Lucatelli - are trying to organize a
workshop called "Logic for Children", that will happen in the UniLog
2018 in Vichy, France, in june 21-26...
The "children" in "logic for children" means "people without
mathematical maturity", which in its turn means people who:
- have trouble with very abstract definitions,
- prefer starting from particular cases (and then generalize),
- handle diagrams better than algebraic notations,
- like to use diagrams and analogies (as in [BP2006]).
If we say that categorical definitions are "for adults" - because
they may be very abstract - and that particular cases, diagrams, and
analogies are "for children", then our intent with this workshop
becomes easy to state. "Children" are willing to use "tools for
children" to do mathematics, even if they will have to translate
everything to a language "for adults" to make their results
dependable and publishable, and even if the bridge between their
tools "for children" and "for adults" is somewhat defective, i.e.,
if the translation only works on simple cases...
We are interested in that bridge between maths "for adults"
and "for children" in several areas. Maths "for children" are hard
to publish, even informally as notes (see this thread in the
Categories mailing list), so often techniques are rediscovered over
and over, but kept restricted to the "oral culture" of the area.
Our main intents with this workshop are:
- to discuss (over coffe breaks!) the techniques of the "bridge"
that we currently use in seemingly ad-hoc ways,
- to systematize and "mechanize" these techniques to make them
quicker to apply,
- to find ways to publish those techniques - in journals or
elsewhere,
- to connect people in several areas working in related ideas,
and to create repositories of online resources.
3. I made a video advertising the workshop.
It was based on these slides - the video is here.
The UniLog youtube channel is here.
4. Presentations:
5. Keynote speakers:
- Ralf Krömer:
Category theory and its foundations: the role of diagrams and other "intuitive" material.
Abstract and
slides of his talk.
- Bob Coecke:
Quantum Theory for Kids.
Abstract and
slides of his talk.
- (Mateja Jamnik almost became a keynote, but Krömer and Coecke
confirmed first.)
6. Other people / related work / resources:
- Eduardo Ochs ("me"): the paper IDARCT
describes several tools for making versions "for children" of
mathematical concepts, and ZHAs for
children puts some of these ideas in practice. There's also this
recent draft:
A skeleton for the
proof of the Yoneda Lemma,
that describes a handful of very useful techniques
(e.g.: internal views) for obtaining the "missing diagrams" in
basic Category Theory.
- Lawvere and Schanuel's book: Conceptual Mathematics. I learned the idea of "internal views"
from it.
- "Generic Figures and Their Glueings" (PDF), by Reyes, Reyes and Zolfaghari, is a kind of follow-up to
Lawvere and Schanuel's book. Some sections of "A skeleton for the proof
of the Yoneda Lemma" are dedicated to RRZ's notation.
- Emily Riehl's "Category Theory in
Context" uses internal diagrams a bit and is one of my favorite
books on CT.
- Ronnie Brown won't be
able to come but (...) ...and he pointed to his paper Analogy and Comparison; I would love to find a way to formalize
his use of analogies.
- The Quantum Group
at Oxford. It includes Bob Coecke and Dan Marsden - see
his Category Theory Using
String Diagrams.
- Robert Seely has lots of
papers with, and about, diagrams (mainly proof nets). A good
starting point is this recent survey article: Proof
Theory of the Cut Rule.
- Mateja Jamnik's book Mathematical Reasoning with Diagrams.
- The Theory and Application
of Diagrams (biannual
conference)
- "History of
string diagrams" - a thread on the Categories mailist list,
2017may03-2017may15. Search gmail for categories
diagrams after:2017/4/19 before:2017/5/18.
- Brian Peter Ledger sent an e-mail called "Visual mnemonics for
Category Theory" to the Categories mailing list in 2017nov08.
Search gmail for categories brian peter ledger.
- A question. Most CT books have lots of elementary exercises
whose solutions consist of defining functors, NTs, etc, and doing
calculations with them and proving things. Is there a "canonical
language" for solving those exercises? I am giving a course for students with
very little mathematical background that is partly an
introduction to CT, and they almost teared all their hair off
trying to write their solutions in "standard" language... things
got much better when I convinced them to use (untyped)
lambda-calculus almost everywhere - but what do people do in
other elementary courses about CT? (Note: I asked this on the
Categories mailing list on 2017dec05 - search gmail for
categories canonical language for exercises).
- Serge Robert will give a talk on the impact of Philosophy on
children and their logical reasoning elsewhere at the UniLog.
- There's a journal called "Diagrammes", with all its issues online.
- Dominique Duval
has been working on the "lie-to-children"
idea, and she'll be at the UniLog presenting why logical rules are fractions.
7. Connections with λ-calculus, type theories and proof assistants:
- Gross, Chlipala and Spivak's Experience Implementing a Performant Category-Theory Library in
Coq (PDF) - in page 4
they explain that in their (first) implementation a category C is a record with eight fields, like this: C = (COb,
CHom, Co, C1, CAssoc, CLeftId, CRightId,
CTruncated).
- In sections 12 and 19 of IDARCT (PDF) there's a
sketch of an idea for implementing skeletons of
constructions and proofs: in the "real world" a category is a
7-uple and in the "syntactical world" it is a 4-uple; a
projection from the "real world" to the "syntactical world" drops
the last 3 fields; when we have to handle both worlds at once the
shorter structure is called a "protocategory", and we also have
protofunctors, proto-NTs, proto-adjunctions, proto-fibrations,
and so on; skeletons are these proto-things from the syntactical
world; the easy direction of the "bridge" between the real and
the syntactical world just drops some fields, and the hard
direction infers or reconstructs them.
- I never worked out the details of proto-categories,
proto-fibrations, proto-CCCs and so on beyond the level of detail
of these
seminar notes from 2010. =(
- We (Ochs/Lucatelli) are trying to get in touch with people who
work with proof assistants - it would be great to have some of
them in the workshop!
8. Our next step: getting more submissions
Note: there is still a tiny chance that the workshop
won't happen "officially" and that people would have to present their
work either on other workshops at the UniLog or at the main
conference, and meet informally... officially each workshop needs at
least 10 presenters that are neither organizers nor keynotes, so we
(Ochs/Lucatelli) are going to try a trick that Jean-Yves Beziau
suggested to us, which is to send individual e-mails to people that
can be interested in participating (he said that sending "about 100
invitations" usually works)...
If you have people to suggest please send us their names, and, if
possible, their e-mails... we work mostly on Category Theory, and we
think that this workshop could of interest to people working on, e.g.,
Education, Diagrammatic reasoning, Visualization of algorithms - and
we don't know many people in these areas yet...
9. If you
would like to help us, here are some trivial ways:
- you can send us pointers to related work,
- you can send us pointers to people that we should get in touch
with,
- you can ask to receive updates from us (that keeps our spirits
high!), and maybe contribute in the future.
And here are some less trivial ways:
- you can send us folklore ideas (without pointers),
- you can attend the workshop,
- you can submit something to the workshop. =)
10. On funding:
Some people have asked me if I can obtain some kind of funding to
support their trip to the UniLog. I've tried to ask around, but I
didn't even get any useful hints... The conference has a page listing its sponsors, and
that's all I know at this moment. Hints welcome!!! =\
11. My contacts:
eduardoochs@gmail.com
https://www.facebook.com/eduardo.ochs
(55)(21)98884-2389 (Whatsapp / Telegram)
^ If you want to propose changes to this page chat may be the best way!
|