|
Warning: this is an htmlized version!
The original is here, and the conversion rules are here. |
% (find-angg "LATEX/2017-2-LA-material.tex")
% (defun c () (interactive) (find-LATEXsh "lualatex -record 2017-2-LA-material.tex"))
% (defun d () (interactive) (find-xpdfpage "~/LATEX/2017-2-LA-material.pdf"))
% (defun b () (interactive) (find-zsh "bibtex 2017-2-LA-material; makeindex 2017-2-LA-material"))
% (defun b () (interactive) (find-zsh "bibtex 2017-2-LA-material"))
% (defun e () (interactive) (find-LATEX "2017-2-LA-material.tex"))
% (defun u () (interactive) (find-latex-upload-links "2017-2-LA-material"))
% (find-xpdfpage "~/LATEX/2017-2-LA-material.pdf")
% (find-sh0 "cp -v ~/LATEX/2017-2-LA-material.pdf /tmp/")
% (find-sh0 "cp -v ~/LATEX/2017-2-LA-material.pdf /tmp/pen/")
% file:///home/edrx/LATEX/2017-2-LA-material.pdf
% file:///tmp/2017-2-LA-material.pdf
% file:///tmp/pen/2017-2-LA-material.pdf
% http://angg.twu.net/LATEX/2017-2-LA-material.pdf
% Index: (lam172i)
% «.introduction» (to "introduction")
%
% «.expressions-and-reductions» (to "expressions-and-reductions")
% «.expressions-with-vars» (to "expressions-with-vars")
% «.subst-and-copy» (to "subst-and-copy")
% «.lambda» (to "lambda")
% «.lambda-exercises» (to "lambda-exercises")
% «.function-graphs» (to "function-graphs")
% «.types» (to "types")
% «.typed-L1-trees» (to "typed-L1-trees")
% «.types-exercises» (to "types-exercises")
% «.type-inference» (to "type-inference")
% «.term-inference» (to "term-inference")
% «.term-inference-answers» (to "term-inference-answers")
% «.contexts» (to "contexts")
% «.curry-howard-0» (to "curry-howard-0")
% «.curry-howard-1» (to "curry-howard-1")
% «.ZHAs-1» (to "ZHAs-1")
% «.algebraic-structures» (to "algebraic-structures")
% «.protocategories» (to "protocategories")
%
% «.composition» (to "composition")
% «.lateral-inverses» (to "lateral-inverses")
% «.multiple-inverses» (to "multiple-inverses")
% «.no-inverses» (to "no-inverses")
% «.products» (to "products")
% «.exponentials» (to "exponentials")
\documentclass[oneside]{book}
\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"} % (find-LATEX "dednat6load.lua")
\def\Diag#1{\pu\diag{#1}}
%L addabbrevs("\"", " ")
\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
\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} _{{∧}{→}}}
% ____ _____ _ _ ____
% |___ \__ _|___ / _ | || |__ _| ___|
% __) \ \/ / |_ \ _| |_ | || |\ \/ /___ \
% / __/ > < ___) | |_ _| |__ _> < ___) |
% |_____/_/\_\____/ |_| |_|/_/\_\____/
%
% «expressions-and-reductions» (to ".expressions-and-reductions")
% (lam172p 1 "expressions-and-reductions")
% (laq171 1)
% (laq171 2)
% \noindent
{\bf 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)
\newpage
% _____ _ _ _
% | ____|_ ___ __ _ __ ___ __ _(_) |_| |__ __ ____ _ _ __ ___
% | _| \ \/ / '_ \| '__/ __| \ \ /\ / / | __| '_ \ \ \ / / _` | '__/ __|
% | |___ > <| |_) | | \__ \ \ V V /| | |_| | | | \ V / (_| | | \__ \
% |_____/_/\_\ .__/|_| |___/ \_/\_/ |_|\__|_| |_| \_/ \__,_|_| |___/
% |_|
%
% «expressions-with-vars» (to ".expressions-with-vars")
% (lam172p 2 "expressions-with-vars")
% (lalp 2)
{\bf Expressions with variables}
\ssk
$\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)$.
\newpage
% ____ _ _ _
% / ___| _ _| |__ ___| |_ __ _ _ __ __| | ___ ___ _ __ _ _
% \___ \| | | | '_ \/ __| __| / _` | '_ \ / _` | / __/ _ \| '_ \| | | |
% ___) | |_| | |_) \__ \ |_ | (_| | | | | (_| | | (_| (_) | |_) | |_| |
% |____/ \__,_|_.__/|___/\__| \__,_|_| |_|\__,_| \___\___/| .__/ \__, |
% |_| |___/
% «subst-and-copy» (to ".subst-and-copy")
% (lam172p 3 "subst-and-copy")
% (lalp 2)
{\bf Operations with substitution and copying}
\ssk
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}
$
}
\newpage
% _ _ _
% | | __ _ _ __ ___ | |__ __| | __ _
% | | / _` | '_ ` _ \| '_ \ / _` |/ _` |
% | |__| (_| | | | | | | |_) | (_| | (_| |
% |_____\__,_|_| |_| |_|_.__/ \__,_|\__,_|
%
% «lambda» (to ".lambda")
% (lam172p 4 "lambda")
% (lalp 3)
% (laq171 2)
% (laq171 3)
{\bf Lambda}
\ssk
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}
$$
\newpage
% _ _ _
% | | __ _ _ __ ___ | |__ __| | __ _ _____ _____
% | |/ _` | '_ ` _ \| '_ \ / _` |/ _` | / _ \ \/ / __|
% | | (_| | | | | | | |_) | (_| | (_| | | __/> <\__ \
% |_|\__,_|_| |_| |_|_.__/ \__,_|\__,_| \___/_/\_\___/
%
% «lambda-exercises» (to ".lambda-exercises")
% (lam172p 5 "lambda-exercises")
{\bf Lambda notation: exercises}
\ssk
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}
$$
\newpage
% __ _ _ _
% / _|_ _ _ __ ___| |_(_) ___ _ __ __ _ _ __ __ _ _ __ | |__ ___
% | |_| | | | '_ \ / __| __| |/ _ \| '_ \ / _` | '__/ _` | '_ \| '_ \/ __|
% | _| |_| | | | | (__| |_| | (_) | | | | | (_| | | | (_| | |_) | | | \__ \
% |_| \__,_|_| |_|\___|\__|_|\___/|_| |_| \__, |_| \__,_| .__/|_| |_|___/
% |___/ |_|
%
% «function-graphs» (to ".function-graphs")
% (lam172p 6 "function-graphs")
% (lalp 4)
{\bf Functions as their graphs}
\ssk
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
%
\newpage
% _____
% |_ _| _ _ __ ___ ___
% | || | | | '_ \ / _ \/ __|
% | || |_| | |_) | __/\__ \
% |_| \__, | .__/ \___||___/
% |___/|_|
%
% «types» (to ".types")
% (lam172p 7 "types")
{\bf Types (introduction)}
\ssk
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})
$$
\newpage
% _ _ _ _
% | | __ _ _ __ ___ | |__ __| | __ _ | |_ _ __ ___ ___ ___
% | |/ _` | '_ ` _ \| '_ \ / _` |/ _` | | __| '__/ _ \/ _ \/ __|
% | | (_| | | | | | | |_) | (_| | (_| | | |_| | | __/ __/\__ \
% |_|\__,_|_| |_| |_|_.__/ \__,_|\__,_| \__|_| \___|\___||___/
%
% «typed-L1-trees» (to ".typed-L1-trees")
% (lam172p 8 "typed-L1-trees")
{\bf Typed $λ$-calculus: trees}
\ssk
$\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}$$
\bsk
\newpage
% _____
% |_ _| _ _ __ ___ ___ _ _____ _____
% | || | | | '_ \ / _ \/ __(_) / _ \ \/ / __|
% | || |_| | |_) | __/\__ \_ | __/> <\__ \
% |_| \__, | .__/ \___||___(_) \___/_/\_\___/
% |___/|_|
%
% «types-exercises» (to ".types-exercises")
% (lam172p 9 "types-exercises")
% (lalp 8)
{\bf Types: exercises}
\msk
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)))$.
\newpage
% _____ _ __
% |_ _| _ _ __ ___ (_)_ __ / _| ___ _ __ ___ _ __ ___ ___
% | || | | | '_ \ / _ \ | | '_ \| |_ / _ \ '__/ _ \ '_ \ / __/ _ \
% | || |_| | |_) | __/ | | | | | _| __/ | | __/ | | | (_| __/
% |_| \__, | .__/ \___| |_|_| |_|_| \___|_| \___|_| |_|\___\___|
% |___/|_|
%
% «type-inference» (to ".type-inference")
% (lam172p 10 "type-inference")
{\bf Type inference}
\ssk
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
\newpage
% _____ _ __
% |_ _|__ _ __ _ __ ___ (_)_ __ / _| ___ _ __ ___ _ __ ___ ___
% | |/ _ \ '__| '_ ` _ \ | | '_ \| |_ / _ \ '__/ _ \ '_ \ / __/ _ \
% | | __/ | | | | | | | | | | | | _| __/ | | __/ | | | (_| __/
% |_|\___|_| |_| |_| |_| |_|_| |_|_| \___|_| \___|_| |_|\___\___|
%
% «term-inference» (to ".term-inference")
% (lam172p 11 "term-inference")
{\bf Term inference}
\ssk
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}$$
\newpage
% _____ _ __ ____
% |_ _|__ _ __ _ __ ___ (_)_ __ / _| ___ _ __ ___ _ __ ___ ___ |___ \
% | |/ _ \ '__| '_ ` _ \ | | '_ \| |_ / _ \ '__/ _ \ '_ \ / __/ _ \ __) |
% | | __/ | | | | | | | | | | | | _| __/ | | __/ | | | (_| __/ / __/
% |_|\___|_| |_| |_| |_| |_|_| |_|_| \___|_| \___|_| |_|\___\___| |_____|
%
% «term-inference-answers» (to ".term-inference-answers")
% (lam172p 12 "term-inference-answers")
{\bf 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}$$
\newpage
% ____ _ _
% / ___|___ _ __ | |_ _____ _| |_ ___
% | | / _ \| '_ \| __/ _ \ \/ / __/ __|
% | |__| (_) | | | | || __/> <| |_\__ \
% \____\___/|_| |_|\__\___/_/\_\\__|___/
%
% «contexts» (to ".contexts")
% (lam172p 13 "contexts")
{\bf Contexts and `$⊢$'}
\ssk
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''.
\newpage
% ____ _ _ ___
% / ___| _ _ __ _ __ _ _ | | | | _____ __ / _ \
% | | | | | | '__| '__| | | |_____| |_| |/ _ \ \ /\ / / | | | |
% | |__| |_| | | | | | |_| |_____| _ | (_) \ V V / | |_| |
% \____\__,_|_| |_| \__, | |_| |_|\___/ \_/\_/ \___/
% |___/
%
% «curry-howard-0» (to ".curry-howard-0")
% (lam172p 14 "curry-howard-0")
{\bf Curry-Howard: introduction}
\ssk
\par We are learning a system called
\par ``the simply-typed $λ$-calculus (with binary products)'' ---
\par system $λ1$, for short.
\msk
\par In $λ1$ in its fullest form,
\par its objects are trees of `$\ldots⊢term:type$'s,
\par but we saw (evidence) that we can:
\par • reconstruct the full tree from just the `$term:type$'s,
\par • write just `$:type$'s (except on the leaves, to get the var names),
\par • reconstruct the full tree from just the bottom `$term:type$'...
\msk
For example, we can reconstruct the whole tree,
{\sl with contexts}, from:
%
%: [p:A{×}B]^1
%: ---------π'
%: [p:A{×}B]^1 :B f:B→C
%: ------π ----------------\app
%: :A :C
%: ----------------------\pair
%: :A{×}C
%: ---------λ
%: :A{×}B→A{×}C
%:
%: ^curryhow1
%:
$$\pu\ded{curryhow1}$$
\par If we erase the terms and the `:'s and leave only the types,
\par we get something that is strikingly similar to a tree in
\par Natural Deduction,
%
%: [A{×}B]^1
%: ---------π'
%: [A{×}B]^1 B B→C
%: ------π --------------\app
%: A C
%: ------------------\pair
%: A{×}C
%: ---------λ
%: A{×}B→A{×}C
%:
%: ^curryhow2
%:
%: [P{∧}Q]^1
%: ---------∧E_2
%: [P{∧}Q]^1 Q Q{→}R
%: ------{∧}E_1 -----------------{→}E
%: P R
%: ------------------∧I
%: P{∧}R
%: ---------{→}I;1
%: P{∧}R→P{∧}Q
%:
%: ^curryhow3
%:
\pu
$$\ded{curryhow2}$$
$$\squigto \qquad \cded{curryhow3}$$
which talks about {\sl logic}.
\newpage
% ____ _ _ _
% / ___| _ _ __ _ __ _ _ | | | | _____ __ / |
% | | | | | | '__| '__| | | |_____| |_| |/ _ \ \ /\ / / | |
% | |__| |_| | | | | | |_| |_____| _ | (_) \ V V / | |
% \____\__,_|_| |_| \__, | |_| |_|\___/ \_/\_/ |_|
% |___/
%
% «curry-howard-1» (to ".curry-howard-1")
% (lam172p 15 "curry-howard-1")
{\bf Curry-Howard: Natural Deduction}
\ssk
The tree
%: [P{∧}Q]^1
%: ---------∧E_2
%: [P{∧}Q]^1 Q Q{→}R
%: ------{∧}E_1 -----------------{→}E
%: P R
%: ------------------{∧}I
%: P{∧}R
%: ---------{→}I;1
%: P{∧}R→P{∧}Q
%:
%: ^curryhow3
%:
\pu
$$\ded{curryhow3}$$
is in $\NDai$ (or in $\IPLai$), the fragment of
Natural Deduction (or intuitionistic predicate logic)
that only has the connectives $∧$ and $→$.
\msk
Its rules are:
%:
%: P Q P∧Q P∧Q
%: ----{∧}I ----{∧}E_1 ---{∧}E_2
%: P∧Q P Q
%:
%: ^ndai ^ndae1 ^ndae2
%:
%: P [Q]^1
%: ::::::::
%: R P P→Q
%: -------{→}I;1 -------{→}E
%: Q→R Q
%:
%: ^ndii ^ndie
%:
\pu
$$\ded{ndai} \qquad \ded{ndae1} \qquad \ded{ndae2}$$
$$\ded{ndii} \qquad \ded{ndie}$$
\bsk
New rules (for $⊤$, $⊥$, $∨$):
(not yet --- see the whiteboard for 20170418)
% (laq171 9 "20170418" "ND: provando certas coisas vindas de diagramas; regras")
\newpage
% ______ _ _ _
% |__ / | | | / \ ___ / |
% / /| |_| | / _ \ / __| | |
% / /_| _ |/ ___ \\__ \ | |
% /____|_| |_/_/ \_\___/ |_|
%
% «ZHAs-1» (to ".ZHAs-1")
% (lam172p 16 "ZHAs-1")
% (laq171 11 "20170425" "Lógica em ZHAs")
{\bf Planar Heyting Algebras}
\ssk
Read sections 2--8 of:
\url{http://angg.twu.net/LATEX/2017planar-has.pdf}
% (pha)
% (phap)
\msk
%L local mp = mpnew({def="foo", scale="7pt", meta="s"}, "12321L")
%L mp:addlrs():output()
\pu
Let $B=\foo$ .
Exercises:
Calculate, and represent in positional notation when possible:
\ssk
\def\o#1{\mathop{\mathsf{#1}}}
\def\o#1{\mathbin{\mathsf{#1}}}
\def∧{\land}
\par a) $λlr{:}B.l$
\par b) $λlr{:}B.r$
\par c) $λlr{:}B.(l≤1)$
\par d) $λlr{:}B.(r≥1)$
\par e) $λlr{:}B.lr≤11$
\par f) $λlr{:}B.lr∧12$
\par g) $λlr{:}B.\o{valid}(\ang{l+1,r})$
\par h) $λlr{:}B.lr \o{leftof} 11$
\par i) $λlr{:}B.lr \o{leftof} 12$
\par j) $λlr{:}B.lr \o{above} 11$
\par k) $λlr{:}B.\o{ne}(lr)$
\par l) $λlr{:}B.\o{nw}(lr)$
\ssk
\par m) $20→11$
\par n) $02→11$
\par o) $22→11$
\par p) $00→11$
\ssk
\par q) $λlr{:}B.¬lr$
\par r) $λlr{:}B.¬¬lr$
\par s) $λlr{:}B.(lr=¬¬lr)$
\newpage
% _ _ _ _
% / \ | | __ _ ___| |_ _ __ _ _ ___| |_ ___
% / _ \ | |/ _` | / __| __| '__| | | |/ __| __/ __|
% / ___ \| | (_| | \__ \ |_| | | |_| | (__| |_\__ \
% /_/ \_\_|\__, | |___/\__|_| \__,_|\___|\__|___/
% |___/
%
% «algebraic-structures» (to ".algebraic-structures")
% (lam172p 17 "algebraic-structures")
{\bf Algebraic structures}
\ssk
A {\sl ring} is a 6-uple
%
$$(R, 0_R, 1_R, +_R, -_R, ·_R)$$
where $R, 0_R, \ldots, ·_R$ have the following types,
\msk
\par \quad $R$ is a set,
\par \quad $0_R∈R$,
\par \quad $1_R∈R$,
\par \quad $+_R:R×R→R$,
\par \quad $-_R:R→R$ (unary minus),
\par \quad $·_R:R×R→R$,
\msk
and where the components obey these equations ($∀a,b,c∈R$):
\msk
\par \quad $a+0_R = 0_R+a = a$, \; $a+b=b+a$, \; $a+(b+c) = (a+b)+c$, \; $a+(-a) = 0$,
\par \quad $a·1_R = 1_R·a = a$, \; $a·b=b·a$, \; $a·(b·c) = (a·b)·c$,
\par \quad $a·(b+c) = a·b+a·c$.
\msk
A {\sl proto-ring} is a 6-uple $(R, 0_R, 1_R, +_R, -_R, ·_R)$
that obeys the typing conditions of a ring.
A {\sl ring} is a proto-ring plus the assurance that it obeys the ring equations.
\bsk
% (ebsp 9 "HAs")
% (ebs "HAs")
A {\sl proto-Heyting Algebra} is a 7-uple
$$H = (Ω,≤_H,⊤_H,⊥_H,∧_H,∨_H,→_H)$$
\msk
in which:
\msk
\par \quad $Ω$ is a set (the ``set of truth values''),
\par \quad $≤_H ⊂ Ω×Ω$ (partial order),
\par \quad $⊤_H ∈ Ω$,
\par \quad $⊥_H ∈ Ω$,
\par \quad $∧_H:Ω×Ω→Ω$
\par \quad $∨_H:Ω×Ω→Ω$
\par \quad $→_H:Ω×Ω→Ω$
\msk
Sometimes we add operations `$¬$' and `$↔$' to a (proto-)HA $H$,
%
$$H = (Ω,≤_H,⊤_H,⊥_H,∧_H,∨_H,→_H,¬_H,↔_H)$$
by {\sl defining them} as $¬P:=P→⊥$ and $P↔Q:=(P→Q)∧(Q→P)$
(i.e., $¬_H P:=P →_H ⊥_H$
and $P ↔_H Q := (P →_H Q) ∧_H (Q →_H P)$).
\bsk
\bsk
This abuse of language is very common:
$R$ ``$=$'' $(R, 0_R, 1_R, +_R, -_R, ·_R)$.
\newpage
% ____ _ _
% | _ \ _ __ ___ | |_ ___ ___ __ _| |_ ___
% | |_) | '__/ _ \| __/ _ \ / __/ _` | __/ __|
% | __/| | | (_) | || (_) | (_| (_| | |_\__ \
% |_| |_| \___/ \__\___/ \___\__,_|\__|___/
%
% «protocategories» (to ".protocategories")
% (lam172p 18 "protocategories")
{\bf Protocategories}
\ssk
A {\sl protocategory} is a 4-uple
%
$$\catC = (\catC_0, \Hom_\catC, \id_\catC, ∘_\catC)$$
where
\msk
\par \quad $\catC_0$ is a set (more precisely a ``class''),
\par \quad $\Hom_\catC : \catC_0×\catC_0 → \Sets$,
\par \quad $\id_\catC(A) ∈ \Hom_\catC(A,A)$,
\par \quad $(∘_\catC)_{ABC}: \Hom_\catC(B,C) × \Hom_\catC(A,B) → \Hom_\catC(A,C)$.
\msk
A {\sl category} is a protocategory plus the assurance that
identities behave as expected and composition is associative.
\msk
Sometimes we add an operation `;' to a category,
$$\catC = (\catC_0, \Hom_\catC, \id_\catC, ∘_\catC, ;_\catC)$$
where `;' is the composition in other order: $f∘g$ = $g;f$.
% (find-books "__cats/__cats.el" "awodey")
% (find-books "__cats/__cats.el" "maclane")
\newpage
% ------------------------------------------------------------
\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\app{\operatorname{app}}
\def\ren{\operatorname{ren}}
\def∧{\&}
\def\namedfunction#1#2#3#4#5{
\begin{array}{rrcl}
#1: & #2 & → & #3 \\
& #4 & ↦ & #5 \\
\end{array}
}
% ------------------------------------------------------------
% _ _ _
% ___ ___ _ __ ___ _ __ ___ ___(_) |_(_) ___ _ __
% / __/ _ \| '_ ` _ \| '_ \ / _ \/ __| | __| |/ _ \| '_ \
% | (_| (_) | | | | | | |_) | (_) \__ \ | |_| | (_) | | | |
% \___\___/|_| |_| |_| .__/ \___/|___/_|\__|_|\___/|_| |_|
% |_|
%
% «composition» (to ".composition")
% (lac162p 1 "composition")
Composition
(is associative)
%L mapstos_1 = function (str)
%L local n, latex = 0, ""
%L for d in str:gmatch("%d") do
%L latex = latex .. format("%d \\mapsto %d \\\\\n", n, d)
%L n = n + 1
%L end
%L return latex
%L end
%L
%L mapstos_2 = function (str)
%L local latex = ""
%L for a,b in str:gmatch("(%d)(%d)") do
%L latex = latex .. format("%d \\mapsto %d \\\\\n", a, b)
%L end
%L return latex
%L end
\pu
\def\mapsb #1{\sm{\expr{mapstos_1("#1")}}}
\def\mapsab#1{\sm{\expr{mapstos_2("#1")}}}
% \bsk
%D diagram ??
%D 2Dx 100 +35 +35 +35 +35 +35
%D 2D 100 A --> B a --> b
%D 2D | |
%D 2D v v
%D 2D +35 C --> D c --> d
%D 2D
%D ren a b ==> \{1,2\} \{3,4\}
%D ren c d ==> \{5,6\} \{7,8\}
%D (( A B -> .plabel= a f
%D B C -> .plabel= m g
%D C D -> .plabel= b h
%D A C -> .plabel= l (g∘f=)\;\;f;g
%D B D -> .plabel= r g;h\;\;(=h∘g)
%D
%D a b -> .plabel= a \mapsab{13,24}
%D b c -> .plabel= m \mapsab{36,45}
%D c d -> .plabel= b \mapsab{57,67}
%D a c -> b d ->
%D ))
%D enddiagram
%D
$$\pu
\diag{??}
$$
\bsk
%D diagram composition-1
%D 2Dx 100 +30 +30 +30
%D 2D 100 D <-- C <-- B <-- A
%D 2D
%D (( D A <- .plabel= a (h∘g)∘f .slide= 22pt
%D D B <- .plabel= a h∘g .slide= 10pt
%D D C <- .plabel= m h C B <- .plabel= m g B A <- .plabel= m f
%D C A <- .plabel= b g∘f .slide= -10pt
%D D A <- .plabel= b h∘(g∘f) .slide= -22pt
%D ))
%D enddiagram
%D
%
$$\begin{array}{rcl}
((h∘g)∘f)(a) &=& (h∘g)(f(a)) \\
&=& h(g(f(a))) \\
&=& h((g∘f)(a)) \\
&=& (h∘(g∘f))(a) \\[5pt]
((h∘g)∘f)(a) &=& (h∘(g∘f))(a) \\[5pt]
(h∘g)∘f &=& h∘(g∘f) \\
\end{array}
\qquad
\Diag{composition-1}
$$
\bsk
\bsk
Identities:
If $f:A→B$ then $\id_A;f = f = f;\id_B$
%D diagram ??
%D 2Dx 100 +35 +35 +35 +35 +35
%D 2D 100 A --> B a --> b
%D 2D | |
%D 2D v v
%D 2D +35 C --> D c --> d
%D 2D
%D ren A B ==> A A
%D ren C D ==> B B
%D ren a b ==> \{1,2\} \{1,2\}
%D ren c d ==> \{3,4\} \{3,4\}
%D (( A B -> .plabel= a \id_A
%D B C -> .plabel= m f
%D C D -> .plabel= b \id_B
%D A C -> .plabel= l f\;=\;\id_A;f
%D B D -> .plabel= r f;\id_B\;=\;f
%D
%D a b -> .plabel= a \mapsab{11,22}
%D b c -> .plabel= m \mapsab{13,24}
%D c d -> .plabel= b \mapsab{33,44}
%D a c -> b d ->
%D ))
%D enddiagram
%D
$$\pu
\diag{??}
$$
\bsk
\bsk
% «lateral-inverses» (to ".lateral-inverses")
A theorem about lateral inverses:
If $f;g = \id$ and $g;h=\id$ then $f=h$
%D diagram ??
%D 2Dx 100 +35 +35 +35 +35 +35
%D 2D 100 A --> B a --> b
%D 2D | |
%D 2D v v
%D 2D +35 C --> D c --> d
%D 2D
%D ren A B ==> B A
%D ren C D ==> B A
%D ren a b ==> \{1,2\} \{1,2\}
%D ren c d ==> \{3,4\} \{3,4\}
%D (( A B -> .plabel= a f
%D B C -> .plabel= m g
%D C D -> .plabel= b h
%D A C -> .plabel= l \id_B\;=\;f;g
%D B D -> .plabel= r \id_A\;=\;g;h
%D
%D # a b -> .plabel= a \mapsab{11,22}
%D # b c -> .plabel= m \mapsab{13,24}
%D # c d -> .plabel= b \mapsab{33,44}
%D # a c -> b d ->
%D ))
%D enddiagram
%D
$$\pu
\diag{??}
\qquad
\begin{array}{rcl}
\multicolumn {3}{c} {(f;g);h = \id_B;h = h} \\
\multicolumn {3}{c} {f;(g;h) = f;\id_A = f} \\[5pt]
f &=& f;\id_A \\
&=& f;(g;h) \\
&=& (f;g);h \\
&=& \id_B;h \\
&=& h
\end{array}
$$
\newpage
% «multiple-inverses» (to ".multiple-inverses")
% (lac162p 2 "multiple-inverses")
Multiple inverses
%L forths["->>"] = function () pusharrow("->>") end
%D diagram ??
%D 2Dx 100 +35 +35 +35
%D 2D 100 A --> B D
%D 2D | |
%D 2D v v
%D 2D +35 C E --> F
%D 2D
%D ren A B D ==> \{1,2\} \{3,4,5\} \{5,6\}
%D ren C E F ==> \{1,2\} \{7,8,9\} \{5,6\}
%D (( A B >-> sl^ .plabel= a ? A B >-> sl_ .plabel= b ?
%D B C ->> .plabel= r \mapsab{31,42,52}
%D A C -> .plabel= l \id
%D
%D D E ->> .plabel= l \mapsab{57,68}
%D E F >-> sl^ .plabel= a ? E F >-> sl_ .plabel= b ?
%D D F -> .plabel= r \id
%D ))
%D enddiagram
%D
$$\pu
\diag{??}
$$
\bsk
\bsk
\def\frown{=(}
% «no-inverses» (to ".no-inverses")
No inverses
%D diagram ??
%D 2Dx 100 +35 +35 +10 +35 +35
%D 2D 100 A --> B E --> F
%D 2D | |
%D 2D v v
%D 2D +35 C --> D G --> H
%D 2D
%D ren A B E F ==> \{3,4,5\} \{1,2\} \{8,9\} \{5,6,7\}
%D ren C D G H ==> \{3,4,5\} \{1,2\} \{8,9\} \{5,6,7\}
%D (( A B -> .plabel= a \frown
%D B C >-> .plabel= m \mapsab{13,24}
%D A C -> .plabel= l \id
%D C D ->> sl^ C D ->> sl_
%D B D -> .plabel= r \id
%D
%D E G -> .plabel= l \id
%D E F >-> sl^ E F >-> sl_
%D F G ->> .plabel= m \mapsab{58,69,79}
%D G H -> .plabel= b \frown
%D F H -> .plabel= r \id
%D ))
%D enddiagram
%D
$$\pu
\diag{??}
$$
%D diagram ??
%D 2Dx 100 +35 +35
%D 2D 100 A --> B
%D 2D |
%D 2D v
%D 2D +35 C --> D
%D 2D
%D ren A B ==> \{4,5,6\} \{1,2,3\}
%D ren C D ==> \{4,5,6\} \{1,2,3\}
%D (( A B -> .plabel= a \frown
%D B C -> .plabel= m \mapsab{14,25,35}
%D C D -> .plabel= r \frown
%D A C -> .plabel= l \id
%D B D -> .plabel= r \id
%D ))
%D enddiagram
%D
$$\pu
\diag{??}
$$
\bsk
\bsk
\bsk
% «products» (to ".products")
% (lac162p 2 "products")
{\bf Products}
Property: $∀f,g.∃!h.(f=h;π\;∧\;g=h;π')$
Solution: $h=λa:A.(f(a),g(a))$
Bijection: $(f,g)↔h$
$(→)$: $λ(f,g).(λa:A.(f(a),g(a)))$
$(←)$: $λh.((h;π),(h;π'))$
\bsk
%D diagram product-ABC
%D 2Dx 100 +45 +45
%D 2D 100 A
%D 2D |
%D 2D v
%D 2D +45 B <-- BxC --> C
%D 2D
%D ren A ==> A
%D ren B BxC C ==> B B×C C
%D
%D (( A B -> .plabel= l f
%D A BxC -> .plabel= m h
%D A C -> .plabel= r g
%D B BxC <- .plabel= b π\mathstrut
%D BxC C -> .plabel= b π'
%D ))
%D enddiagram
%D
%D diagram product-explicit
%D 2Dx 100 +45 +45
%D 2D 100 A
%D 2D |
%D 2D v
%D 2D +45 B <-- BxC --> C
%D 2D
%D ren A ==> \{1,2\}
%D ren B BxC C ==> \{3,4\} \csm{(3,5),(3,6),\\(4,5),(4,6)} \{5,6\}
%D
%D (( A B -> .plabel= l \mapsab{13,24}
%D A BxC -> .plabel= m \midmap
%D A C -> .plabel= r \mapsab{15,26}
%D B BxC <- .plabel= b π\mathstrut
%D BxC C -> .plabel= b π'
%D ))
%D enddiagram
%D
$$\pu
\def\midmap{\sm{1↦(3,5)\\2↦(4,6)}}
%
\diag{product-ABC}
\qquad
\diag{product-explicit}
$$
\newpage
% «exponentials» (to ".exponentials")
% (lac162p 3 "exponentials")
{\bf Exponentials}
Bijection: $f↔g$
$(→)$ (``currying''): $g := \cur f := λa:A.λb:B.f(a,b)$
$(←)$ (``uncurrying''): $f := \uncur g := λ(a,b):A×B.((g(a))(b))$
\bsk
%D diagram exponentials-ABC
%D 2Dx 100 +45
%D 2D 100 AxB <--| A
%D 2D | |
%D 2D | <-> |
%D 2D v v
%D 2D +50 C |--> B->C
%D 2D
%D ren AxB A ==> A×B A
%D ren C B->C ==> C B{→}C
%D (( AxB A <-| .plabel= a λA.(A×B)
%D C B->C |-> .plabel= b λC.(B{→}C)
%D AxB C -> .plabel= l f
%D A B->C -> .plabel= r g
%D A C harrownodes nil 20 nil <->
%D ))
%D enddiagram
%D
%D diagram exponentials-explicit
%D 2Dx 100 +60
%D 2D 100 AxB <--| A
%D 2D | |
%D 2D | <-> |
%D 2D v v
%D 2D +50 C |--> B->C
%D 2D
%D ren AxB A ==> \csm{(1,3),(1,4)\\(2,3),(2,4)} \{1,2\}
%D ren C B->C ==> \{5,6\} \csm{\fu55,\fu56,\\\fu65,\fu66}
%D (( AxB A <-|
%D C B->C |->
%D AxB C -> .plabel= l \sm{(1,3)↦5\\(1,4)↦6\\(2,3)↦6\\(2,4)↦5}
%D A B->C -> .plabel= r \sm{1↦\fu56\\2↦\fu65}
%D A C harrownodes nil 20 nil <->
%D ))
%D enddiagram
%D
$$\pu
\def\fu#1#2{\csm{(3,#1),\\(4,#2)}}
\diag{exponentials-ABC}
\diag{exponentials-explicit}
$$
\bsk
\bsk
Properties: $\cur \uncur f = f$, \; $\uncur \cur g = g$
where: $f×f' := \ang{π;f,\,π';f'}$, \; $\uncur g := (g×\id);\ev$
solving type equations:
\bsk
% :*"* *
%:
%:
%: π f π' f' π:A×?→A f:A→B π':?×A'→A' f':A'→B'
%: ----- ------ ------ ------------ ---------------------
%: π;f π';f' π;f:A×?→B π';f':?×A'→B'
%: ---------------- ----------------------------------------
%: \ang{π;f,\,π';f'} \ang{π;f,\,π';f'}:A×A'→B×B'
%: ------------------\ren ----------------------------\ren
%: f×f' f×f':A×A'→B×B'
%:
%: ^fxf'_1 ^fxf'_2
%:
%:
%: g \id g:A→(B{→}C) \id:?→?
%: ------ ----------------------
%: g×\id \ev g×\id:A×?→(B{→}C)×? \ev:(B{→}C)×B→C
%: ----------- -----------------------------------------
%: (g×\id);\ev (g×\id);\ev:A×?→C
%: -----------\ren ------------------
%: \uncur"g \uncur"g:A×?→C
%:
%: ^uncur_g_1 ^uncur_g_2
%:
\pu
$$\ded{fxf'_1} \qquad \ded{fxf'_2}$$
$$\ded{uncur_g_1} \qquad \ded{uncur_g_2}$$
\end{document}
% Local Variables:
% coding: utf-8-unix
% ee-anchor-format: "«%s»"
% End: