% (find-angg "LATEX/2018jacobs.tex")
% (defun c () (interactive) (find-LATEXsh "lualatex -record 2018jacobs.tex" :end))
% (defun d () (interactive) (find-xpdfpage "~/LATEX/2018jacobs.pdf"))
% (defun b () (interactive) (find-zsh "bibtex 2018jacobs; makeindex 2018jacobs"))
% (defun e () (interactive) (find-LATEX "2018jacobs.tex"))
% (defun u () (interactive) (find-latex-upload-links "2018jacobs"))
% (find-xpdfpage "~/LATEX/2018jacobs.pdf")
% (find-sh0 "cp -v  ~/LATEX/2018jacobs.pdf /tmp/")
% (find-sh0 "cp -v  ~/LATEX/2018jacobs.pdf /tmp/pen/")
%   file:///home/edrx/LATEX/2018jacobs.pdf
%               file:///tmp/2018jacobs.pdf
%           file:///tmp/pen/2018jacobs.pdf
% http://angg.twu.net/LATEX/2018jacobs.pdf

% «.abstract»			(to "abstract")
% «.contents»			(to "contents")
%
% «.types-0»			(to "types-0")
% «.comprehension»		(to "comprehension")
% «.comprehension-tables»	(to "comprehension-tables")
% «.cartesian-product»		(to "cartesian-product")
% «.comprehension-exercises»	(to "comprehension-exercises")

\documentclass[oneside]{article}
\usepackage[colorlinks]{hyperref} % (find-es "tex" "hyperref")
%\usepackage[latin1]{inputenc}
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{pict2e}
\usepackage{color}                % (find-LATEX "edrx15.sty" "colors")
\usepackage{colorweb}             % (find-es "tex" "colorweb")
%\usepackage{tikz}
%
% (find-dn6 "preamble6.lua" "preamble0")
\usepackage{proof}   % For derivation trees ("%:" lines)
\input diagxy        % For 2D diagrams ("%D" lines)
%\xyoption{curve}     % For the ".curve=" feature in 2D diagrams
%
\usepackage{edrx15}               % (find-angg "LATEX/edrx15.sty")
\input edrxaccents.tex            % (find-angg "LATEX/edrxaccents.tex")
\input edrxchars.tex              % (find-LATEX "edrxchars.tex")
\input edrxheadfoot.tex           % (find-dn4ex "edrxheadfoot.tex")
\input edrxgac2.tex               % (find-LATEX "edrxgac2.tex")
%
\begin{document}

\catcode`\^^J=10
\directlua{dofile "dednat6load.lua"}

\def\expr#1{\directlua{output(tostring(#1))}}
\def\eval#1{\directlua{#1}}
\def\pu{\directlua{pu()}}

\directlua{dofile "edrxtikz.lua"} % (find-LATEX "edrxtikz.lua")
\directlua{dofile "edrxpict.lua"} % (find-LATEX "edrxpict.lua")
%L V.__tostring = function (v) return format("(%.3f,%.3f)", v[1], v[2]) end





%  _____ _ _   _      
% |_   _(_) |_| | ___ 
%   | | | | __| |/ _ \
%   | | | | |_| |  __/
%   |_| |_|\__|_|\___|
%                     
% or: Notes on Notation: Bart Jacobs

\title{Types for Children (working draft)}

\author{Eduardo Ochs}

\maketitle


% \setlength{\extrarowheight}{1pt}


%     _    _         _                  _   
%    / \  | |__  ___| |_ _ __ __ _  ___| |_ 
%   / _ \ | '_ \/ __| __| '__/ _` |/ __| __|
%  / ___ \| |_) \__ \ |_| | | (_| | (__| |_ 
% /_/   \_\_.__/|___/\__|_|  \__,_|\___|\__|
%                                           
% «abstract» (to ".abstract")
% (find-es "tex" "abstract")
\begin{abstract}

My favorite way to explain types to undergraduate students is by
showing first how to understand judgments that are very concrete ---
for example, if $A=\{1,2\}$, $B=\{3,4\}$ and $C=\{5,6\}$ then we can
make sense of $p:A×B, f:B→C ⊢ (πp,f(π'p)):A×C$ --- and then showing
that type systems are based on these ideas, but with some things made
more abstract, and with some restrictions that may seem arbitrary at
first.

In the first part of these notes we define a certain notation for set
comprehension --- because once we understand $\{p:A×B, f:B→C;
(πp,f(π'p))\}$ it is easy to give meaning to $p:A×B, f:B→C ⊢
(πp,f(π'p)):A×C$ --- and in the second part we define lambdas, types
(informally), judgments, derivation trees, derivation rules, and
discharges. In the third part we define a type system based on these
operations and we show some tools for reading a standard presentation
of that system (chapter 2 of Bart Jacobs's book). In the fourth
part we extend that system with $Σ$, $Π$ and dependent types and show
how to compare our concrete presentation with the one in the chapter
10 of Jacobs's book.

\end{abstract}


%   ____            _             _       
%  / ___|___  _ __ | |_ ___ _ __ | |_ ___ 
% | |   / _ \| '_ \| __/ _ \ '_ \| __/ __|
% | |__| (_) | | | | ||  __/ | | | |_\__ \
%  \____\___/|_| |_|\__\___|_| |_|\__|___/
%                                         
% «contents» (to ".contents")
% (find-es "tex" "tableofcontents")
% \tableofcontents
% (find-LATEXfile "2017yoneda.toc")

\bsk

Index of sections:

{\makeatletter
\renewcommand*\l@section{\@dottedtocline{1}{1.5em}{2.3em}}
\@starttoc{toc}
}

\bsk




% (gamp)
% 3-8: (gam)


% Até p.14: (lamp)
% (lam)

















\def\erro{\operatorname{erro}}
\def\setofpt  #1 #2 #3 #4 {\setofet{(#1,#2)+t\VEC{#3,#4}}}
\def\setofpu  #1 #2 #3 #4 {\setofeu{(#1,#2)+u\VEC{#3,#4}}}

% (find-LATEXfile "2016-1-GA-material.tex" "setofet")
\def\setofet  #1{\setofst{#1}{t∈\R}}
\def\setofeu  #1{\setofst{#1}{u∈\R}}
\def\setofpt  #1 #2 #3 #4 {\setofet{(#1,#2)+t\VEC{#3,#4}}}
\def\setofpu  #1 #2 #3 #4 {\setofeu{(#1,#2)+u\VEC{#3,#4}}}

\unitlength=5pt



% «picturedots» (to ".picturedots")
% (find-LATEX "edrxpict.lua" "pictdots")
% (find-LATEX "edrxgac2.tex" "pict2e")
% (to "comprehension-gab")
%
\def\beginpicture(#1,#2)(#3,#4){\expr{beginpicture(v(#1,#2),v(#3,#4))}}
\def\pictaxes{\expr{pictaxes()}}
\def\pictdots#1{\expr{pictdots("#1")}}
\def\picturedots(#1,#2)(#3,#4)#5{%
  \vcenter{\hbox{%
  \beginpicture(#1,#2)(#3,#4)%
  \pictaxes%
  \pictdots{#5}%
  \end{picture}%
  }}%
}

\unitlength=5pt

%L p = function (a, b) return O + a*uu + b*vv end

%L --  «pictOuv» (to ".pictOuv")
%L pictOOuuvv = function (OO, xx, yy, OOtext, xxtext, yytext, vtextdist, Otextdist)
%L     local bprint, out = makebprint()
%L     local xxpos = OO + xx/2 + xx:rotright():unit(vtextdist)
%L     local yypos = OO + yy/2 + yy:rotleft() :unit(vtextdist)
%L     local OOpos = OO + (-xx-yy):unit(Otextdist or vtextdist)
%L     local f = function (str) return (str:gsub("!", "\\")) end
%L     bprint("\\Vector%s%s", OO, OO+xx)
%L     bprint("\\Vector%s%s", OO, OO+yy)
%L     bprint("\\put%s{\\cell{%s}}", OOpos, f(OOtext))
%L     bprint("\\put%s{\\cell{%s}}", xxpos, f(xxtext))
%L     bprint("\\put%s{\\cell{%s}}", yypos, f(yytext))
%L     return out()
%L   end
%L -- sysco = pictOOuuvv
\def\pictOuv(#1,#2){
  {\color{GrayPale}\expr{pictpgrid(0,0,4,4)}}
  \pictaxes
  {\linethickness{1.0pt}
   \expr{pictOOuuvv(O, uu, vv,  "O", "!uu", "!vv", #1, #2)}
  }
}

%L -- «pictABCDE» (to ".pictABCDE")
%L tt = v(1, 0)
%L pictABCDE = function (aang, bang, cang, dang, eang)
%L     local bprint, out = makebprint()
%L     local AA, BB, CC, DD, EE = p(1,1), p(1,3), p(3,3), p(1,2), p(2,2)
%L     local f = function (str) return (str:gsub("!", "\\")) end
%L     bprint("\\Line%s%s", AA, BB)
%L     bprint("\\Line%s%s", BB, CC)
%L     bprint("\\Line%s%s", DD, EE)
%L     bprint("\\put%s{\\closeddot}", AA)
%L     bprint("\\put%s{\\closeddot}", BB)
%L     bprint("\\put%s{\\closeddot}", CC)
%L     bprint("\\put%s{\\closeddot}", DD)
%L     bprint("\\put%s{\\closeddot}", EE)
%L     bprint("\\put%s{\\cell{%s}}", AA + tt:rot(aang), "A")
%L     bprint("\\put%s{\\cell{%s}}", BB + tt:rot(bang), "B")
%L     bprint("\\put%s{\\cell{%s}}", CC + tt:rot(cang), "C")
%L     bprint("\\put%s{\\cell{%s}}", DD + tt:rot(dang), "D")
%L     bprint("\\put%s{\\cell{%s}}", EE + tt:rot(eang), "E")
%L     return out()
%L   end
\def\pictABCDE(#1,#2,#3,#4,#5){
  {\linethickness{1.0pt}
   \expr{pictABCDE(#1,#2,#3,#4,#5)}
  }
}

\pu


% «cells» (to ".cells")
% (find-es "tex" "fbox")

% \def\cellhr#1{\hbox to 0pt    {\cellfont${#1}$\hss}}
% \def\cellhc#1{\hbox to 0pt{\hss\cellfont${#1}$\hss}}
% \def\cellhl#1{\hbox to 0pt{\hss\cellfont${#1}$}}
% \def\cellva#1{\setbox0#1\raise \dp0       \box0}
% \def\cellvm#1{\setbox0#1\lower \celllower \box0}
% \def\cellvb#1{\setbox0#1\lower \ht0       \box0}
% 
% \def\cellnw  #1{\cellva{\cellhl{#1}}}
%  \def\celln  #1{\cellva{\cellhc{#1}}}
%   \def\cellne#1{\cellva{\cellhr{#1}}}
% \def\cellw   #1{\cellvm{\cellhl{#1}}}
%  \def\celle  #1{\cellvm{\cellhr{#1}}}
% \def\cellsw  #1{\cellvb{\cellhl{#1}}}
%  \def\cells  #1{\cellvb{\cellhc{#1}}}
%   \def\cellse#1{\cellvb{\cellhr{#1}}}

% \newdimen\cellsep
% \cellsep=4pt
% \def\addcellsep{%
%   \setbox0=\hbox{\kern\cellsep\box0\kern\cellsep}%
%   \ht0=\ht0 plus \cellsep%
%   \dp0=\dp0 plus \cellsep%
%   \box0%
% }
% \def\cellsp#1{%
%   \setbox0=\hbox{#1}%
%   \addcellsep%
%   \box0%
% }






% «pictureFxy» (to ".pictureFxy")
\def\tcell#1{\lower\celllower\hbox to 0pt{\hss\cellfont#1\hss}}
\def\pictureFxy(#1,#2)(#3,#4)#5{%
  \vcenter{\hbox{%
  \beginpictureb(#1,#2)(#3,#4){.7}%
  {\color{GrayPale}%
   \Line(#1,0)(#3,0)%
   \Line(0,#2)(0,#4)%
  }
  \expr{pictFxy("#5")}
  \end{picture}%
  }}%
}





% %   ____      _                                 _ _
% %  / ___|___ (_)___  __ _ ___   _ __ ___  _   _(_) |_ ___
% % | |   / _ \| / __|/ _` / __| | '_ ` _ \| | | | | __/ _ \
% % | |__| (_) | \__ \ (_| \__ \ | | | | | | |_| | | || (_) |
% %  \____\___/|_|___/\__,_|___/ |_| |_| |_|\__,_|_|\__\___/
% %
% % «coisas-muito» (to ".coisas-muito")
% % (gam181p 1 "coisas-muito")
% \label{coisas-muito}
% 
% {\setlength{\parindent}{0em}
% \footnotesize
% \par Geometria Analítica - material para exercícios
% \par PURO-UFF - 2018.1 - Eduardo Ochs
% \par Links importantes:
% \par \url{http://angg.twu.net/2018.1-GA.html} (página do curso)
% \par \url{http://angg.twu.net/2018.1-GA/2018.1-GA.pdf} (quadros)
% \par \url{http://angg.twu.net/LATEX/2018-1-GA-material.pdf} (isto aqui)
% \par {\tt eduardoochs@gmail.com} (meu e-mail)
% \par Dá pra chegar na página do curso googlando por ``Eduardo Ochs'',
% \par indo pra qualquer subpágina do angg.twu.net, e clicando em ``GA''
% \par na barra de navegação à esquerda.
% 
% }
% 
% \bsk
% \bsk
% 
% 
% 
% 
% {
% \setlength{\parindent}{0em}
% 
% {\bf Coisas {\bf MUITO} importantes sobre Geometria Analítica}
% }
% 
% \msk
% 
% A matéria é sobre duas linguagens diferentes: a
% %
% \begin{itemize}
% \item ``Geometria'', que é sobre coisas gráficas como pontos, retas e
%   círculos, e a
% 
% \item ``Analítica'', que é sobre ``álgebra'', sobre coisas matemáticas
%   ``formais'' como contas, conjuntos e equações;
% 
% \end{itemize}
% %
% além disso Geometria Analítica é também sobre a TRADUÇÃO entre essas
% duas linguagens.
% 
% \msk
% 
% Lembre que boa parte do que você aprendeu sobre álgebra no ensino
% médio era sobre {\sl resolver equações}.
% 
% {\sl Encontrar soluções} de equações é difícil --- são muitos métodos,
% e dá pra errar bastante no caminho --- mas {\sl testar} as soluções é
% fácil.
% 
% \msk
% 
% Boa parte do que você aprendeu (ou deveria ter aprendido) sobre
% geometria no ensino médio envolvia construções gráficas; por exemplo,
% a partir de pontos $A$, $B$, $C$,
% 
% Seja $A'$ o ponto médio entre $B$ e $C$,
% 
% Seja $B'$ o ponto médio entre $A$ e $C$,
% 
% Seja $C'$ o ponto médio entre $A$ e $B$,
% 
% Seja $r_a$ a reta que passa por $A'$ e é ortogonal a $BC$,
% 
% Seja $r_b$ a reta que passa por $B'$ e é ortogonal a $AC$,
% 
% Seja $r_c$ a reta que passa por $C'$ e é ortogonal a $AB$,
% 
% Seja $D$ o ponto de interseção das retas $r_a$, $r_b$ e $r_c$,
% 
% então $D$ é o centro do círculo que passa por $A$, $B$ e $C$.
% 
% \msk
% 
% Você {\bf VAI TER QUE} aprender a definir seus objetos --- pontos, retas,
% conjuntos, círculos, etc... isso provavelmente vai ser algo novo pra
% você e é algo que precisa de MUITO treino. Dá pra passar em Cálculo 1
% e em Prog 1 só aprendendo a ``ler'' as definições que o professor e os
% livros mostram, mas em Geometria Analítica NÃO DÁ, em GA você vai ter
% que aprender a ler {\bf E A ESCREVER} definições.
% 
% 
% 
% 
% \newpage
% 
% %  ____  _
% % |  _ \(_) ___ __ _ ___
% % | | | | |/ __/ _` / __|
% % | |_| | | (_| (_| \__ \
% % |____/|_|\___\__,_|___/
% %
% % «dicas» (to ".dicas")
% % (gam181p 2 "dicas")
% \label{dicas}
% 
% {\bf Dicas MUITO IMPORTANTES e pouco óbvias:}
% 
% \ssk
% 
% 1) Aprenda a testar tudo: contas, possíveis soluções de equações,
% representações gráficas de conjuntos...
% 
% 2) Cada ``seja'' ou ``sejam'' que aparece nestas folhas é uma
% definição, e você pode usá-los como exemplos de definições
% bem-escritas (ééé!!!!) pra aprender jeitos de escrever as suas
% definições.
% 
% 3) Em ``matematiquês'' a gente quase não usa termos como ``ele'',
% ``ela'', ``isso'', ``aquilo'' e ''lá'' --- ao invés disso a gente dá
% nomes curtos pros objetos ou usa expressões matemáticas pra eles cujo
% resultado é o objeto que a gente quer (como nas pags
% \pageref{comprehension-ex123} e \pageref{projecoes})... mas {\sl
%   quando a gente está discutindo problemas no papel ou no quadro} a
% gente pode ser referir a determinados objetos {\sl apontando pra eles
%   com o dedo} e dizendo ``esse aqui''.
% 
% 4) Se você estiver em dúvida sobre o que um problema quer dizer tente
% escrever as suas várias hipóteses --- a prática de escrever as suas
% idéias é o que vai te permitir aos poucos conseguir resolver coisas de
% cabeça.
% 
% 5) Muitas coisas aparecem nestas folhas escritas primeiro de um jeito
% detalhado, e depois aos poucos de jeitos cada vez mais curtos. Você
% vai ter que aprender a completar os detalhes.
% 
% 6) Alguns exercícios destas folhas têm muitos subcasos. Nos primeiros
% subcasos você provavelmente vai precisar fazer as contas com todos os
% detalhes e verificá-las várias vezes pra não errar, depois você vai
% aprender a fazê-las cada vez mais rápido, depois vai poder fazê-las de
% cabeça, e depois você vai começar a visualizar o que as contas
% ``querem dizer'' e vai conseguir chegar ao resultado graficamente, sem
% contas; e se você estiver em dúvida se o seu ``método gráfico'' está
% certo você vai poder conferir se o ``método gráfico'' e o ``método
% contas'' dão aos mesmos resultados. Exemplo: p.\pageref{coordenadas}.
% 
% 7) Uma solução bem escrita pode incluir, além do resultado final,
% contas, definições, representações gráficas, explicações em português,
% testes, etc. Uma solução bem escrita é fácil de ler e fácil de
% verificar. Você pode testar se uma solução sua está bem escrita
% submetendo-a às seguinte pessoas: a) você mesmo logo depois de você
% escrevê-la --- releia-a e veja se ela está clara; b) você mesmo, horas
% depois ou no dia seguinte, quando você não lembrar mais do que você
% pensava quando você a escreveu; c) um colega que seja seu amigo; d) um
% colega que seja menos seu amigo que o outro; e) o monitor ou o
% professor. Se as outras pessoas acharem que ler a sua solução é um
% sofrimento, isso é mau sinal; se as outras pessoas acharem que a sua
% solução está claríssima e que elas devem estudar com você, isso é bom
% sinal. {\sl GA é um curso de escrita matemática:} se você estiver
% estudando e descobrir que uma solução sua pode ser reescrita de um
% jeito bem melhor, não hesite --- reescrever é um ótimo exercício.
% 
% 8) Estas notas {\sl vão ser} uma versão ampliada e melhorada destas
% notas aqui, do semestre passado:
% 
% \url{http://angg.twu.net/LATEX/2017-1-GA-material.pdf}
% 
% 
% 
% 
% \newpage






%  __  __       _        _
% |  \/  | __ _| |_ _ __(_)_______  ___
% | |\/| |/ _` | __| '__| |_  / _ \/ __|
% | |  | | (_| | |_| |  | |/ /  __/\__ \
% |_|  |_|\__,_|\__|_|  |_/___\___||___/
%
% «types-0» (to ".types-0")
% (gam181p 3 "matrizes")
\section{Types in basic math}
\label{types-0}

Multiplicação de matrizes:

\def\und#1#2{\underbrace{#1}_{#2}}

$\und{\pmat{1 & 2 & 3 \\ 4 & 5 & 6 \\ 7 & 8 & 9}}{3×3}
 \und{\pmat{1000 \\ 100 \\ 10}}{3×1}
 = \und{\pmat{1230 \\ 4560 \\ 7890}}{3×1}
$

$\und{\pmat{a & b \\ c & d \\ e & f}}{3×2}
 \und{\pmat{g & h & i & j \\ k & l & m & n}}{2×4}
 = \und{\pmat{ag+bk & ah+bl & ai+bm & aj+bn \\
              cg+dk & ch+dl & ci+dm & cj+dn \\
              eg+fk & eh+fl & ei+fm & ej+fn \\}}{3×4}
$

$\und{\pmat{g & h & i & j \\ k & l & m & n}}{2×4}
 \und{\pmat{a & b \\ c & d \\ e & f}}{3×2}
 = \; \text{erro \qquad (porque $4≠3$)}
$

$\pmat{1 & 2 \\ 3 & 4} \pmat{100 & 0 \\ 10 & 0} = \pmat{120 & 0 \\ 340 & 0}$

\ssk

$\pmat{100 & 0 \\ 10 & 0} \pmat{1 & 2 \\ 3 & 4} = \pmat{100 & 200 \\ 10 & 20}$

\ssk

$\pmat{2 \\ 3 \\ 4}^T \pmat{100 \\ 10 \\ 1} = \pmat{2 & 3 & 4} \pmat{100 \\ 10 \\ 1} = (234) = 234$

\bsk

Soma de matrizes:

$\pmat{10 & 20 & 30 \\ 40 & 50 & 60} + \pmat{2 & 3 & 4 \\ 5 & 6 & 7} = \pmat{12 & 23 & 34 \\ 45 & 56 & 67}$

$\pmat{10 & 20 & 30 \\ 40 & 50 & 60} + \pmat{2 & 3 \\ 5 & 6 } = \; \text{erro}$

\bsk

Multiplicação de número por matriz:

$10 \pmat{2 & 3 & 4 \\ 5 & 6 & 7} = \pmat{20 & 30 & 40 \\ 50 & 60 & 70}$



\bsk

\def\V{\mathbf{V}}
\def\F{\mathbf{F}}

Operações lógicas:

\ssk

$\begin{array}[t]{rcl}
 \text{``E'':} \\
 \F\&\F &=& \F \\
 \F\&\V &=& \F \\
 \V\&\F &=& \F \\
 \V\&\V &=& \V \\
 \end{array}
 %
 \quad
 %
 \begin{array}[t]{rcl}
 \text{``Ou'':} \\
 \F∨\F &=& \F \\
 \F∨\V &=& \V \\
 \V∨\F &=& \V \\
 \V∨\V &=& \V \\
 \end{array}
 %
 \quad
 %
 \begin{array}[t]{rcl}
 \text{``Implica'':}\hss \\
 \F→\F &=& \V \\
 \F→\V &=& \V \\
 \V→\F &=& \F \\
 \V→\V &=& \V \\
 \end{array}
 %
 \quad
 %
 \begin{array}[t]{rcl}
 \text{``Não'':} \\
 ¬\F &=& \V \\
 ¬\V &=& \F \\
 \end{array}
$

\bsk

Se $x=6$,

$\und{\und{2<\und{x}{6}}{\V} \&
      \und{\und{x}{6}<5}{\F}
     }{\F}
$




%   ____                               _                    _
%  / ___|___  _ __ ___  _ __  _ __ ___| |__   ___ _ __  ___(_) ___  _ __
% | |   / _ \| '_ ` _ \| '_ \| '__/ _ \ '_ \ / _ \ '_ \/ __| |/ _ \| '_ \
% | |__| (_) | | | | | | |_) | | |  __/ | | |  __/ | | \__ \ | (_) | | | |
%  \____\___/|_| |_| |_| .__/|_|  \___|_| |_|\___|_| |_|___/_|\___/|_| |_|
%                      |_|
%
% «comprehension» (to ".comprehension")
% (gam181p 4 "comprehension")
\section{Set comprehension}
\label{comprehension}

\def\und#1#2{\underbrace{#1}_{#2}}
\def\und#1#2{\underbrace{#1}_{\text{#2}}}
\def\ug#1{\und{#1}{ger}}
\def\uf#1{\und{#1}{filt}}
\def\ue#1{\und{#1}{expr}}

Notação explícita, com geradores, filtros,

e um ``;'' separando os geradores e filtros da expressão final:

$\begin{array}{lll}
\{\ug{a∈\{1,2,3,4\}}; \ue{10a}\}     &=& \{10,20,30,40\} \\
\{\ug{a∈\{1,2,3,4\}}; \ue{a}\}       &=& \{1,2,3,4\} \\
\{\ug{a∈\{1,2,3,4\}}, \uf{a≥3}; \ue{a}\} &=& \{3,4\} \\
\{\ug{a∈\{1,2,3,4\}}, \uf{a≥3}; \ue{10a}\} &=& \{30,40\} \\
\{\ug{a∈\{10,20\}}, \ug{b∈\{3,4\}}; \ue{a+b}\} &=& \{13,14,23,24\} \\
\{\ug{a∈\{1,2\}}, \ug{b∈\{3,4\}}; \ue{(a,b)}\} &=& \{(1,3),(1,4),(2,3),(2,4)\} \\
\end{array}
$





% (setq last-kbd-macro (kbd "C-w \\ uf{ C-y }"))
% (setq last-kbd-macro (kbd "C-w \\ ue{ C-y }"))

\msk
\msk

Notações convencionais, com ``$|$'' ao invés de ``;'':

Primeiro tipo --- expressão final, ``$|$'', geradores e filtros:

$\begin{array}{lll}
\setofst{10a}{a∈\{1,2,3,4\}} &=&
  \{\ug{a∈\{1,2,3,4\}}; \ue{10a}\} \\
\setofst{10a}{a∈\{1,2,3,4\}, a≥3} &=&
  \{\ug{a∈\{1,2,3,4\}}, \uf{a≥3}; \ue{10a}\} \\
\setofst{a}{a∈\{1,2,3,4\}} &=&
  \{\ug{a∈\{1,2,3,4\}}; \ue{a}\} \\
% \{\ug{a∈\{1,2\}}, \ug{b∈\{3,4\}}; \ue{(a,b)}\} \\
\end{array}
$

\msk

O segundo tipo --- gerador, ``$|$'', filtros ---

pode ser convertido para o primeiro...

o truque é fazer a expressão final ser a variável do gerador:

$\begin{array}{lll}
\setofst{a∈\{1,2,3,4\}}{a≥3} &=& \\
\setofst{a}{a∈\{1,2,3,4\}, a≥3} &=&
  \{\ug{a∈\{1,2,3,4\}}, \uf{a≥3}; \ue{a}\} \\
% \{\ug{a∈\{10,20\}}, \ug{b∈\{3,4\}}; \ue{a+b}\} \\
\end{array}
$

\msk

O que distingue as duas notacões ``$\{\ldots|\ldots\}$'' é

se o que vem antes da ``$|$'' é ou não um gerador.

\bsk

Observações:

$\setofst{\text{gerador}}{\text{filtros}} =
 \{\text{gerador},\text{filtros};\ue{\text{variável do gerador}}\}$

$\setofst{\text{expr}}{\text{geradores e filtros}} =
 \{\text{geradores e filtros}; \text{expr}\}
$

\msk

As notações ``$\{\ldots|\ldots\}$'' são padrão e são usadas em muitos livros de matemática.

A notação ``$\{\ldots;\ldots\}$'' é bem rara; eu aprendi ela em
artigos sobre linguagens de programação, e resolvi apresentar ela aqui
porque acho que ela ajuda a explicar as duas notações
``$\{\ldots|\ldots\}$''.


%                                     _                    _               _____
%   ___ ___  _ __ ___  _ __  _ __ ___| |__   ___ _ __  ___(_) ___  _ __   |_   _|
%  / __/ _ \| '_ ` _ \| '_ \| '__/ _ \ '_ \ / _ \ '_ \/ __| |/ _ \| '_ \    | |
% | (_| (_) | | | | | | |_) | | |  __/ | | |  __/ | | \__ \ | (_) | | | |   | |
%  \___\___/|_| |_| |_| .__/|_|  \___|_| |_|\___|_| |_|___/_|\___/|_| |_|   |_|
%                     |_|
%
% «comprehension-tables» (to ".comprehension-tables")
% (gam181p 5 "comprehension-tables")
% (find-es "tex" "vrule")

\section{A way to calculate comprehensions with tables}
\label{comprehension-tables}

\def\tbl#1#2{\fbox{$\begin{array}{#1}#2\end{array}$}}
\def\tbl#1#2{\fbox{$\sm{#2}$}}
\def\V{\mathbf{V}}
\def\F{\mathbf{F}}

% "Stop":
\def\S{\omit$|$\hss}
\def\S{\omit\vrule\hss}
\def\S{\omit\vrule$($\hss}
\def\S{\omit\vrule$\scriptstyle($\hss}
\def\S{\omit\vrule\phantom{$\scriptstyle($}\hss}   % stop

Alguns exemplos:

\msk

\def\s{\mathstrut}
\def\s{\phantom{$|$}}
\def\s{\phantom{|}}
\def\s{}

Se $A := \{x∈\{1,2\}; (x,3-x)\}$

então $A = \{(1,2), (2,1)\}$:

\tbl{ccc}{
 \s x & (x,3-x) \\\hline
 \s 1 & (1,2) \\
 \s 2 & (2,1) \\
}

\msk

Se $I := \{x∈\{1,2,3\}, y∈\{3,4\}, x+y<6; (x,y)\}$

então $I = \{(1,3),(1,4),(1,5)\}$:

\tbl{ccc}{
 \s x & y & x+y<6 & (x,y) \\\hline
 \s 1 & 3 & \V & (1,3) \\
 \s 1 & 4 & \V & (1,4) \\
 \s 2 & 3 & \V & (2,3) \\
 \s 2 & 4 & \F & \S \\
 \s 3 & 3 & \F & \S \\
 \s 3 & 4 & \F & \S \\
}

\msk

Se $D := \setofst{(x,2x)}{x∈\{0,1,2,3\}}$

então $D = \{x∈\{0,1,2,3\}; (x,2x)\}$,

$D = \{(0,0), (1,2), (2,4), (3,6)\}$:

\tbl{ccc}{
 \s x & (x,2x) \\\hline
 \s 0 & (0,0) \\
 \s 1 & (1,2) \\
 \s 2 & (2,4) \\
 \s 3 & (3,6) \\
}

\msk

Se $P := \setofst {(x,y)∈\{1,2,3\}^2} {x≥y}$

então $P = \{(x,y)∈\{1,2,3\}^2, x≥y; (x,y)\}$,

$P = \{(1,1), (2,1), (2,2), (3,1), (3,2), (3,3)\}$:

\tbl{ccc}{
 \s (x,y) & x & y & x≥y & (x,y) \\\hline
 \s (1,1) & 1 & 1 & \V & (1,1) \\
 \s (1,2) & 1 & 2 & \F & \S    \\
 \s (1,3) & 1 & 3 & \F & \S    \\
 \s (2,1) & 2 & 1 & \V & (2,1) \\
 \s (2,2) & 2 & 2 & \V & (2,2) \\
 \s (2,3) & 2 & 3 & \F & \S    \\
 \s (3,1) & 3 & 1 & \V & (3,1) \\
 \s (3,2) & 3 & 2 & \V & (3,2) \\
 \s (3,3) & 3 & 3 & \V & (3,3) \\
}

\bsk

Obs: os exemplos acima correspondem aos

exercícios 2A, 2I, 3D e 5P das próximas páginas.


%   ____           _                         _ 
%  / ___|__ _ _ __| |_   _ __  _ __ ___   __| |
% | |   / _` | '__| __| | '_ \| '__/ _ \ / _` |
% | |__| (_| | |  | |_  | |_) | | | (_) | (_| |
%  \____\__,_|_|   \__| | .__/|_|  \___/ \__,_|
%                       |_|                    
%
% «cartesian-product» (to ".cartesian-product")
\section{Cartesian product}
\label{comprehension-prod}

$A×B:=\{a∈A,b∈B;(a,b)\}$

Exemplo: $\{1,2\}×\{3,4\} = \{(1,3),(1,4),(2,3),(2,4)\}$.

\ssk

Uma notação: $A^2 = A×A$.

Exemplo: $\{3,4\}^2 = \{3,4\}×\{3,4\} = \{(3,3),(3,4),(4,3),(4,4)\}$.



%  _____                   _      _
% | ____|_  _____ _ __ ___(_) ___(_) ___  ___
% |  _| \ \/ / _ \ '__/ __| |/ __| |/ _ \/ __|
% | |___ >  <  __/ | | (__| | (__| | (_) \__ \
% |_____/_/\_\___|_|  \___|_|\___|_|\___/|___/
%
% «comprehension-exercises» (to ".comprehension-exercises")
% (gam181p 6 "comprehension-ex123")
\section{Comprehension: exercices}
\label{comprehension-ex123}

1) Represente graficamente:

$\begin{array}{rcl}
 A & := & \{(1,4), (2,4), (1,3)\} \\
 B & := & \{(1,3), (1,4), (2,4)\} \\
 C & := & \{(1,3), (1,4), (2,4), (2,4)\} \\
 D & := & \{(1,3), (1,4), (2,3), (2,4)\} \\
 E & := & \{(0,3), (1,2), (2,1), (3,0)\} \\
\end{array}
$

\msk

2) Calcule e represente graficamente:

$\begin{array}{rcl}
 A & := & \{x∈\{1,2\}; (x,3-x)\} \\
 B & := & \{x∈\{1,2,3\}; (x,3-x)\} \\
 C & := & \{x∈\{0,1,2,3\}; (x,3-x)\} \\
 D & := & \{x∈\{0,0.5,1, \ldots, 3\}; (x,3-x)\} \\
 E & := & \{x∈\{1,2,3\}, y∈\{3,4\}; (x,y)\} \\
 F & := & \{x∈\{3,4\}, y∈\{1,2,3\}; (x,y)\} \\
 G & := & \{x∈\{3,4\}, y∈\{1,2,3\}; (y,x)\} \\
 H & := & \{x∈\{3,4\}, y∈\{1,2,3\}; (x,2)\} \\
 I & := & \{x∈\{1,2,3\}, y∈\{3,4\}, x+y<6; (x,y)\} \\
 J & := & \{x∈\{1,2,3\}, y∈\{3,4\}, x+y>4; (x,y)\} \\
 K & := & \{x∈\{1,2,3,4\}, y∈\{1,2,3,4\}; (x,y)\} \\
 L & := & \{x,y∈\{0,1,2,3,4\}; (x,y)\} \\
 M & := & \{x,y∈\{0,1,2,3,4\}, y=3; (x,y)\} \\
 N & := & \{x,y∈\{0,1,2,3,4\}, x=2; (x,y)\} \\
 O & := & \{x,y∈\{0,1,2,3,4\}, x+y=3; (x,y)\} \\
 P & := & \{x,y∈\{0,1,2,3,4\}, y=x; (x,y)\} \\
 Q & := & \{x,y∈\{0,1,2,3,4\}, y=x+1; (x,y)\} \\
 R & := & \{x,y∈\{0,1,2,3,4\}, y=2x; (x,y)\} \\
 S & := & \{x,y∈\{0,1,2,3,4\}, y=2x+1; (x,y)\} \\
\end{array}
$

\msk

3) Calcule e represente graficamente:

$\begin{array}{rcl}
 A & := & \setofst{(x,0)}{x∈\{0,1,2,3\}} \\
 B & := & \setofst{(x,x/2)}{x∈\{0,1,2,3\}} \\
 C & := & \setofst{(x,x)}{x∈\{0,1,2,3\}} \\
 D & := & \setofst{(x,2x)}{x∈\{0,1,2,3\}} \\
 E & := & \setofst{(x,1)}{x∈\{0,1,2,3\}} \\
 F & := & \setofst{(x,1+x/2)}{x∈\{0,1,2,3\}} \\
 G & := & \setofst{(x,1+x)}{x∈\{0,1,2,3\}} \\
 H & := & \setofst{(x,1+2x)}{x∈\{0,1,2,3\}} \\
 I & := & \setofst{(x,2)}{x∈\{0,1,2,3\}} \\
 J & := & \setofst{(x,2+x/2)}{x∈\{0,1,2,3\}} \\
 K & := & \setofst{(x,2+x)}{x∈\{0,1,2,3\}} \\
 L & := & \setofst{(x,2+2x)}{x∈\{0,1,2,3\}} \\
 M & := & \setofst{(x,2)}{x∈\{0,1,2,3\}} \\
 N & := & \setofst{(x,2-x/2)}{x∈\{0,1,2,3\}} \\
 O & := & \setofst{(x,2-x)}{x∈\{0,1,2,3\}} \\
 P & := & \setofst{(x,2-2x)}{x∈\{0,1,2,3\}} \\
\end{array}
$


%  ____                _                  _
% |  _ \ _ __ ___   __| |   ___ __ _ _ __| |_
% | |_) | '__/ _ \ / _` |  / __/ _` | '__| __|
% |  __/| | | (_) | (_| | | (_| (_| | |  | |_
% |_|   |_|  \___/ \__,_|  \___\__,_|_|   \__|
%
% «comprehension-prod» (to ".comprehension-prod")
% (gam181p 7 "comprehension-prod")

Sejam:

$A = \{1,2,4\}$,

$B = \{2,3\}$,

$C = \{2,3,4\}$.


\msk

{\bf Exercícios}

\ssk

4) Calcule e represente graficamente:

\begin{tabular}{lll}
a) $A×A$ & d) $B×A$ & g) $C×A$ \\
b) $A×B$ & e) $B×B$ & h) $C×B$ \\
c) $A×C$ & f) $B×C$ & i) $C×C$ \\
\end{tabular}

\msk

5) Calcule e represente graficamente:

$\begin{array}{rcl}
 A &:=& \{x,y∈\{0,1,2,3\};(x,y)\} \\
 B &:=& \{x,y∈\{0,1,2,3\}, y=2; (x,y)\} \\
 C &:=& \{x,y∈\{0,1,2,3\}, x=1; (x,y)\} \\
 D &:=& \{x,y∈\{0,1,2,3\}, y=x; (x,y)\} \\
 E &:=& \{x,y∈\{0,1,2,3,4\}, y=2x; (x,y)\} \\
 F &:=& \{(x,y)∈\{0,1,2,3,4\}^2, y=2x; (x,y)\} \\
 G &:=& \{(x,y)∈\{0,1,2,3,4\}^2, y=x; (x,y)\} \\
 H &:=& \{(x,y)∈\{0,1,2,3,4\}^2, y=x/2; (x,y)\} \\
 I &:=& \{(x,y)∈\{0,1,2,3,4\}^2, y=x/2+1; (x,y)\} \\
 J &:=& \setofst {(x,y)∈\{0,1,2,3,4\}^2} {y=2x} \\
 K &:=& \setofst {(x,y)∈\{0,1,2,3,4\}^2} {y=x} \\
 L &:=& \setofst {(x,y)∈\{0,1,2,3,4\}^2} {y=x/2} \\
 M &:=& \setofst {(x,y)∈\{0,1,2,3,4\}^2} {y=x/2+1} \\
 N &:=& \setofst {(x,y)∈\{1,2,3\}^2} {0x+0y=0} \\
 O &:=& \setofst {(x,y)∈\{1,2,3\}^2} {0x+0y=2} \\
 P &:=& \setofst {(x,y)∈\{1,2,3\}^2} {x≥y} \\
 \end{array}
$

\msk

6) Represente graficamente:

$\begin{array}{rcl}
 J' &:=& \setofst {(x,y)∈\R^2} {y=2x} \\
 K' &:=& \setofst {(x,y)∈\R^2} {y=x} \\
 L' &:=& \setofst {(x,y)∈\R^2} {y=x/2} \\
 M' &:=& \setofst {(x,y)∈\R^2} {y=x/2+1} \\
 N' &:=& \setofst {(x,y)∈\R^2} {0x+0y=0} \\
 O' &:=& \setofst {(x,y)∈\R^2} {0x+0y=2} \\
 P' &:=& \setofst {(x,y)∈\R^2} {x≥y} \\
 \end{array}
$




%   ____       _                _ _
%  / ___| __ _| |__   __ _ _ __(_) |_ ___
% | |  _ / _` | '_ \ / _` | '__| | __/ _ \
% | |_| | (_| | |_) | (_| | |  | | || (_) |
%  \____|\__,_|_.__/ \__,_|_|  |_|\__\___/
%
% «comprehension-gab» (to ".comprehension-gab")
% (gam181p 8 "comprehension-gab")
% (to "picturedots")
\section{Answers to the exercises}
\label{comprehension-gab}

{\bf Gabarito dos exercícios de set comprehensions}

% \bhbox{$\picturedots(-1,-2)(5,5){ 3,1 3,2 3,3 }$}

1)
$
A = B = C = \picturedots(0,0)(3,4){ 1,4 2,4 1,3 }
\quad
D = \picturedots(0,0)(3,4){ 1,4 2,4 1,3 2,3 }
\quad
E = \picturedots(0,0)(4,4){ 0,3 1,2 2,1 3,0 }
$

\bsk

2)
$     A = \picturedots(0,0)(4,4){     1,2 2,1     }
\quad B = \picturedots(0,0)(4,4){     1,2 2,1 3,0 }
\quad C = \picturedots(0,0)(4,4){ 0,3 1,2 2,1 3,0 }
\quad D = \picturedots(0,0)(4,4){ 0,3 .5,2.5 1,2 1.5,1.5 2,1 2.5,.5 3,0 }
$

\msk

$
\quad E = \picturedots(0,0)(4,4){ 1,3 2,3 3,3   1,4 2,4 3,4 }
\quad F = \picturedots(0,0)(4,4){ 3,1 4,1   3,2 4,2   3,3 4,3 }
\quad G = \picturedots(0,0)(4,4){ 1,3 2,3 3,3   1,4 2,4 3,4 }
\quad H = \picturedots(0,0)(4,4){ 3,2 4,2 }
\quad I = \picturedots(0,0)(4,4){ 1,3 2,3       1,4         }
\quad J = \picturedots(0,0)(4,4){     2,3 3,3   1,4 2,4 3,4 }
$

\msk

$
\quad K = \picturedots(0,0)(4,4){     1,4 2,4 3,4 4,4
                                      1,3 2,3 3,3 4,3
                                      1,2 2,2 3,2 4,2
                                      1,1 2,1 3,1 4,1 }
\quad L = \picturedots(0,0)(4,4){ 0,4 1,4 2,4 3,4 4,4
                                  0,3 1,3 2,3 3,3 4,3
                                  0,2 1,2 2,2 3,2 4,2
                                  0,1 1,1 2,1 3,1 4,1
                                  0,0 1,0 2,0 3,0 4,0 }
\quad M = \picturedots(0,0)(4,4){ 0,3 1,3 2,3 3,3 4,3 }
\quad N = \picturedots(0,0)(4,4){ 2,0 2,1 2,2 2,3 2,4 }
\quad O = \picturedots(0,0)(4,4){ 0,3 1,2 2,1 3,0 }
\quad P = \picturedots(0,0)(4,4){ 0,0 1,1 2,2 3,3 4,4 }
$

\msk

$
\quad Q = \picturedots(0,0)(4,4){ 0,1 1,2 2,3 3,4 }
\quad R = \picturedots(0,0)(4,4){ 0,0 1,2 2,4 }
\quad S = \picturedots(0,0)(4,4){ 0,1 1,3 }
$

\bsk

3)
$     A = \picturedots(0,0)(4,4){ 0,0 1,0  2,0 3,0   }
\quad B = \picturedots(0,0)(4,4){ 0,0 1,.5 2,1 3,1.5 }
\quad C = \picturedots(0,0)(4,4){ 0,0 1,1  2,2 3,3   }
\quad D = \picturedots(0,0)(4,7){ 0,0 1,2  2,4 3,6   }
$

$
\quad E = \picturedots(0,0)(4,4){ 0,1 1,1   2,1 3,1   }
\quad F = \picturedots(0,0)(4,4){ 0,1 1,1.5 2,2 3,2.5 }
\quad G = \picturedots(0,0)(4,4){ 0,1 1,2   2,3 3,4   }
\quad H = \picturedots(0,0)(4,7){ 0,1 1,3   2,5 3,7   }
$

$
\quad I = \picturedots(0,0)(4,4){ 0,2 1,2   2,2 3,2   }
\quad J = \picturedots(0,0)(4,4){ 0,2 1,2.5 2,3 3,3.5 }
\quad K = \picturedots(0,0)(4,4){ 0,2 1,3   2,4 3,5   }
\quad L = \picturedots(0,0)(4,8){ 0,2 1,4   2,6 3,8   }
$

$
\quad M = \picturedots(0,0)(4,4){ 0,2 1,2   2,2 3,2   }
\quad N = \picturedots(0,0)(4,4){ 0,2 1,1.5 2,1 3,.5 }
\quad O = \picturedots(0,-1)(4,4){ 0,2 1,1   2,0 3,-1  }
\quad P = \picturedots(0,-5)(4,3){ 0,2 1,0   2,-2 3,-4   }
$

\bsk

4)
$     A×A = \picturedots(0,0)(4,4){ 1,1 2,1 4,1   1,2 2,2 4,2   1,4 2,4 4,4 }
\quad B×A = \picturedots(0,0)(4,4){ 2,1 3,1       2,2 3,2       2,4 3,4     }
\quad C×A = \picturedots(0,0)(4,4){ 2,1 3,1 4,1   2,2 3,2 4,2   2,4 3,4 4,4 }
$

\msk

$
\quad A×B = \picturedots(0,0)(4,4){ 1,2 2,2 4,2   1,3 2,3 4,3 }
\quad B×B = \picturedots(0,0)(4,4){ 2,2 3,2       2,3 3,3     }
\quad C×B = \picturedots(0,0)(4,4){ 2,2 3,2 4,2   2,3 3,3 4,3 }
$

\msk

$
\quad A×C = \picturedots(0,0)(4,4){ 1,2 2,2 4,2   1,3 2,3 4,3   1,4 2,4 4,4 }
\quad B×C = \picturedots(0,0)(4,4){ 2,2 3,2       2,3 3,3       2,4 3,4     }
\quad C×C = \picturedots(0,0)(4,4){ 2,2 3,2 4,2   2,3 3,3 4,3   2,4 3,4 4,4 }
$

\bsk

5)
$     A = \picturedots(0,0)(4,4){ 0,3 1,3 2,3 3,3
                                  0,2 1,2 2,2 3,2
                                  0,1 1,1 2,1 3,1
                                  0,0 1,0 2,0 3,0 }
\quad B = \picturedots(0,0)(4,4){ 0,2 1,2 2,2 3,2 }
\quad C = \picturedots(0,0)(4,4){ 1,0 1,1 1,2 1,3 }
\quad D = \picturedots(0,0)(4,4){ 0,0 1,1 2,2 3,3 }
\quad E = \picturedots(0,0)(4,4){ 0,0 1,2 2,4 }
$

\msk

$
\quad F = \picturedots(0,0)(4,4){ 0,0 1,2 2,4         }
\quad G = \picturedots(0,0)(4,4){ 0,0 1,1 2,2 3,3 4,4 }
\quad H = \picturedots(0,0)(4,4){ 0,0 2,1 4,2         }
\quad I = \picturedots(0,0)(4,4){ 0,1 2,2 4,3         }
$

\msk

$
\quad J = \picturedots(0,0)(4,4){ 0,0 1,2 2,4         }
\quad K = \picturedots(0,0)(4,4){ 0,0 1,1 2,2 3,3 4,4 }
\quad L = \picturedots(0,0)(4,4){ 0,0 2,1 4,2         }
\quad M = \picturedots(0,0)(4,4){ 0,1 2,2 4,3         }
$

\msk

$
\quad N = \picturedots(0,0)(4,4){ 1,3 2,3 3,3
                                  1,2 2,2 3,2
                                  1,1 2,1 3,1 }
\quad O = \picturedots(0,0)(4,4){             }
\quad P = \picturedots(0,0)(4,4){         3,3
                                      2,2 3,2
                                  1,1 2,1 3,1 }
$






% ------------------------------------------------------------





























































\def\tabl#1{\begin{tabular}{l}#1\end{tabular}}
\def\tablt#1{\begin{tabular}[t]{l}#1\end{tabular}}

\def\und#1#2{\underbrace{#1}_{#2}}
\def\und#1#2{\underbrace{#1}_{\textstyle #2}}
\def\subf#1{\underbrace{#1}_{}}
\def\p{\phantom{(}}

\def\cur{\operatorname{cur}}
\def\uncur{\operatorname{uncur}}
\def\ren{\operatorname{ren}}
\def\app{\operatorname{app}}
\def\pair{\operatorname{pair}}

\def\cur{\mathsf{cur}}
\def\uncur{\mathsf{uncur}}
\def\ren{\mathsf{ren}}
\def\app{\mathsf{app}}
\def\pair{\mathsf{pair}}

% \def∧{\&}

\def\namedfunction#1#2#3#4#5{
  \begin{array}{rrcl}
    #1: & #2 & → & #3 \\
        & #4 & ↦ & #5 \\
  \end{array}
  }

\def\IPLai{\text{IPL}_{{∧}{→}}}
\def\NDai {\text{ND} _{{∧}{→}}}



%  ___       _                 _            _   _             
% |_ _|_ __ | |_ _ __ ___   __| |_   _  ___| |_(_) ___  _ __  
%  | || '_ \| __| '__/ _ \ / _` | | | |/ __| __| |/ _ \| '_ \ 
%  | || | | | |_| | | (_) | (_| | |_| | (__| |_| | (_) | | | |
% |___|_| |_|\__|_|  \___/ \__,_|\__,_|\___|\__|_|\___/|_| |_|
%                                                             
% «introduction» (to ".introduction")
% (lam181p 1 "introduction")
% (laq171 1)
% (laq171 2)

\section{Introduction to lambdas and types}

This is {\sl part} of the material that I've prepared for a very
introductory course on $λ$-calculus, types, intuitionistic
propositional logic, Curry-Howard, Categories, Lisp and Lua... the
course is 2hs/week, has no prerequisites at all, has no homework, and
is usually attended by 2nd/3rd semester CompSci students; they spend
most of their time in class discussing and doing exercises together in
groups on a whiteboard.

I still need to: a) typeset lots of exercises that I wrote directly on
the whiteboard, and some of their solutions --- see:

\par \url{http://angg.twu.net/2017.2-LA/2017.2-LA.pdf} (whiteboards, PDFized)

\par \url{http://angg.twu.net/2017.2-LA.html} (course page)

\noindent and b) write a decent introduction, and c) make this
self-contained.


\msk

{\bf Outline of the course}

Evaluation

Directed graphs

Basic mathematical objects

Variables (and simultaneous substitution)

Functions as their graphs (i.e., as sets of pairs)

Operations like `$Σ$' (including `$λ$')

(and lots more)




Btw:

\par \url{http://angg.twu.net/LATEX/idarct-preprint.pdf}

\par \url{http://angg.twu.net/LATEX/2017planar-has-1.pdf}

\par \url{http://angg.twu.net/math-b.html\#idarct}

\par \url{http://angg.twu.net/math-b.html\#zhas-for-children-2}

\par \url{http://angg.twu.net/logic-for-children-2018.html}

\bsk

Eduardo Ochs, 2017dez20







%  ____       _____           _  _       ____  
% |___ \__  _|___ /     _    | || |__  _| ___| 
%   __) \ \/ / |_ \   _| |_  | || |\ \/ /___ \ 
%  / __/ >  < ___) | |_   _| |__   _>  < ___) |
% |_____/_/\_\____/    |_|      |_|/_/\_\____/ 
%                                              
% «expressions-and-reductions» (to ".expressions-and-reductions")
% (lam181p 1 "expressions-and-reductions")
% (laq171 1)
% (laq171 2)

% \noindent
\section{Expressions (and reductions)}

$$\tablt{
  The usual way to calculate an \\
  expression, one step at a time, \\
  with `$=$'s: \\
  \\
  $\begin{array}[c]{rclcrcl}
  2·3+4·5 &=& 2·3+20 \\
          &=& 6+20   \\
          &=& 26     \\
                     \\
  2·3+4·5 &=& 6+4·5  \\
          &=& 6+20   \\
          &=& 26     \\
  \end{array}$
  \\
  \\
  Each `$=$' corresponds to a `$\diagxyto/->/$' \\
  in the reduction diagram below. \\
  }
  %
  \qquad
  %
  \tablt{
  A notation for calculating the \\
  value of an expression by \\
  calculating the values of all \\
  its subexpressions: \\
  \\
  $\mat{\und{\und{2·3}{6} + \und{4·5}{20}}{26}}$ \\
  \\
  Each `$=$' in the previous diagram \\
  corresponds to applying one `$\subf{}{}$'. \\
  }
$$

\bsk
\bsk

A {\sl reduction diagram} for $2·3+4·5$:

(See Hindley/Seldin, pages 14 and 17)
%
%D diagram 2x4+4x5
%D 2Dx     100  +50  +40
%D 2D  100 A    B
%D 2D
%D 2D  +30 C    D    E
%D 2D
%D ren  A  B      ==>   2·3+4·5   2·3+20
%D ren  C  D  E   ==>     6+4·5     6+20  26
%D (( A B ->   A C -> B D ->
%D    C D ->   D E ->
%D ))
%D enddiagram
%D
\pu
$$\diag{2x4+4x5}$$

Note that when we can choose two subexpressions to calculate

the `$↓$' evaluatess the leftmost one, and the `$→$' evaluates

the rightmost one.


\bsk
\bsk

The {\sl subexpressions} of $2·3+4·5$:

$\subf{\subf{\subf{2}·\subf{3}} +
       \subf{\subf{4}·\subf{5}}
      }
$

\bsk
\msk

Exercise:

Do the same as above for these expressions:

a) $2·(3+4)+5·6$

b) $2+3+4$

c) $2+3+4+5$

(Improvise when needed)



%  _____                                _ _   _                           
% | ____|_  ___ __  _ __ ___  __      _(_) |_| |__   __   ____ _ _ __ ___ 
% |  _| \ \/ / '_ \| '__/ __| \ \ /\ / / | __| '_ \  \ \ / / _` | '__/ __|
% | |___ >  <| |_) | |  \__ \  \ V  V /| | |_| | | |  \ V / (_| | |  \__ \
% |_____/_/\_\ .__/|_|  |___/   \_/\_/ |_|\__|_| |_|   \_/ \__,_|_|  |___/
%            |_|                                                          
%
% «expressions-with-vars» (to ".expressions-with-vars")
% (lam181p 2 "expressions-with-vars")
% (lalp 2)


\section{Expressions with variables}

$\begin{array}{l}
    \text{If $a=5$ and $b=2$, then:} \\[5pt]
    \und{(\und{\und{a}{5} + \und{b}{2}}{7}) ·
         (\und{\und{a}{5} - \und{b}{2}}{3} )
         }{21} \\
  \end{array}
  %
  \qquad
  %
  \begin{array}{l}
    \text{If $a=10$ and $b=1$, then:} \\[5pt]
    \und{(\und{\und{a}{10} + \und{b}{1}}{11}) ·
         (\und{\und{a}{10} - \und{b}{1}}{9} )
         }{99} \\
  \end{array}
$

\bsk
\bsk

We know -- by algebra, which is not for (tiny) children --

that $(a+b)·(a-b) = a·a - b·b$ is true for all $a,b∈\R$

We know -- without algebra -- how to test

``$(a+b)·(a-b) = a·a - b·b$''

for specific values of $a$ and $b$...

\bsk

$\begin{array}{l}
    \text{If $a=5$ and $b=2$, then:} \\[5pt]
    \und{
      \und{(\und{\und{a}{5} + \und{b}{2}}{7}) ·
           (\und{\und{a}{5} - \und{b}{2}}{3})
           }{21}
      =
      \und{\und{\und{a}{5} · \und{a}{5}}{25} -
           \und{\und{b}{2} · \und{b}{2}}{4}
          }{21}
    }{\text{true}} \\
  \end{array}
$

\msk

$\begin{array}{l}
    \text{If $a=10$ and $b=1$, then:} \\[5pt]
    \und{
      \und{(\und{\und{a}{10} + \und{b}{1}}{11}) ·
           (\und{\und{a}{10} - \und{b}{1}} {9})
           }{99}
      =
      \und{\und{\und{a}{10} · \und{a}{10}}{100} -
           \und{\und{b}{1} · \und{b}{1}}{1}
          }{99}
    }{\text{true}} \\
  \end{array}
$


\bsk
\bsk
\bsk

A notation for (simultaneous) substitution:
%
% (phap 13 "logic-in-HAs")
% (pha     "logic-in-HAs")
% (pha     "logic-in-HAs" "simultaneous substitution")
%
$$((x+y)·z) \subst{ 
    x:=a+y \\
    y:=b+z \\
    z:=c+x \\
  }
  \;\;=\;\;
  ((a+y)+(b+z))·(c+x).
$$

Note that $((a+b)·(a-b))\subst{a:=5 \\ b:=2 \\} = (5+2)·(5-2)$.


%  ____        _         _                     _                         
% / ___| _   _| |__  ___| |_    __ _ _ __   __| |   ___ ___  _ __  _   _ 
% \___ \| | | | '_ \/ __| __|  / _` | '_ \ / _` |  / __/ _ \| '_ \| | | |
%  ___) | |_| | |_) \__ \ |_  | (_| | | | | (_| | | (_| (_) | |_) | |_| |
% |____/ \__,_|_.__/|___/\__|  \__,_|_| |_|\__,_|  \___\___/| .__/ \__, |
%                                                           |_|    |___/ 
% «subst-and-copy» (to ".subst-and-copy")
% (lam181p 3 "subst-and-copy")
% (lalp 2)

\section{Operations with substitution and copying}

We know that $Σ_{i=2}^5 \, i^3 = 2^3 + 3^3 + 4^3 + 5^3$.

If we introduce some intermediate steps we get:

\msk

{

\def\IN{\text{ in }}
\def\sto{\squigto\;\;}
\def∧{\mathbin{\&}}

$\begin{array}{l}
 Σ_{i=2}^5 \, i^3 \\
 \sto Σ_{i \IN (2,3,4,5)} \, i^3 \\
 \sto (i^3)[i:=2] + (i^3)[i:=3] + (i^3)[i:=4] + (i^3)[i:=5] \\
 \sto 2^3 + 3^3 + 4^3 + 5^3 \\
 \end{array}
$

\msk

$\begin{array}{l}
 ∀a∈\{2,3,5\}. \, a<4 \\
 \sto ∀a \IN (2,3,5). \, a<4 \\
 \sto (a<4)[a:=2] ∧ (a<4)[a:=3] ∧ (a<4)[a:=5] \\
 \sto (2<4) ∧ (3<4) ∧ (5<4) \\
 \sto \text{false} \\
 \end{array}
$

\msk

$\begin{array}{l}
 ∀a∈\{2,3,3,5\}. \, a<4 \\
 \sto ∀a \IN (2,3,3,5). \, a<4 \\
 \sto (a<4)[a:=2] ∧ (a<4)[a:=3] ∧ (a<4)[a:=3] ∧ (a<4)[a:=5] \\
 \sto (2<4) ∧ (3<4) ∧ (3<4) ∧ (5<4) \\
 \sto \text{false} \\
 \end{array}
$

\msk

$\begin{array}{l}
 \setofst{a^3}{a∈\{2,3,5\}} \\
 \sto \{(a^3)[a:=2], (a^3)[a:=3], (a^3)[a:=5]\} \\
 \sto \{2^3, 3^3, 5^3\} \\
 \end{array}
$

\msk

$\begin{array}{l}
 \setofst{(a,a^3)}{a∈\{2,3,5\}} \\
 \sto \{(a,a^3)[a:=2], (a,a^3)[a:=3], (a,a^3)[a:=5]\} \\
 \sto \{(2,2^3), (3,3^3), (5,5^3)\} \\
 \sto \{(2,8), (3,27), (5,125)\} \\
 \end{array}
$

\msk

{\sl One way} to understand the `$λ$' operator is using the idea ---

from Calculus 1 and Discrete Mathematics -- that a function is

a set of pairs (its ``graph'')...

\msk

$\begin{array}{l}
 λa{:}\{2,3,5\}.\,a^3 \\
 \sto \setofst{(a,a^3)}{a∈\{2,3,5\}} \\
 \sto \{(a,a^3)[a:=2], (a,a^3)[a:=3], (a,a^3)[a:=5]\} \\
 \sto \{(2,2^3), (3,3^3), (5,5^3)\} \\
 \sto \{(2,8), (3,27), (5,125)\} \\
 \end{array}
$

\msk

Note that


\msk

$\begin{array}{l}
 (λa{:}\{2,3,5\}.\,a^3)(5) \\
 \sto (\{(2,2^3), (3,3^3), (5,5^3)\})(5) \\
 \sto 5^3 \\
 \sto 125 \\
 \end{array}
$

\msk

$\begin{array}{l}
 (λa{:}\{2,3,5\}.\,a^3)(4) \\
 \sto (\{(2,2^3), (3,3^3), (5,5^3)\})(4) \\
 \sto \text{error} \\
 \end{array}
$

}



%  _                    _         _       
% | |    __ _ _ __ ___ | |__   __| | __ _ 
% | |   / _` | '_ ` _ \| '_ \ / _` |/ _` |
% | |__| (_| | | | | | | |_) | (_| | (_| |
% |_____\__,_|_| |_| |_|_.__/ \__,_|\__,_|
%                                         
% «lambda» (to ".lambda")
% (lam181p 4 "lambda")
% (lalp 3)
% (laq171 2)
% (laq171 3)

\section{Lambda}

A named function: $g(a) = a·a+4$

An unnamed function: $λa.\,a·a+4$

Let $h = λa.\,a·a+4$.

Then:



%D diagram reduce-g
%D 2Dx     100 +30 +30
%D 2D  100 A ----> B
%D 2D      |       |
%D 2D      v       v
%D 2D  +40 C ----> D
%D 2D      |       |
%D 2D      v       |
%D 2D  +20 E       |
%D 2D      | \     |
%D 2D      |  v    |
%D 2D  +20 |   F   |
%D 2D      |    \  |
%D 2D      v     v v
%D 2D  +20 G ----> H
%D 2D              |
%D 2D              v
%D 2D  +20         I
%D 2D              |
%D 2D              v
%D 2D  +20         J
%D 2D
%D ren  A  B  ==>  g(2+3)       g(5)
%D ren  E  F  ==>  (2+3)·(2+3)+4  (2+3)·5+4
%D ren  G  H  ==>  5·(2+3)+4       5·5+4
%D ren  I  J  ==>  25+4            29
%D (( A B ->   E F -> F H ->   G H ->
%D    A E -> E G ->            B H -> H I -> I J ->
%D ))
%D enddiagram
%D
% $$\Diag{reduce-g}$$

%D diagram reduce-h
%D 2Dx     100 +35 +35
%D 2D  100 A ----> B
%D 2D      |       |
%D 2D      v       v
%D 2D  +20 CL ---> DL
%D 2D      |       |
%D 2D      v       |
%D 2D  +20 CS ---> DS
%D 2D      |       |
%D 2D      v       |
%D 2D  +20 E       |
%D 2D      | \     |
%D 2D      |  v    |
%D 2D  +20 |   F   |
%D 2D      |    \  |
%D 2D      v     v v
%D 2D  +20 G ----> H
%D 2D              |
%D 2D              v
%D 2D  +20         I
%D 2D              |
%D 2D              v
%D 2D  +20         J
%D 2D
%D ren  A  B  ==>  h(2+3)            h(5)
%D ren  CL DL ==>  (λa.\,a·a+4)(2+3) (λa.\,a·a+4)(5)
%D ren  CS DS ==>  (a·a+4)[a:=2+3]   (a·a+4)[a:=5]
%D ren  E  F  ==>  (2+3)·(2+3)+4     (2+3)·5+4
%D ren  G  H  ==>  5·(2+3)+4         5·5+4
%D ren  I  J  ==>  25+4              29
%D (( A B ->   CS DS ->  CL DL ->   E F -> F H ->   G H ->
%D    A CL ->  CL CS ->  CS E -> E G ->
%D    B DL ->  DL DS ->  DS H -> H I -> I J ->
%D ))
%D enddiagram
%D
$$\pu
  \diag{reduce-g}
  \qquad
  \diag{reduce-h}
$$


\bsk

% TODO
% (find-istfile "1.org" "Defining named functions")
% (find-istfile "1.org" "defining unnamed functions")

The usual notation for defining functions is like this:

$$\begin{array}{rrcl}
 f: & \N & → & \R \\
    & n & ↦ & 2+\sqrt{n} \\
 \end{array}
$$


$$\def\t#1{\text{(#1)}}
 \begin{array}{rrcl}
 \t{name}: & \t{domain} & → & \t{codomain} \\
           & \t{variable} & ↦ & \t{expression} \\
 \end{array}
$$

It creates {\sl named} functions

(with domains and codomains).

\msk

The usual notation for creating named functions

without specifying their domains and codomains

is just $f(n) = 2+\sqrt{n}$.

\ssk

Note that this is:
%
$$\def\t#1{\text{(#1)}}
  \begin{array}{cccc}
         f & (\,n\,)            & = & 2+\sqrt{n} \\[5pt]
  \t{name} & (\,\t{variable}\,) & = & \t{expression} \\
  \end{array}
$$


%  _                 _         _                       
% | | __ _ _ __ ___ | |__   __| | __ _    _____  _____ 
% | |/ _` | '_ ` _ \| '_ \ / _` |/ _` |  / _ \ \/ / __|
% | | (_| | | | | | | |_) | (_| | (_| | |  __/>  <\__ \
% |_|\__,_|_| |_| |_|_.__/ \__,_|\__,_|  \___/_/\_\___/
%                                                      
% «lambda-exercises» (to ".lambda-exercises")
% (lam181p 5 "lambda-exercises")

\section{Lambda notation: exercises}

a) $(λa.10a)(2+3)$

b) $(λa.10a)((λb.b+4)(3))$

\msk

Hint: use the speed you're most comfortable with. For example:
%
$$\und{\und{\und{(λa.10a)(\und{\und{\und{(λb.b+4)(3)}{(b+4)[b:=3]}}{3+4}}{7})}
      {(10a)[a:=7]}}{10·7}}{70}
  \qquad
  \und{\und{(λa.10a)(\und{\und{(λb.b+4)(3)}{3+4}}7)}{10·7}}{70}
  \qquad
  \und{(λa.10a)(\und{(λb.b+4)(3)}{7})}{70}
$$

c) $((λa.(λb.10a+b))(3))(4)$

d) $((λf.(λa.f(f(a))))(λx.10x))(7)$

\msk

Hint 2: give names to subexpressions.
%
$$\und{(λa.10a)}{α}(\und{\und{(λb.b+4)}{β}(3)}{γ})
  \qquad
  \begin{array}[t]{rcl}
  α(γ) &=& α(β(3)) \\
       &=& α((λb.b+4)(3)) \\
       &=& α((b+4)[b:=3]) \\
       &=& α(3+4) \\
       &=& α(7) \\
       &=& (λa.10a)(7) \\
       &=& 70 \\
  \end{array}
$$





%   __                  _   _                                     _         
%  / _|_   _ _ __   ___| |_(_) ___  _ __     __ _ _ __ __ _ _ __ | |__  ___ 
% | |_| | | | '_ \ / __| __| |/ _ \| '_ \   / _` | '__/ _` | '_ \| '_ \/ __|
% |  _| |_| | | | | (__| |_| | (_) | | | | | (_| | | | (_| | |_) | | | \__ \
% |_|  \__,_|_| |_|\___|\__|_|\___/|_| |_|  \__, |_|  \__,_| .__/|_| |_|___/
%                                           |___/          |_|              
%
% «function-graphs» (to ".function-graphs")
% (lam181p 6 "function-graphs")
% (lalp 4)

\section{Functions as their graphs}

The {\sl graph} of

$$\begin{array}{rrcl}
 h: & \{-2,-1,0,1,2\} & → & \{0,1,2,3,4\} \\
    & k & ↦ & k^2 \\
 \end{array}
$$

is $\{(-2,4),(-1,1),(0,0),(1,1),(2,4)\}$.

\bsk

We can think that a function {\sl is} its graph,

and that a lambda-expression (with domain) reduces to a graph.

Then $h = \{(-2,4),(-1,1),(0,0),(1,1),(2,4)\}$

and $h(-2) = \{(-2,4),(-1,1),(0,0),(1,1),(2,4)\}(-2) = 4.$

\bsk

Let $h := (λk:\{-2,-1,0,1,2\}.k^2)$.

We have:
%
%D diagram reduce-k2-with-domain
%D 2Dx     100    +90   +70
%D 2D  100        A
%D 2D             |
%D 2D             v
%D 2D  +20 b      B --> C 
%D 2D      |      |     |
%D 2D      v      v     v
%D 2D  +35 d      D --> E
%D 2D      |      |     |
%D 2D      v      v     v
%D 2D  +45 f      F --> G
%D 2D
%D ren  A  B  C   ==>   h(-2)   (λk:\{-2,-1,0,1,2\}.k^2)(-2)    ?
%D ren     D  E   ==>                     \grapha(-2)             (-2)^2
%D ren     F  G   ==>                     \graphb(-2)              4
%D ren  b  d  f   ==>   (λk:\{-2,-1,0,1,2\}.k^2)  \grapha  \graphb
%D (( A B -> B E ->
%D           B D -> # C E ->
%D           D E ->
%D           D F -> E G ->
%D           F G ->
%D    b d -> d f ->
%D ))
%D enddiagram
%D
\pu
$$\def\grapha{\csm{(-2,(-2)^2),\\(-1,(-1)^2),\\(0,0^2),\\(1,1^2),\\(2,2^2)}}
  \def\graphb{\csm{(-2,4),\\(-1,1),\\(0,0),\\(1,1),\\(2,4)}}
  \diag{reduce-k2-with-domain}
$$

\bsk

Note:

the graph of $(λn:\N.n^2)$ has infinite points,

the graph of $(λn:\N.n^2)$ is an infinite set,

the graph of $(λn:\N.n^2)$ can't be written down {\sl explicitly} without `...'s...

\msk

Mathematicians love infinite sets.

Computers hate infinite sets.

For mathematicians a function {\sl is} its graph

($\uparrow$ remember Discrete Mathematics!)

For computer scientists a function {\sl is} is a finite program.

Computer scientists love `$λ$'s!

\msk

{\sl I} love things like this: $\csm{(3,30),\\(4,40)}(3) = 30$


% \end{document}

% The usual notation for defining functions is like this:
% 
%   f: N -> R                      (*)
%      n |-> 2+sqrt(n)
% 
%   name: domain -> codomain
%         variable |-> expression
% 
% It creates _named_ functions.
% 
% To use this notation we have to fill up five slots,
% and use a ":", an "->" and a "|->" in the right places.
% 
% After stating (*) we can "reduce" expressions with f, like this:
% 
%   f(4+5) ---> 2+sqrt(4+5)
%     :            :
%     :            :
%     v            v
%    f(9) ---> 2+sqrt(9) ---> 2+3 ---> 5
% 
% ** DONE $λ$-calculus: defining unnamed functions
% 
% Now compare
% 
%   name: domain -> codomain
%         variable |-> expression   name = \variable.expression
% 
%   g: N  -> R
%      a |-> a*a+4                    h = \a.a*a+4
% 
%   g(2+3) -----------> g(5)   h(2+3) ------------> h(5)
%     |                   |      |                   |
%     |                   |      v                   v
%     |                   |  (\a.a*a+4)(2+3) ---> (\a.a*a+4)(5)
%     |                   |      |                   |
%     v                   |      v                   |
%   (2+3)*(2+3)+4         |    (2+3)*(2+3)+4         |
%         |    \          |          |    \          |
%         |     v         |          |     v         |
%         |   (2+3)*5+4   |          |   (2+3)*5+4   |
%         |          \    |          |          \    |
%         v           v   v          v           v   v
%     5*(2+3)+4 -----> 5*5+4     5*(2+3)+4 -----> 5*5+4
% 





%  _____                      
% |_   _|   _ _ __   ___  ___ 
%   | || | | | '_ \ / _ \/ __|
%   | || |_| | |_) |  __/\__ \
%   |_| \__, | .__/ \___||___/
%       |___/|_|              
%
% «types» (to ".types")
% (lam181p 7 "types")

\section{Types (introduction)}

Let:

$\begin{array}{l}
 A = \{1,2\} \\
 B = \{30,40\}. \\
 \end{array}
$

\ssk

If $f:A→B$, then $f$ is one of these

four functions: 
%
$${\def\f#1 #2 {\sm{1↦#1\\2↦#2}}
 \f 30 30 , \f 30 40 , \f 40 30 , \f 40 40
}
$$

or, in other notation,
%
$${\def\f#1 #2 {\csm{(1,#1)\\(2,#2)}}
 \f 30 30 , \f 30 40 , \f 40 30 , \f 40 40
}
$$

which means that:
%
$$\def\f#1 #2 {\csm{(1,#1)\\(2,#2)}}
  f ∈ \csm{ \f 30 30 , \f 30 40 , \f 40 30 , \f 40 40 }
$$

Let's use the notation ``$A→B$'' for

``the set of all functions from $A$ to $B$''.

\msk

Then $(A→B) =
  \def\f#1 #2 {\csm{(1,#1)\\(2,#2)}}
  \csm{ \f 30 30 , \f 30 40 , \f 40 30 , \f 40 40 }
$

and $f:A→B$

means $f∈(A→B)$.

\msk

In Type Theory and $λ$-calculus ``$a:A$''

is pronounced ``$a$ is of type $A$'', and the meaning

of this is {\sl roughly} ``$a∈B$''.

(We'll see the differences between `$∈$' and `$:$' (much) later).

\msk

Note that:

1. if $f:A→B$ and $a:A$ then $f(a):B$

2. if $a:A$ and $b:B$ then $(a,b):A×B$

3. if $p:A×B$ then $πp:A$ and $π'p:B$, where

`$π$' means `first projection' and

`$π'$' means `second projection';

if $p=(2,30)$ then $πp=2$, $π'p=30$.

\msk

If $p:A×B$ and $g:B→C$, then:
%
\def\und#1#2{\underbrace{#1}_{#2}}
%
$$\und{(\und{π\und{p}{:A×B}}{:A},\;\;
        \und{\und{g}{:B→C}(\und{π'\und{p}{:A×B}}{:B})}{:C})}{:A×C})
$$






%  _                 _         _         _                      
% | | __ _ _ __ ___ | |__   __| | __ _  | |_ _ __ ___  ___  ___ 
% | |/ _` | '_ ` _ \| '_ \ / _` |/ _` | | __| '__/ _ \/ _ \/ __|
% | | (_| | | | | | | |_) | (_| | (_| | | |_| | |  __/  __/\__ \
% |_|\__,_|_| |_| |_|_.__/ \__,_|\__,_|  \__|_|  \___|\___||___/
%                                                               
% «typed-L1-trees» (to ".typed-L1-trees")
% (lam181p 8 "typed-L1-trees")

\section{Typed $λ$-calculus: trees}

$\begin{array}{l}
A = \{1,2\} \\
B = \{3,4\} \\
C = \{30,40\} \\
D = \{10,20\} \\
A×B = \cmat{(1,3),(1,4),\\(2,3),(2,4)} \\
B→C = \cmat{
  \csm{(3,30),\\(4,30)},
  \csm{(3,30),\\(4,40)},
  \csm{(3,40),\\(4,30)},
  \csm{(3,40),\\(4,40)}\\
} \\
\end{array}
$

\bsk

If we know [the values of] $a$, $b$, $f$

then we know [the value of] $(a,f(b))$.

If $(a,b)=(2,3)$ and $f=\csm{(3,30),\\(4,40)}$

then $(a,f(b))=(2,30)$.
%
%:
%:            (a,b)                   (2,3)
%:            -----π'                 -----π'
%:   (a,b)      b      f       (2,3)    3      \cmat{(3,30),(4,40)}
%:   -----π    --------\app    -----π  --------------------------\app
%:     a         f(b)            2              30
%:     --------------\pair       -----------------\pair
%:        (a,f(b))                  (2,30)
%:
%:        ^idxf1                    ^idxf2
%:
$$\pu \ded{idxf1} \qquad \ded{idxf2}$$

\msk

If we know the {\sl types} of $a$, $b$, $f$

we know the type of $(a,f(b))$.

If we know the types of $p$, $f$

we know the type of $(πp,f(π'p))$.

If we know the types of $p$, $f$

we know the type of $(λp:A×B.(πp,f(π'p)))$.



%:
%:               (a,b):A×B                             p:A×B
%:               ---------π'                           -----π'
%:   (a,b):A×B      b:B       f:B→C        p:A×B       π'p:B       f:B→C
%:   ---------π     ---------------\app    ------π     ----------------\app
%:       a:A             f(b):C              πp:A            f(π'p):C
%:       ----------------------\pair         ----------------------\pair
%:              (a,f(b)):A×C                      (πp,f(π'p)):A×C             
%:                                                                             
%:              ^idxf3                             ^idxf4                     
%:
%:
%:              p:A×B
%:              -----π'
%:  p:A×B       π'p:B       f:B→C
%:  ------π     ----------------\app
%:    πp:A            f(π'p):C
%:    ----------------------\pair
%:         (πp,f(π'p)):A×C
%:      -----------------------------λ
%:      (λp:A×B.(πp,f(π'p))):A×B→A×C 
%:                                     
%:          ^idxf5                    
\pu
% $$\ded{idxf3} \qquad \ded{idxf4}$$

$$\ded{idxf3}$$

% $$\ded{idxf4}$$

$$\ded{idxf5}$$




%  _____                                        
% |_   _|   _ _ __   ___  ___ _    _____  _____ 
%   | || | | | '_ \ / _ \/ __(_)  / _ \ \/ / __|
%   | || |_| | |_) |  __/\__ \_  |  __/>  <\__ \
%   |_| \__, | .__/ \___||___(_)  \___/_/\_\___/
%       |___/|_|                                
%
% «types-exercises» (to ".types-exercises")
% (lam181p 9 "types-exercises")

% (lalp 8)

\section{Types: exercises}

Let:

$\begin{array}{l}
A = \{1,2\} \\
B = \{3,4\} \\
C = \{30,40\} \\
D = \{10,20\} \\
f=\csm{(3,30),\\(4,40)} \\
g=\csm{(1,10),\\(2,20)} \\
\end{array}
$

Note that $f:B→C$ and $g:A→D$.

\msk

a) Evaluate $A×B$.

b) Evaluate $A→D$.

c) Evaluate $(πp,f(π'p))$ for each of the four possible values of $p:A×B$.

d) Evaluate $λp{:}A{×}B.(πp,f(π'p))$.

e) Is this true?
%
$$(λp{:}A{×}B.(πp,f(π'p))) = \csm{
  ((1,3),(1,30)), \\
  ((1,4),(1,40)), \\
  ((2,3),(2,30)), \\
  ((2,4),(2,40)) \\
}$$

f) Let $p = (2,3)$. Evaluate $(g(πp),f(π'p))$.

g) Check that if $p:A×B$ then $(g(πp),f(π'p)):D×C$.

h) Check that
$$(λp{:}A{×}B.(g(πp),f(π'p))):A×B→D×C.$$

i) Evaluate $(λp{:}A{×}B.(g(πp),f(π'p)))$.


%  _____                   _        __                              
% |_   _|   _ _ __   ___  (_)_ __  / _| ___ _ __ ___ _ __   ___ ___ 
%   | || | | | '_ \ / _ \ | | '_ \| |_ / _ \ '__/ _ \ '_ \ / __/ _ \
%   | || |_| | |_) |  __/ | | | | |  _|  __/ | |  __/ | | | (_|  __/
%   |_| \__, | .__/ \___| |_|_| |_|_|  \___|_|  \___|_| |_|\___\___|
%       |___/|_|                                                    
%
% «type-inference» (to ".type-inference")
% (lam181p 10 "type-inference")

\section{Type inference}

Here is another notation for checking types:
%
\def\und#1#2{\underbrace{#1}_{#2}}
%
$$\und{(λ\und{p}{:A×B}:A×B.\;\;
       \und{(\und{π\und{p}{:A×B}}{:A},\;\;
             \und{\und{f}{:B→C}(\und{π'\und{p}{:A×B}}{:B})}{:C})}{:A×C})
  }{:A×B→A×C}
$$

Compare it with:
%
$$\ded{idxf5}$$

\bsk


Exercise:

Infer the type of each of the terms below (at the right of the `$:=$').

Use the two notations above.

The types of $f$, $g$, $h$, $k$ are shown in the diagram below.

$\begin{array}{rrcl}
a) &  ({×}C)f &:=& λp{:}A{×}C.(f(πp),π'p) \\
b) &      h^♭ &:=& λq{:}B{×}C.(h(πq))(π'q) \\
c) &     g^♯  &:=& λb{:}B.λc{:}C.g(b,c) \\
d) & (C{→})k &:=& λφ{:}C{→}D.λc{:}C.k(φc) \\
\end{array}
$

\bsk

%D diagram CCC-adj
%D 2Dx      100     +40
%D 2D  100 AxC <--| A
%D 2D       |       |
%D 2D       |  <-|  |
%D 2D       v       v
%D 2D  +30 BxC <--| B
%D 2D       |       |
%D 2D       |  <-|  |
%D 2D       |  |->  |
%D 2D       v       v
%D 2D  +30  D |--> C->D
%D 2D       |       |
%D 2D       |  |->  |
%D 2D       v       v
%D 2D  +30  E |--> C->E
%D 2D
%D ren AxC BxC C->D C->E ==> A{×}C B{×}C C{→}D C{→}E
%D 2D
%D (( AxC A <-|
%D    BxC B <-|
%D    D C->D |->
%D    E C->E |->
%D
%D    A   B   -> .plabel= r f
%D    AxC BxC -> .plabel= l ({×}C)f
%D    AxC B    harrownodes nil 20 nil <-|
%D
%D    BxC D    -> .plabel= l \sm{h^\flat\\g}
%D    B   C->D -> .plabel= r \sm{h\\g^\sharp}
%D    BxC C->D harrownodes nil 20 nil <-| sl^
%D    BxC C->D harrownodes nil 20 nil |-> sl_
%D
%D    D    E    -> .plabel= l k
%D    C->D C->E -> .plabel= r (C{→})k
%D    D    C->E harrownodes nil 20 nil |->
%D ))
%D enddiagram
%D
\pu
$$\diag{CCC-adj}$$




% https://en.wikipedia.org/wiki/Simply_typed_lambda_calculus


%  _____                     _        __                              
% |_   _|__ _ __ _ __ ___   (_)_ __  / _| ___ _ __ ___ _ __   ___ ___ 
%   | |/ _ \ '__| '_ ` _ \  | | '_ \| |_ / _ \ '__/ _ \ '_ \ / __/ _ \
%   | |  __/ |  | | | | | | | | | | |  _|  __/ | |  __/ | | | (_|  __/
%   |_|\___|_|  |_| |_| |_| |_|_| |_|_|  \___|_|  \___|_| |_|\___\___|
%                                                                     
% «term-inference» (to ".term-inference")
% (lam181p 11 "term-inference")

\section{Term inference}

Exercises:

\def\co#1#2{#1:#2}
\def\cp#1#2{#1:#2}
\def\cp#1#2{\phantom{#1}:#2}

%:
%:  \co{p}{A×C}
%:  ----------π
%:  \cp{πp}{A}    \co{f}{A→B}    \co{p}{A×C}
%:  ------------------------\app  ----------π'
%:        \cp{f(πp)}{B}           \cp{π'p}{C}
%:        ------------------------------------\pair
%:              \cp{(f(πp),π'p)}{B×C}
%:        -------------------------------------λ
%:        \cp{λp{:}A{×}C.(f(πp),π'p)}{A×C→B×C}
%:
%:        ^CCC-adj-f
%:
%:                \co{q}{B×C}
%:                -----------π
%:  \co{q}{B×C}    \cp{πq}{B}   \co{h}{B→(C→D)}
%:  -----------π'  ----------------------------\app
%:  \cp{π'q}{C}        \cp{h(πq)}{C→D}
%:  -----------------------------------\app
%:        \cp{h(πq)(π'q)}{D}
%:      ----------------------------------λ
%:      \cp{λq{:}B{×C}.h(πq)(π'q)}{B×C→D}
%:
%:        ^CCC-adj-h
%:
%:    \co{b}{B}  \co{c}{C}
%:    --------------------\pair
%:       \cp{(b,c)}{B×C}         \co{g}{B×C→D}
%:       --------------------------------------\app
%:            \cp{g(b,c)}{D}
%:        ------------------------λ
%:        \cp{λc{:}C.g(b,c)}{C→D}
%:   -----------------------------------λ
%:   \cp{λb{:}B.λc{:}C.g(b,c)}{B→(C→D)}
%:
%:        ^CCC-adj-g
%:
%:     \co{c}{C} \co{φ}{C→D}
%:     ---------------------\app
%:           \cp{φc}{D}           \co{k}{D→E}
%:           ---------------------------------\app
%:                 \cp{k(φc)}{E}
%:           ------------------------λ
%:           \cp{λc{:}C.k(φc)}{(C→E)}
%:  --------------------------------------------λ
%:  \cp{φ{:}C{→}D.λc{:}C.k(φc)}{(C→D)→(C→E)}
%:
%:        ^CCC-adj-k
%:
\pu
$$\ded{CCC-adj-f}$$

$$\ded{CCC-adj-h}$$

$$\ded{CCC-adj-g}$$

$$\ded{CCC-adj-k}$$




%  _____                     _        __                                ____  
% |_   _|__ _ __ _ __ ___   (_)_ __  / _| ___ _ __ ___ _ __   ___ ___  |___ \ 
%   | |/ _ \ '__| '_ ` _ \  | | '_ \| |_ / _ \ '__/ _ \ '_ \ / __/ _ \   __) |
%   | |  __/ |  | | | | | | | | | | |  _|  __/ | |  __/ | | | (_|  __/  / __/ 
%   |_|\___|_|  |_| |_| |_| |_|_| |_|_|  \___|_|  \___|_| |_|\___\___| |_____|
%                                                                             
% «term-inference-answers» (to ".term-inference-answers")
% (lam181p 12 "term-inference-answers")

\section{Term inference: answers}

\def\co#1#2{#1:#2}
\def\cp#1#2{\phantom{#1}:#2}
\def\cp#1#2{#1:#2}

$$\ded{CCC-adj-f}$$

$$\ded{CCC-adj-h}$$

$$\ded{CCC-adj-g}$$

$$\ded{CCC-adj-k}$$



%   ____            _            _       
%  / ___|___  _ __ | |_ _____  _| |_ ___ 
% | |   / _ \| '_ \| __/ _ \ \/ / __/ __|
% | |__| (_) | | | | ||  __/>  <| |_\__ \
%  \____\___/|_| |_|\__\___/_/\_\\__|___/
%                                        
% «contexts» (to ".contexts")
% (lam181p 13 "contexts")

\section{Contexts and `$⊢$'}


Suppose that $A$, $B$, $C$ are known, and are sets.

(Jargon: ``fix sets $A$, $B$, $C$''.)

Then this
%
% (find-angg ".emacs" "laq162" "|-")
% (laq162 14 "20161129" "Coproduct diagram, |-, regras")
%
$$\def\t#1{\text{#1}}
  \def\fooa{\sm{\t{``context'': a series of} \\ \t{declarations like} \\ var:type}}
  \def\foob{\sm{expr:type}} \\
  %
  \und{p:A×B,f:B→C}{\fooa} ⊢ \und{f(π'p):C}{\foob}
$$

Means:

``In this context the expression $expr$ makes sense,
is not \textsf{error},

and its result is of type $type$.''

\ssk

Note that calculating $f(π'p)$ yields \textsf{error}

if we do not know the values of $f$ or $p$.

\msk

What happens if we add contexts to each $term:type$ in a tree?

The two bottom nodes in
%
$$\ded{idxf5}$$

would become:

$$ f:B→C,p:A×B ⊢         (πp,f(π'p))      :A×C $$
$$ f:B→C       ⊢ (λp:A×B.(πp,f(π'p))):A×B→A×C $$

After the rule `$λ$' the `$p$' is no longer needed!

\msk

If we add the contexts and omit the types, the tree becomes:
%
%:              p⊢p
%:              -----π'
%:  p⊢p        p⊢π'p       f⊢f
%:  ------π     ----------------\app
%:  p⊢πp            f,p⊢f(π'p)
%:    ----------------------\pair
%:         f,p⊢(πp,f(π'p))
%:      -----------------------------λ
%:      f⊢(λp{:}A{×}B.(πp,f(π'p)))
%:                                     
%:          ^cont1                    
%:
%:              [p⊢p]^1
%:              -----π'
%:  [p⊢p]^1     p⊢π'p     f⊢f
%:  ------π     ----------------\app
%:  p⊢πp            f,p⊢f(π'p)
%:    ----------------------\pair
%:         f,p⊢(πp,f(π'p))
%:      -----------------------------λ;1
%:      f⊢(λp{:}A{×}B.(πp,f(π'p)))
%:                                     
%:          ^cont2
%:
%:           [p]^1
%:           -----π'
%:  [p]^1     π'p     f
%:  ------π   ----------\app
%:  πp            f(π'p)
%:  ---------------------\pair
%:        (πp,f(π'p))
%:  -----------------------------λ;1
%:   (λp{:}A{×}B.(πp,f(π'p)))
%:                                     
%:          ^cont3
%:
\pu
$$\ded{cont1} \quad\squigto\qquad \ded{cont3}$$

Notational trick:

below the bar `$λ;1$' the value of $p$ is no longer needed;

we say that the $p$ is ``discharged'' (from the list of hypotheses)

and we mark the `$p$' on the leaves of the tree with `$[·]^1$';

a `$[·]^1$' on a hypothesis means: ``below the bar `$λ;1$' I am

no longer a hypothesis''.







\end{document}

% Local Variables:
% coding: utf-8-unix
% End:
