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: