Warning: this is an htmlized version!
The original is across this link,
and the conversion rules are here.
% (setenv "TEXINPUTS" "~/LATEX:")
% (setenv "TEXINPUTS" nil)
% (defun c () (interactive) (find-LATEXsh "run-latex 'stem=2014sfc-slides;pla'"))
% (defun c () (interactive) (find-LATEXsh "run-latex 'stem=2014sfc-slides;d4;pla'"))
% (defun d () (interactive) (find-xpdfpage "~/LATEX/2014sfc-slides.pdf"))
% (defun fra () (interactive) (insert "\n% <>\n%\n\\begin{frame}\n\\frametitle{}\n\\end{frame}\n"))

% http://angg.twu.net/LATEX/2014sfc-slides.pdf

% (find-pen-links)
% (find-sh0 "cp -v 2014sfc-slides.pdf /tmp/pen/ebl2014-ochs.pdf")

% «.title-page»				(to "title-page")
% «.where-sheaves-stand»		(to "where-sheaves-stand")
% «.CT-why»				(to "CT-why")
% «.CT-why-now» 			(to "CT-why-now")
% «.CT-should-be»			(to "CT-should-be")
% «.CT-lambda-calculus»			(to "CT-lambda-calculus")
% «.ZSets»				(to "ZSets")
% «.ZDAGs»				(to "ZDAGs")
% «.truth-values»			(to "truth-values")
% «.intuitionistic-truth-values»	(to "intuitionistic-truth-values")
% «.the-order-topology»			(to "the-order-topology")
% «.priming»				(to "priming")
% «.unpriming»				(to "unpriming")
% «.priming-theorems»			(to "priming-theorems")
% «.glueing-functions»			(to "glueing-functions")
% «.sheafness»				(to "sheafness")
% «.topological-sheafness»		(to "topological-sheafness")
% «.the-evil-presheaf»			(to "the-evil-presheaf")
% «.dual-operations»			(to "dual-operations")
% «.where-are-the-theorems»		(to "where-are-the-theorems")
% «.closure-and-ess»			(to "closure-and-ess")

% (find-LATEX "README")
% (find-dn4file ".files.sh" "cptexinputs")
% (find-sh "pwd; ~/dednat4/.files.sh -n rmtexinputs")
% (find-sh "pwd; ~/dednat4/.files.sh -n cptexinputs")
% (find-sh "pwd; ~/dednat4/.files.sh    rmtexinputs")
% (find-sh "pwd; ~/dednat4/.files.sh    cptexinputs")

% (find-BEAMERfile "foo-ornate.tex")
% (find-BEAMERfile "foo.tex")

% (find-node "(kpathsea)Index" "TEXINPUTS")
% (find-es "tex" "TEXINPUTS")

% (find-LATEXfile "" "edrx08.sty")

% \usepackage[colorlinks]{hyperref} % (find-es "tex" "hyperref")
\usepackage{etex}   % (find-es "tex" "no-room-for-a-new-dimen")
  % \usetheme{Warsaw}
  % or whatever (possibly just delete it)


\input 2011ebl-defs.tex
% (find-LATEX "2011ebl-abs.tex" "priming")
%L process "edrx08.sty"  -- (find-dn4ex "edrx08.sty")

\input 2014sfc-slides.dnt


% (find-beamerugpage 73 "\\setbeamertemplate{navigation symbols}{}")
% (find-beamerugtext 73 "\\setbeamertemplate{navigation symbols}{}")
\setbeamertemplate{navigation symbols}{}

% «title-page» (to ".title-page")
\title{Sheaves for Children}
\author{Eduardo Ochs}
  Departmento de Física e Matemática\\
  Pólo Universitário de Rio das Ostras\\
  % \footnotesize
  \url{http://angg.twu.net/math-b.html} \\
  \url{http://angg.twu.net/ferramentas-para-ativistas.html} \\
  \tiny \phantom{a}
  {\color{gray}(Version: 2014apr09)} \\
\date{EBL 2014}


% «where-sheaves-stand» (to ".where-sheaves-stand")
\frametitle{Where sheaves stand}
  |                    |
  |  Category Theory   |    Cartesian Closed Categories,
  |  ________________  |        Lambda-Calculus,           
  | |                | |      Intuitionistic Logic         
  | |  Topos Theory  | |        
  | |  ____________  | |      
  | | |            | | |        Modal Logic (S4)
  | | |   Sheaves  | | |
  | | |____________| | |          Topology
  | |________________| |        
  |____________________|      Algebraic Geometry

% «CT-why» (to ".CT-why")
\frametitle{CT: Why?}
\par Category Theory is fascinating (for some people!),
\par but (usually) too abstract...
\par The right level of abstraction
\par makes lots of proofs {\it almost} automatic:
\par {\it proving} something in CT means
\par {\it constructing} something (CT is constructive!), and
\par all ``natural'' constructions are equivalent (``coherence'').
\par More or less like this:
  \par Let A and B be (arbitrary) sets.
  \par Then there is an ``obvious'' function $\text{flip}: A×B \to B×A$.
% \msk
\par This {\sl ought} to make some parts of CT {\sl easy}!!!
\par (Long story... see ``Internal Diagrams and Archetypal Reasoning
in Category Theory'')


% «CT-why-now»	(to ".CT-why-now")
\frametitle{Why study CT {\sl now}?}
\par Public education in Brazil is being dismantled -
\par maybe we should be doing better things than studying
\par very technical \& inaccessible subjects
\par with no research grants -

% «CT-should-be» (to ".CT-should-be")
\frametitle{Category theory should be more accessible}
\par Most texts about CT are for specialists in research universities...
\par {\sl Category theory should be more accessible.}
\par To whom?...
\item Non-specialists (in research universities)
\item Grad students (in research universities)
\item Undergrads (in research universities)
\item Non-specialists (in conferences - where we have to be quick)
\item Undergrads (e.g., in CompSci - in teaching colleges) - (``Children'')

% «ZSets» (to ".ZSets")
\par Take a finite, non-empty subset of $\N^2$;
\par translate it lowerleftwards as most as possible in $\N^2$,
\par until you get something that touches both axes.
\par Subsets of $\N^2$ obtained in this way are said to be
\par ``well-positioned'', and we call them {\sl ZSets}.
\par We can use a positional notation with bullets
\par to denote our favourite ZSets (unambiguously!)...

\begin{tabular}{|l|l|c|l|}            \hline
% Lambda & $\dagLambda***$ & \\ \hline
  $V$ & Vee    & $\dagVee***$    & $\{(0,1),\, (2,1),\, (1,0)\}$ \\ \hline
  $K$ & Kite   & $\dagKite*****$ & $\{(1,3),\, (0,2),\, (2,2),\, (1,1),\, (1,0)\}$ \\ \hline              
  $H$ & House  & $\dagHouse*****$ & $\{(1,2),\, (0,2),\, (2,2),\, (0,1),\, (2,1)\}$ \\ \hline

\par $\uparrow$ Some of my favorite ZSets -
\par note that they have both short, one-letter names
\par and long, pronounceable names.


% «ZDAGs» (to ".ZDAGs")
\par An arrow between points of $\N^2$ that goes one unit down
\par and 0/1/-1 units horizontally is called a {\sl black pawn's move}.
\par Take a ZSet, $D$, and draw all possible black pawns moves
\par between its points; this gives us a set of arrows, $\BPM(D)$,
\par that turns $D$, a ZSet, into a directed, acyclical, graph, $\bbD$,
\par in a canonical way: $\bbD = (D, \BPM(D)).$
\par Note the change of font!!!: \quad $D \dashrightarrow \bbD$
%Notation (note the change of font):
%  D is a ZSet,
%  bbD = (D, BPM(D)) is a _ZDAG_.



  K \;\; = \;\; \dagKite***** \;\; = \quad
   \bigKite {(1,3)} {(0,2)\ph} {\ph(2,2)} {(0,1)} {(0,0)}
  \bbK \;\; = \quad
  \bigKite {(1,3)} {(0,2)\ph} {\ph(2,2)} {(0,1)} {(0,0)}


% «truth-values» (to ".truth-values")

\par A function from a ZSet $D$ to $\{0,1\}$ is a {\color{red}\sl
  modal truth-value}.

\par The positional notation gives us a way to write modal
truth-values very compactly, and the points on a ZSet have a natural
order - the ``reading order'', in which we read them line by line,
left to right in each line. \msk \par This gives us a way to {\sl read
  aloud} modal truth-values - \par and to list all modal truth-values
in order.

$$\bigKite abcde
  \bigKite 00110
  \;\; = \;\; \dagKite00110 \;\; = \;\; P
  (\text{``Kite 00110''})


Notation: $\Pts(\bbD)$ is the set of modal truth-values on $\bbD$

We use ``$\Pts(\bbD)$'' because $\dagKite00110$ ``is'' $\{c,d\}$ ($\subset K$)


% «intuitionistic-truth-values» (to ".intuitionistic-truth-values")
\frametitle{Intuitionistic truth-values}
$$\bigKite a b c d e   \qquad \bigKite 0 0 1 1 0 \;\; = P \qquad (\text{``Kite 00110''})
\par Now consider that each 1 in $P$ is covered with (wet) black paint.
\par Then $P$ (``Kite 00110'') is not {\sl stable}, because the paint
\par of the 1 in position $d$ will flow down into the 0 of position $e$,
\par and paint it black.
\par {\color{red}\sl Stable} modal truth-values are called
     {\color{red}\sl intuitionistic truth-values}.
\par Notation: $\dn P$ is $P$ after letting the black paint flow down.
\par Example: $\dn \dagKite 00110 = \dagKite 00111$


% «the-order-topology» (to ".the-order-topology")
\frametitle{The order topology}
     $$\dn \dagKite 00110 = \dagKite 00111$$
\par Notation: $\Pts(\bbD)$ is the set of modal truth-values on $\bbD$
\par Notation: $\Opens(\bbD)$ is the set of intuitionistic truth-values on $\bbD$
     $$\dn: \Pts(\bbD) \to \Opens(\bbD)$$
\par The topology $\Opens(\bbD)$ is the {\sl order topology} -
\par an arrow $\aa \to \bb$ in $\bbD$ means that
\par if an open set contains $\aa$ it has to contain $\bb$ too.
\par {\footnotesize (Order topologies are Alexandroff.)}

% «priming» (to ".priming")
\par Amazing fact: very often $\Opens(\bbD)$ can be represented as a ZDAG too!
\par $\Opens(\bbD)$ has a natural order:
\par $P \to Q$ means
     $P \le Q$,
     $P \subseteq Q$,
     $P \vdash Q$,
\par and $ = \dagVee111$ (``Top'') is the terminal of the category...
\par But if we draw $\Opens(\bbD)^\op$ instead of $\Opens(\bbD)$
\par we can see clearly how $\bbD \ito \Opens(\bbD)^\op$:
$$\bigVee a b c
  \bigKite {\dagVee111} {\dagVee101} {\dagVee 011} {\dagVee 001} {\dagVee 000}
  \bigKite {\dn ab} {\dn a} {\dn b} {\dn c} {\emp}
\par Note that $\dn ab = \dn \{a,b\} = \dn \dagVee110 = \dagVee111$.
\par Def: $\bbD' = \Opens(\bbD)^\op$.
\par $\bbV' \cong \bbK$ - and, by abuse of language, $\bbV' = \bbK$.

% «unpriming» (to ".unpriming")
\par If $\bbC' = \bbD$ can we recover $\bbC$ from $\bbD$?
\par Better: if $\bbD$ is a ZDAG that is a Heyting algebra
\par can we find a $\bbC \subset \bbD$ such that $\bbC' = \bbD$?
\par Can we use that to determine quickly whether
\par an arbitrary $\bbD$ is a Heyting algebra?
\par Yes, yes, \& yes!
% Look at the elements of $\left(\dagGuill******\right)'$
% that have exactly one arrow leaving them...
  \bigGuill abcdef
  \quad \cong \quad
    {\G 111111}  % 12
    {\G 101111}  % 11
    {\G 011111}  % 10
    {\G 001111}  % 8
    {\G 010111}  % 9
    {\G 001011}  % 7
    {\G 000111}  % 5
    {\G 001010}  % 6
    {\G 000011}  % 4
    {\G 000010}  % 3
    {\G 000001}  % 2
    {\G 000000}  % 1
    {\dn ab}   % 111111
    {\dn a}    % 101111
    {\dn bc}   % 011111
    {\dn cd}   % 001111
    {\dn b}    % 010111
    {\dn cf}   % 001011
    {\dn d}    % 000111
    {\dn c}    % 001010
    {\dn ef}   % 000011
    {\dn e}    % 000010
    {\dn f}    % 000001
    {\emptyset } % 000000


% «priming-theorems» (to ".priming-theorems")
\frametitle{Priming: theorems}
% \par For each ZDAG $\bbD$, let $\catD$ be $\bbD^*$ seen as a category.
% \par We say that $\bbC \subset \bbD$ when there is a
% \par proper inclusion $\catC \ito \catD$.
\par We say that $\bbD$ is {\em 3-thin} when $\dagHthree*** \not\subset \bbD$.
\par We say that $\bbD$ is {\em square-thin} when $\dagVV**** \not\subset \bbD$.
\par We say that $\bbD$ is {\em thin} when it is both 3-thin and square-thin.
\par Fact: if $\bbD$ is 3-thin then $\bbD'$ is a ZDAG.
\par Fact: if $\bbD$ is   thin then $\bbD'$ is a thin ZDAG.


Fact: every topology - whether planar or not - is a
Heyting algebra - i.e., we can interpret $T$, $F$, $\land$, $\lor$, $\to$,
$\neg$ on it, and every $\bbD'$ is a topology...

\par Priming gives us LOTS of Heyting algebras,
\par and lots of {\sl planar} Heyting algebras!


{\sl Topological} sheaves are defined on diagrams like
$\bbD \ito \bbD' \ito \bbD''$.


% «glueing-functions» (to ".glueing-functions")
% (find-LATEX "2011ebl-abs.tex" "quotient")
\frametitle{Glueing locally-defined functions}

\par Let $U$ be $(-,1)$
\par and $V$ be $(0,)$...
\par Consider these open sets in $\R$,
   \bigKite {(-,)} {(-,1)\ph} {\ph(0,)} {(0,1)} {\emp}
   % \quad
   \bigKite {UV} {U} {V} {UV} {\emp}
   \bigKite {X} {U} {V} {W} {\emp}
  \bigKite {\ctor X} {\ctor U\ph\ph} {\ph\ph\ctor V} {\ctor W} {\ctor\emp}
  \bigKite {\ctos X} {\ctos U} {\ctos V} {\ctos W} {\ctos\emp}
\par and the sheaf $C$ of $\Cinfty$ functions from them to $\R$.
\par Upward arrows are {\sl inclusions} (of an open set into another).
\par Downward arrows are {\sl restrictions} (of domains).
\par Two functions $f_U$ and $f_V$ are {\sl compatible}
\par if their restrictions to $UV$ coincide.
\par Each compatible family $\{f_U, f_V\}$ in $C$ has a unique glueing $f_X$.
\par Generalize that, and you get the definition of {\sl sheafness}.


% «sheafness» (to ".sheafness")

\par A compatible family $\{f_U, f_V\}$ is defined on $\{U, V\} = \dagKite01100$,
\par and it can be extended, using the restriction maps $\rho_{UW}:FU \to FW$ etc,
\par to a downward-closed compatible family $\{f_U, f_V, f_W, f_\emp\}$,
\par defined on $\{U, V, W, \emp\} = \dagKite01111$...
\par The ``unique glueing'' $f_X$ of $\{f_U, f_V\}$ can be extended
\par to a downward-closed compatible family $\{f_X, f_U, f_V, f_W, f_\emp\}$,
\par defined on $\{X, U, V, W, \emp\} = \dagKite11111$.
\par The restriction 
$$\{f_X, f_U, f_V, f_W, f_\emp\}
  \;\; \mton{\rho} \;\;
  \{f_U, f_V, f_W, f_\emp\}
\par is trivial to define -
\par {\color{red}sheafness means that maps like these are bijections.}


% «topological-sheafness» (to ".topological-sheafness")
\frametitle{Topological sheafness}
\par A closure operator:
$$ \{U, V, W, \emp\} = \{X, U, V, W, \emp\}$$
\par it takes the union $U  V  W  \emp = X$
\par and then all subsets of that.
\par It acts on $\bbV''$: \quad $: \dagVee***'' \to \dagVee***''$
$$ \dagKite01111 = \dagKite11111$$
\par Which elements of $\bbV''$ are stable by $$?
\par Only $\dn\{U,V\} \mto \dn \{X\}$ ($\dagKite01111 \mapsto \dagKite11111$)
     and  $\emp       \mto \{\emp\}$  ($\dagKite00000 \mapsto \dagKite00001$)
\par are {\sl not} stable by $$.
\par The stable elements of $\bbV''$ are these: $\dagKitePrime1011110$.
\par {\color{red}These diagrams of stable elements are what we need to
\par define sheaves ``in general''.}

% «the-evil-presheaf» (to ".the-evil-presheaf")
% (find-LATEXfile "2011ebl-abs.tex" "evil-presheaf")
\frametitle{The evil presheaf}

A presheaf $F$ in $\Set^{\Opens(\bbV)^\op}$

is simply a functor $F: \Opens(\bbV)^\op \to \Set$.
% (find-dn4 "experimental.lua" "relphantom")
%L forths[".xtag="] = function ()
%L     local dx, tag = getwordasluaexpr(), getword()
%L     tex = "\\ph{"..tag.."}"
%L     ds[1] = storenode{x=ds[1].x+dx, y=ds[1].y, tex=tex, tag=tag}
%L   end
%D diagram evil-presheaf
%D 2Dx     100 +20 +20  +30 +20 +20
%D 2D  100     A0           B0     
%D 2D         /  \         /  \    
%D 2D        v    v       v    v   
%D 2D  +20 A1      A2   B1      B2 
%D 2D        \    /       \    /   
%D 2D         v  v         v  v    
%D 2D  +20     A3           B3     
%D 2D          |            |      
%D 2D          v            v      
%D 2D  +20     A4           B4     
%D 2D
%D (( A0 .tex= E(X)
%D    A1 .tex= E(U)
%D    A2 .tex= E(V)
%D    A3 .tex= E(W)
%D    A4 .tex= E(\emp)
%D    A0 A1 ->
%D    A0 A2 ->
%D    A1 A3 ->
%D    A2 A3 ->
%D    A3 A4 ->
%D ))
%D (( B0 .tex= \{e_X,e'_X\}  place  .xtag= -6 e_X  .xtag= 12 e'_X
%D  # B1 .tex= \{e_U,e'_U\}  place  .xtag= -5 e_U  .xtag= 10 e'_U
%D    B1 .tex= \{e_U\}
%D    B2 .tex= \{e_V,e'_V\}  place  .xtag= -5 e_V  .xtag= 11 e'_V
%D    B3 .tex= \{e_W\}
%D    B4 .tex= \{e_\emp\}
%D  # e_X e_U ->  e'_X e'_U ->
%D  # e_X e_V ->  e'_X e_V  ->
%D  # e_U B3  ->  e'_U B3   ->
%D  # e_V B3  ->  e'_V B3   ->
%D  # B3 B4 ->
%D    e_X B1  ->  e'_X B1   ->
%D    e_X e_V ->  e'_X e_V  ->
%D    B1  B3  ->
%D    e_V B3  ->  e'_V B3   ->
%D    B3 B4 ->
%D ))
%D enddiagram
  % (find-LATEXgrep "grep -nH -e color *.tex")
  % \def\ph#1{{\color{red}#1}}
  % \def\ph#1{\phantom{#1}}

The {\color{red}evil presheaf} $E: \Opens(\bbV)^\op \to \Set$, above,

fails to be in a sheaf in two ways:

the compatible family $\{e_U, e_V\}$ has two different glueings,

the compatible family $\{e_U, e'_V\}$ doesn't have a glueing.


% «dual-operations» (to ".dual-operations")
\frametitle{Dual operations}

\par Due to we being in a finite / planar / etc case,
\par several interesting operations have duals (adjoints):

\item In finite DAGs the transitive-reflexive closure $(A,R) \mto (A,R^*)$
\par  has an adjoint that keeps only the ``essential arrows'' of the graph;

\item The ``let the paint flow down'' operation $\dn \dagKite00110=\dagKite00111$
\par  has an adjoint $\dagKite 00111 \mto \dagKite 00100$ that returns
      the ``generators''of an open set;

\item Each closure operator like $\calU \mto \calU$ has an adjoint that
      returns the smallest equivalent cover...

%\par In finite DAGs the transitive-reflexive closure $(A,R) \mto (A,R^*)$
%\par has an adjoint that keeps only the ``essential arrows'' of the graph;
%\par The ``let the paint flow down'' operation $\dn \dagKite00110=\dagKite00111$
%\par has an adjoint $\dagKite 00111 \mto \dagKite 00100$ that returns
%     the ``generators''of an open set;
%\par Each closure operator like $\calU \mto \calU$ has an adjoint that
%     returns the smallest equivalent cover...


% «where-are-the-theorems» (to ".where-are-the-theorems")
\frametitle{Where are the theorems?}

\par {\color{red}Not here! Why???}
\par Because this is ``for children'' -
\par we are focusing on the tools to let people check particular cases...
\par and this {\sl complements} [Bell 1988] and my IDARCT paper,
\par that explains how to do theorems and archetypal cases in parallel
\par Slightly more advanced things:

\item CCCs and Heyting Algebras; $(∧Q) \dashv (Q{\to})$
\item presheaves of the form $\Set^\bbD$ as toposes
\item the classifier object of a $\Set^\bbD$
\item other modalities (besides $$) in a $\Set^\bbD$
\item all logical properties of modalities follow from three axioms
\item operations on the lattice of modalities
\item forcing
\item sheafification
\item geometric morphisms between toposes - I need help here ${=}($


%% All of the following is optional and typically not needed. 
%\subsection<presentation>*{For Further Reading}
  % \frametitle<presentation>{For Further Reading}
  \frametitle{For Further Reading}
  % Start with overview books.

    \newblock {\em Toposes and Local Set Theories}.
    \newblock Oxford, 1988 (re-ed: Dover, 2007).
  % Followed by interesting articles. Keep the list short. 

    \newblock{\em Internal Diagrams and Archetypal Reasoning in Category Theory}
    \newblock Logica Universalis, 2013
  % (find-TH "math-b" "sheaves-on-zdags")
  % (find-TH "math-b" "internal-diags-in-ct")



% «closure-and-ess» (to ".closure-and-ess")
\frametitle{Closure and essentiality}
\par If $(A,R)$ is a graph,
\par then $(A,R^*)$ is its transitive-reflexive closure.
\par Notation and terminology:
\par $\bbD = (D, \BPM(D))$
\par $\bbD^* = (D, \BPM(D)^*)$
\par $\catD$ is $\bbD^*$ seen as a category ($\catD$ a poset)
\par $\Set^\catD$ is a ZDAG-topos
\par $\Opens(\bbD)$ are opens sets of the order topology on $\bbD$
\par $\bbD' = \Opens(\bbD)$
\par We ${\color{red}\heartsuit}$ transitive and reflexive relations
\par (and categories, and posets).
\par The operation $R \mapsto R^*$ is well-known.
\par If $(A,R)$ is a finite DAG,
\par look for the smallest set of arrows, $R^-$,
\par such that $(R^-)^* = R^*$.
\par Fact 1: on finite DAGs this $R^-$ is unique.
\par Fact 2: for any ZDAG $\bbD$ we have $\bbD^- = (\bbD^*)^- = \bbD$.
\par {\sl This is not well-known.}
% \msk
% \par Example: $\bbK \to \bbK^* \to (\bbK^*)^-$

%D diagram miniadj
%D 2Dx      100   120
%D 2D  100 a^L <= a
%D 2D       -     -
%D 2D       |     |
%D 2D       v     v
%D 2D  120  b => b^R
%D a^L a <=   a^L b |->   a b^R |->   b b^R =>
%D enddiagram

%:           [a,b]^1
%:           -------
%:  [a,b]^1     b      b|->c
%:  -------     ------------
%:     a             c
%:     ---------------
%:          a,c
%:        ---------1
%:        a,b|->a,c
%:        ^tree1

% «CT-lambda-calculus» (to ".CT-lambda-calculus")
\frametitle{CT and $\lambda$-calculus}
\par Again:
  \par Let A and B be (arbitrary) sets.
  \par Then there is an ``obvious'' function $\text{flip}: A×B \to B×A$.

\par This idea can be formalized in (typed, polymorphic) $\lambda$-calculus -
\par because $\lambda$-calculus is {\sl made} for expressing computations.
\par Roughly, we have this parallel:

\begin{tabular}{|l|l|} \hline
   $\lambda$-calculus &  Categories    \\ \hline
     computations     &  constructions \\
   $\lambda$-terms    &  diagrams      \\ \hline

Sales pitch:

{\sl Come learn CT, diagrammatic reasoning, $\lambda$-calculus and
  functional languages at the same time!}


% \section{Motivation}
% \subsection{The Basic Problem That We Studied}

% Local Variables:
% coding: raw-text-unix
% End: