|
Warning: this is an htmlized version!
The original is here, and the conversion rules are here. |
% (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: