[INCLUDE TH/speedbar.blogme]
[SETFAVICON dednat4/dednat4-icon.png]
[SETFAVICON IMAGES/forthsun.png]
[#
(defun c () (interactive) (find-blogme3-sh0-if "logic-for-children-2018"))
(defun u () (interactive) (find-blogme-upload-links "logic-for-children-2018"))
;; http://angg.twu.net/logic-for-children-2018.html
;; http://angg.twu.net/logic-for-children-2018.html#help-us
;; http://angg.twu.net/logic-for-children-2018.html#second-description
;; file:///home/edrx/TH/L/logic-for-children-2018.html
;; file:///home/edrx/TH/L/logic-for-children-2018.html#second-description
;; (find-blogme3 "anggdefs.lua" "sec")
;; From:
;; (find-TH "math-b")
;;
(defun bsec (tag h head) (insert (bsec0 tag h head)))
(defun bsec0 (tag h head)
(ee-template0 "
[#
# «.{tag}»\t\t(to \"{tag}\")
# {(ee-S `(bsec ,tag ,h ,head))}
#]
[sec «{tag}» (to \".{tag}\")
{h} {head}]
"))
#]
[lua:
-- (find-blogme3 "anggdefs.lua" "cgiquote")
cgiquote2 = function (str) return (cgiquote(str):gsub("/", "%%2f")) end
def [[ GMAILSEARCH 1 query
R("https://mail.google.com/mail/ca/u/0/#search/"..cgiquote2(query),
query) ]]
def [[ λ 1 _ "λ" ]]
def [[ ö 1 _ "ö" ]]
def [[ ä 1 _ "ä" ]]
def [[ CF 1 text BF("C")..""..text.."" ]]
-- (find-blogme3 "anggdefs.lua" "WITHINDEX")
-- (find-blogme3 "anggdefs.lua" "WITHINDEX" "ANCHOR_I")
def [[ isec 4 n,tag,indextext,bodytext
pushindex(
ANCHOR_I(tag, n..". "..indextext),
ANCHOR_S(tag, n..". "..bodytext))
]]
def [[ INDEX0 1 _ table.concat(secindex, "\n"..BR()) ]]
def [[ INDEX 1 _ _B.P("Quick index:"..BR()..INDEX0()) ]]
]
[htmlize [J Logic for Children - Workshop at UniLog 2018 (Vichy)]
[P Official pages (at uni-log.org):
[BR] [R http://www.uni-log.org/start6.html]
[BR] [R http://www.uni-log.org/wk6-CHI.html]
[# Was: http://www.uni-log.org/wk6-logic-for-children.html]
[BR] [R http://www.uni-log.org/registration6.html] [# (cheaper before Dec.1)]
[BR] The workshop will happen during the "congress" (jun 21-26), not during the "school" (jun 16-20).
]
[P This page is uglier than the [R http://www.uni-log.org/wk6-CHI.html
official one] but we can update it more easily.]
[# [BR] We will use it for information that is mostly for the speakers.]
[WITHINDEX
[br]
[P [BF [isec [++N] first-description [J First description] Our first
description of what the workshop is about]] (from the [R
http://www.uni-log.org/wk6-CHI.html official page]):]
[NARROW
[P When we explain a theorem to children - in the strict sense of
the term - we [R http://angg.twu.net/LATEX/2017planar-has-1.pdf
focus on concrete examples], and we avoid generalizations, abstract
structures and infinite objects.]
[P 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.]
[P One of the aims of this workshop is to discuss techniques for [IT
particularization] and [IT 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. [IT Projections] lose dimensions and may collapse
things that were originally different; [IT [R
http://angg.twu.net/LATEX/idarct-preprint.pdf 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.]
[P The second of our aims is to discuss [IT 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.]
[P Our third aim is to discuss [IT 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 [R
http://angg.twu.net/LATEX/2017planar-has-1.pdf 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.]
[P References:]
[P [' [1]]: [R http://www.cl.cam.ac.uk/~mj201/ Jamnik, Mateja]: [R
https://www.amazon.com/Mathematical-Reasoning-Diagrams-Lecture-Notes/dp/1575863243
Mathematical Reasoning with Diagrams: From Intuition to Automation].
CSLI, 2001.]
[P [' [2]]: [R http://www2.math.uni-wuppertal.de/~kroemer/index.html
Kr[ö]mer, Ralf]: [R
https://www.amazon.com/Tool-Object-Philosophy-Networks-Historical/dp/376437523X/
Tool and Object: A History and Philosophy of Category Theory].
Birkh[ä]user, 2007.]
]
[br]
[P [BF [isec [++N] second-description [J A second description] A
second description of what the workshop is about]] (used in a call for
help):]
[NARROW
[P Hi list,]
[P 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...]
[P The "children" in "logic for children" means "people without
mathematical maturity", which in its turn means people who:]
[LIST3
[J have trouble with very abstract definitions,]
[J prefer starting from particular cases (and then generalize),]
[J handle diagrams better than algebraic notations,]
[J like to use diagrams and analogies (as in [R
https://groupoids.org.uk/pdffiles/Analogy-and-Comparison.pdf ['
[BP2006]]]).]
]
[P 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...]
[P We are interested in that [IT bridge] between maths "for adults"
and "for children" in several areas. Maths "for children" are hard
to publish, even informally as notes (see [R
http://angg.twu.net/categories-2017may02.html 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.]
[# P Our main intent with this workshop are to discuss - over
innumerous coffe breaks - the techniques of the "bridge" that we
currently use in a seemingly ad-hoc way, and systematize and sort of
"mechanize" them to make them quicker to apply in the future, and
(create archives, map resources in the literature).]
[P Our main intents with this workshop are:]
[LIST3
[J to discuss (over coffe breaks!) the techniques of the "bridge"
that we currently use in seemingly ad-hoc ways,]
[J to systematize and "mechanize" these techniques to make them
quicker to apply,]
[J to find ways to publish those techniques - in journals or
elsewhere,]
[J to connect people in several areas working in related ideas,
and to create repositories of online resources.]
]
]
[br]
[P [BF [isec [++N] video [J A video] I made a video advertising the workshop.]]
[BR] It was based on [R http://angg.twu.net/LATEX/2018vichy-video.pdf
these slides] - the video is [R
https://www.youtube.com/watch?v=v2QGtteAqUk&t=5s here].
[BR] The UniLog youtube channel is [R
https://www.youtube.com/channel/UCW9jSSry0zoYz-FdREK5-Uw here].]
[br]
[HLIST3 [BF [isec [++N] presentations Presentations Presentations:]]
[J [R http://www.lanci.uqam.ca/index.php/membres-2/anne-brel-cloutier/ Anne Brel Cloutier]:
[R http://angg.twu.net/logic-for-children-2018/anne_cloutier.pdf
Community of Philosophical Inquiry: Fostering the development
of logical reasoning through metalogical understanding.]
]
[J [R http://www.ms.lt/sodas/Book/Book Andrius Kulikauskas]:
[R http://angg.twu.net/logic-for-children-2018/andrius_kulikauskas.pdf
Visualization as Restructuring and thus a Source of Logical Paradox]
]
[J [R https://arxiv.org/find/math/1/au:+Liberti_I/0/1/0/all/0/1 Ivan di Liberti]:
[R http://angg.twu.net/logic-for-children-2018/ivan_di_liberti.pdf
On the concreteness of certain categories]
]
[J [R http://www.ime.unicamp.br/~laurarifo/research.html Laura Rifo]:
[R http://angg.twu.net/logic-for-children-2018/laura_rifo.pdf
Subjectivism and inferential reasoning on teaching practice]
]
[J [R http://angg.twu.net/math-b.html Eduardo Ochs]:
[R http://angg.twu.net/logic-for-children-2018/eduardo_ochs.pdf
Visualizing Geometric Morphisms]
]
[J [R https://arxiv.org/find/math/1/au:+Nunes_F/0/1/0/all/0/1 Fernando Lucatelli Nunes]:
[R http://angg.twu.net/logic-for-children-2018/fernando_lucatelli.pdf
Elementary introduction to pasting]
]
]
[br]
[HLIST3 [BF [isec [++N] keynotes [J Keynote speakers] Keynote speakers:]]
[J [R http://www2.math.uni-wuppertal.de/~kroemer/index.html Ralf Kr[ö]mer]:
Category theory and its foundations: the role of diagrams and other "intuitive" material.
[BR]
[R http://angg.twu.net/logic-for-children-2018/ralf_kroemer.pdf Abstract] and
[R http://angg.twu.net/logic-for-children-2018/ralf_kroemer__slides.pdf slides] of his talk.]
[J [R http://www.cs.ox.ac.uk/people/bob.coecke/ Bob Coecke]:
Quantum Theory for Kids.
[BR]
[R http://angg.twu.net/logic-for-children-2018/bob_coecke.pdf Abstract] and
[R http://angg.twu.net/logic-for-children-2018/bob_coecke__slides.pdf slides] of his talk.]
[J (Mateja Jamnik almost became a keynote, but Kr[ö]mer and Coecke
confirmed first.)]
]
[br]
[HLIST3
[BF [NAME resources]
[isec [++N] other-people-and-related-work
[J Other people / related work / resources]
Other people / related work / resources:]]
[J Eduardo Ochs ("me"): the paper [R
http://angg.twu.net/math-b.html#internal-diags-in-ct IDARCT]
describes several tools for making versions "for children" of
mathematical concepts, and [R
http://angg.twu.net/math-b.html#zhas-for-children-2 ZHAs for
children] puts some of these ideas in practice. There's also this
recent draft:
[R http://angg.twu.net/LATEX/2017yoneda.pdf A skeleton for the
proof of the Yoneda Lemma],
that describes a handful of [COLOR red very useful] techniques
(e.g.: internal views) for obtaining the "missing diagrams" in
basic Category Theory.]
[J Lawvere and Schanuel's book: [R
https://www.amazon.com/Conceptual-Mathematics-First-Introduction-Categories-dp-052171916X/dp/052171916X/
Conceptual Mathematics]. I learned the idea of "internal views"
from it.]
[J "[R
https://reyes-reyes.com/2004/06/01/generic-figures-and-their-glueings-a-constructive-approach-to-functor-categories/
Generic Figures and Their Glueings]" ([R
https://marieetgonzalo.files.wordpress.com/2004/06/generic-figures.pdf
PDF]), by Reyes, Reyes and Zolfaghari, is a kind of follow-up to
Lawvere and Schanuel's book. Some sections of "[R
http://angg.twu.net/LATEX/2017yoneda.pdf A skeleton for the proof
of the Yoneda Lemma]" are dedicated to RRZ's notation.]
[J [R http://www.math.jhu.edu/~eriehl/ Emily Riehl]'s "[R
http://www.math.jhu.edu/~eriehl/context.pdf Category Theory in
Context]" uses internal diagrams a bit and is one of my favorite
books on CT.]
[J [R https://groupoids.org.uk/publar.html Ronnie Brown] won't be
able to come but (...) ...and he pointed to his paper [R
https://groupoids.org.uk/pdffiles/Analogy-and-Comparison.pdf
Analogy and Comparison]; I would love to find a way to formalize
his use of analogies.]
[J The [R http://www.cs.ox.ac.uk/activities/quantum/ Quantum Group]
at Oxford. It includes Bob Coecke and [R
https://www.cs.ox.ac.uk/people/dan.marsden/ Dan Marsden] - see
his [R https://arxiv.org/abs/1401.7220 Category Theory Using
String Diagrams].]
[J [R http://www.math.mcgill.ca/rags/ Robert Seely] has lots of
papers with, and about, diagrams (mainly proof nets). A good
starting point is this recent survey article: [R
http://www.math.mcgill.ca/rags/misc/proof_theory-essay.pdf Proof
Theory of the Cut Rule].]
[J [R http://www.cl.cam.ac.uk/~mj201/ Mateja Jamnik]'s book [R
https://www.amazon.com/Mathematical-Reasoning-Diagrams-Lecture-Notes/dp/1575863243
Mathematical Reasoning with Diagrams]].
[J [R http://www.diagrams-conference.org/ The Theory and Application
of Diagrams] ([R
http://www.diagrams-conference.org/previous-conferences biannual]
conference)]
[J "[R http://angg.twu.net/categories-2017may02.html History of
string diagrams]" - a thread on the Categories mailist list,
2017may03-2017may15. Search gmail for [GMAILSEARCH categories
diagrams after:2017/4/19 before:2017/5/18].]
[J Brian Peter Ledger sent an e-mail called "Visual mnemonics for
Category Theory" to the Categories mailing list in 2017nov08.
Search gmail for [GMAILSEARCH categories brian peter ledger].]
[J [IT 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 [R
http://angg.twu.net/math-b.html#lclt course] for students with
very little mathematical background that is [IT 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 - [IT 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
[GMAILSEARCH categories canonical language for exercises]).]
[J [R
http://www.er.uqam.ca/nobel/philuqam/dept/textes/CV_SR_english.pdf
Serge Robert] will give a talk on the impact of Philosophy on
children and their logical reasoning elsewhere at the UniLog.]
[J There's a journal called "[R http://www.numdam.org/journals/DIA
Diagrammes]", with all its issues online.]
[J [R https://ljk.imag.fr/membres/Dominique.Duval/ Dominique Duval]
has been working on the "[R
https://en.wikipedia.org/wiki/Lie-to-children lie-to-children]"
idea, and she'll be at the UniLog presenting [R
https://ljk.imag.fr/membres/Dominique.Duval/Research/dialog.html
why logical rules are fractions].]
]
[br]
[HLIST3
[BF [isec [++N] lambda
[J [λ]-calculus, type theories and proof assistants]
Connections with [λ]-calculus, type theories and proof assistants:]]
[J Gross, Chlipala and Spivak's [R https://arxiv.org/abs/1401.7694
Experience Implementing a Performant Category-Theory Library in
Coq] ([R https://arxiv.org/pdf/1401.7694.pdf PDF]) - in page 4
they explain that in their (first) implementation a category [BF
C] is a record with eight fields, like this: [BF C] = ([CF Ob],
[CF Hom], [CF o], [CF 1], [CF Assoc], [CF LeftId], [CF RightId],
[CF Truncated]).]
[J In sections 12 and 19 of [R
http://angg.twu.net/math-b.html#internal-diags-in-ct IDARCT] ([R
http://angg.twu.net/LATEX/idarct-preprint.pdf PDF]) there's a
sketch of an idea for [COLOR red 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.]
[J I never worked out the details of proto-categories,
proto-fibrations, proto-CCCs and so on beyond the level of detail
of [R http://angg.twu.net/LATEX/2010unilog-2010jun21.pdf these
seminar notes] from 2010. =(]
[J 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!]
]
[#
[BR] [R #getting-more-submissions Our next step: getting more submissions],
[BR] [R #help-us If you would like to help us],
[BR] [R #funding On funding],
[BR] [R #contact How to contact us].
]
[br]
[P [BF [isec [++N] getting-more-submissions
[J Our next step: getting more submissions]
Our next step: getting more submissions]]]
[P Note: there is still a [COLOR red 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)...]
[P 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 [IT yet]...]
[br]
[P [BF [isec [++N] help-us [J If you would like to help us] If you
would like to help us]], here are some trivial ways:]
[LIST3
[J you can send us pointers to related work,]
[J you can send us pointers to people that we should get in touch
with,]
[J you can ask to receive updates from us (that keeps our spirits
high!), and maybe contribute in the future.]
]
[P And here are some less trivial ways:]
[LIST3
[J you can send us [R https://ncatlab.org/nlab/show/folklore
folklore] ideas (without pointers),]
[J you can attend the workshop,]
[J you can submit something to the workshop. =)]
]
[br]
[P [BF [isec [++N] funding [J On funding] On funding:]]]
[P 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 [R
http://www.uni-log.org/sponsors6.html page listing its sponsors], and
that's all I know at this moment. Hints welcome!!! =\]
[br]
[P [BF [isec [++N] contact [J How to contact us] My contacts:]]
[BR] [MAILTO eduardoochs@gmail.com]
[BR] [R https://www.facebook.com/eduardo.ochs]
[BR] (55)(21)98884-2389 (Whatsapp / Telegram)
[BR] ^ If you want to propose changes to this page chat may be the best way!
]
]
[#
People who would like to receive updates:
https://mail.google.com/mail/ca/u/0/#inbox/161ad2566f7a09dd Alexander Kurz
#]
[#
"Ivan Di Liberti" ,
"Anne Brel Cloutier" ,
"Laura Leticia Ramos Rifo" ,
"Ivan Di Liberti" ,
"Fernando Lucatelli Nunes" ,
Laura:
https://mail.google.com/mail/ca/u/0/#inbox/15fcbe41c1a09334
Andrius:
https://mail.google.com/mail/ca/u/0/#search/andrius/15f795a5520deeab abstract
https://mail.google.com/mail/ca/u/0/#search/andrius/15fbc1d8839846ea retraction
Anne:
https://mail.google.com/mail/ca/u/0/#search/brel/15eee4f1ed11e4a7
Ivan:
https://mail.google.com/mail/ca/u/0/#search/ivan/15ec96921f6cf3e8
Ronnie:
https://math.stackexchange.com/questions/182665/getting-students-to-not-fear-confusion/182912#182912
https://mail.google.com/mail/ca/u/0/#search/brown/1602c8e114f5d4c2 canonical language
https://mail.google.com/mail/ca/u/0/#search/brown/15eb448f82ad2e79 workshop CFP 1
Dana:
https://mail.google.com/mail/ca/u/0/#search/dana+scott/1602c39839091675
# (find-TH "categories-2017may02")
#]
]
[#
# Local Variables:
# modes: (fundamental-mode blogme-mode)
# End:
#]