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

% «.colors»			(to "colors")
% «.defs»			(to "defs")
% «.title-page»			(to "title-page")
% «.parts»			(to "parts")
% «.eagle-eye-view»		(to "eagle-eye-view")
% «.eagle-eye-view-2»		(to "eagle-eye-view-2")
% «.motivation»			(to "motivation")
% «.motivation-2»		(to "motivation-2")
% «.motivation-3»		(to "motivation-3")
%
% «.part-1»			(to "part-1")
% «.start-with-DM»		(to "start-with-DM")
% «.PURO»			(to "PURO")
% «.DM-PURO»			(to "DM-PURO")
% «.BMOs»			(to "BMOs")
% «.graphical-reprs»		(to "graphical-reprs")
% «.set-comprehensions»		(to "set-comprehensions")
% «.set-comprehensions-2»	(to "set-comprehensions-2")
% «.spoiler»			(to "spoiler")
% «.abuse-of-language»		(to "abuse-of-language")
% «.abuse-of-language-2»	(to "abuse-of-language-2")
% «.lambda-in-DM»		(to "lambda-in-DM")
% «.substitution»		(to "substitution")
% «.substitution-2»		(to "substitution-2")
% «.substitution-and-lambda»	(to "substitution-and-lambda")

% «.part-2»			(to "part-2")
% «.reduction»			(to "reduction")
% «.reductions-2»		(to "reductions-2")
% «.reduction-sequences»	(to "reduction-sequences")
% «.termination-and-confluence»	(to "termination-and-confluence")
% «.untyped-lambdas»		(to "untyped-lambdas")
% «.reducing-funs-lambdas»	(to "reducing-funs-lambdas")
% «.reducing-funs-lambdas-2»	(to "reducing-funs-lambdas-2")
% «.types»			(to "types")
% «.types-2»			(to "types-2")
% «.types-3»			(to "types-3")
% «.types-4»			(to "types-4")
% «.types-5»			(to "types-5")
% «.types-6»			(to "types-6")
% «.types-7»			(to "types-7")
% «.missing-information»	(to "missing-information")
% «.missing-information-2»	(to "missing-information-2")
% «.erasing-and-lambda»		(to "erasing-and-lambda")
% «.erasing-and-lambda-2»	(to "erasing-and-lambda-2")
% «.erasing-and-lambda-3»	(to "erasing-and-lambda-3")
% «.how-discharges-are-marked»	(to "how-discharges-are-marked")
% «.ND»				(to "ND")
% «.ND-2»			(to "ND-2")
% «.ND-3»			(to "ND-3")
% «.PAT»			(to "PAT")
% «.PAT-2»			(to "PAT-2")
% «.PAT-3»			(to "PAT-3")
% «.PAT-4»			(to "PAT-4")
% «.obvious-term»		(to "obvious-term")
% «.CCCs»			(to "CCCs")
% «.CCCs-2»			(to "CCCs-2")
% «.logics»			(to "logics")

% «.part-3»			(to "part-3")
% «.judgments»			(to "judgments")
% «.judgments-2»		(to "judgments-2")
% «.judgments-3»		(to "judgments-3")
% «.simple-typing-csla»		(to "simple-typing-csla")
% «.simple-typing-csla-2»	(to "simple-typing-csla-2")
% «.simple-typing-csla-3»	(to "simple-typing-csla-3")
% «.simple-typing-csla-4»	(to "simple-typing-csla-4")
% «.simple-typing-csla-5»	(to "simple-typing-csla-5")
% «.simple-typing-csla-6»	(to "simple-typing-csla-6")
% «.simple-typing-csla-7»	(to "simple-typing-csla-7")
% «.simple-typing-csla-8»	(to "simple-typing-csla-8")
% «.simple-typing-csla-9»	(to "simple-typing-csla-9")
% «.simple-typing-csla-10»	(to "simple-typing-csla-10")
% «.back-to-types»		(to "back-to-types")
% «.back-to-types-2»		(to "back-to-types-2")

% «.impurities»			(to "impurities")

% «.logic-for-children»		(to "logic-for-children")
% «.logic-for-children-2»	(to "logic-for-children-2")
% «.logic-for-children-tools»	(to "logic-for-children-tools")
% «.logic-for-children-tools-2»	(to "logic-for-children-tools-2")
% «.logic-for-children-tools-3»	(to "logic-for-children-tools-3")
%
% «.spaces-of-functions»	(to "spaces-of-functions")
% «.spaces-of-functions-2»	(to "spaces-of-functions-2")
% «.spaces-of-functions-3»	(to "spaces-of-functions-3")
% «.dependent-products»		(to "dependent-products")
% «.pure-type-systems»		(to "pure-type-systems")
% «.pure-type-systems-2»	(to "pure-type-systems-2")
% «.pts-derivation-1»		(to "pts-derivation-1")
% «.pts-derivation-2»		(to "pts-derivation-2")
% «.two-levels-below-a-sort»	(to "two-levels-below-a-sort")
% «.more-sorts»			(to "more-sorts")
% «.PAT»			(to "PAT")


\documentclass[oneside]{book}
\usepackage[colorlinks,urlcolor=brown]{hyperref} % (find-es "tex" "hyperref")
%\usepackage[latin1]{inputenc}
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{pict2e}
\usepackage[x11names,svgnames]{xcolor} % (find-es "tex" "xcolor")
\usepackage{stmaryrd}              % (find-es "tex" "stmaryrd")
%\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-LATEX "edrx15.sty")
\input edrxaccents.tex            % (find-LATEX "edrxaccents.tex")
\input edrxchars.tex              % (find-LATEX "edrxchars.tex")
\input edrxheadfoot.tex           % (find-LATEX "edrxheadfoot.tex")
\input edrxgac2.tex               % (find-LATEX "edrxgac2.tex")
\input 2017planar-has-defs.tex    % (find-LATEX "2017planar-has-defs.tex")
%
% (find-angg ".emacs.papers" "latexgeom")
% (find-LATEXfile "2016-2-GA-VR.tex" "{geometry}")
% (find-latexgeomtext "total={6.5in,8.75in},")
\usepackage[paperwidth=11.5cm, paperheight=9cm,
            %total={6.5in,4in},
            %textwidth=4in,  paperwidth=4.5in,
            %textheight=5in, paperheight=4.5in,
            %a4paper,
            top=1.5cm, bottom=.5cm, left=1cm, right=1cm, includefoot
           ]{geometry}
%
\begin{document}

\catcode`\^^J=10
\directlua{dofile "dednat6load.lua"}  % (find-LATEX "dednat6load.lua")

\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


% «colors» (to ".colors")
% (find-angg ".emacs.papers" "xcolor")
\long\def\ColorRed   #1{{\color{Red1}#1}}
\long\def\ColorBrown #1{{\color{Brown}#1}}
\long\def\ColorBook  #1{{\color{brown}#1}}
\long\def\ColorViolet#1{{\color{MagentaVioletLight}#1}}
\long\def\ColorViolet#1{{\color{Violet!50!black}#1}}
\long\def\ColorGreen #1{{\color{SpringDarkHard}#1}}
\long\def\ColorGreen #1{{\color{SpringGreenDark}#1}}
\long\def\ColorGreen #1{{\color{SpringGreen4}#1}}
\long\def\ColorGray  #1{{\color{GrayLight}#1}}
\long\def\ColorGray  #1{{\color{black!30!white}#1}}


% «defs» (to ".defs")
\def\V{\mathbf{T}}
\def\F{\mathbf{F}}
\def\smile{\ensuremath{{=})}}
\def\frown{\ensuremath{{=}(}}
\def\smirk{\ensuremath{{=}/}}

\def\und#1#2{\underbrace{#1}_{#2}}
\def\und#1#2{\underbrace{#1}_{\text{#2}}}
\def\ug#1{\und{#1}{gen}}
\def\uf#1{\und{#1}{filt}}
\def\ue#1{\und{#1}{expr}}
\def\uC#1{\und{#1}{context}}
\def\uCH#1{\und{#1}{context / hypotheses}}
\def\uvt#1{\und{#1}{v:T}}
\def\uterm#1{\und{#1}{term}}
\def\utype#1{\und{#1}{type}}
\def\uconc#1{\und{#1}{conclusion}}

\def\Sets{\mathsf{Sets}}
\def\TALA{\mathsf{TA}_λ^→}
\def\app {\mathsf{app}}
\def\pair{\mathsf{pair}}

\def\picturedotsa(#1,#2)(#3,#4)#5{%
  \vcenter{\hbox{%
  \beginpicture(#1,#2)(#3,#4)%
  \pictaxes%
  \pictdots{#5}%
  \end{picture}%
  }}%
}

\def\myvcenter#1{\begin{matrix}#1\end{matrix}}

\def\setofst#1#2{\{\,#1\;|\;#2\,\}}
\def\setofsc#1#2{\{\,#1\;;\;#2\,\}}

\setlength{\parindent}{0em}

\def\O{\mathcal{O}}
\def\T{\mathbf{T}}
\def\F{\mathbf{F}}



%  _____ _ _   _      
% |_   _(_) |_| | ___ 
%   | | | | __| |/ _ \
%   | | | | |_| |  __/
%   |_| |_|\__|_|\___|
%                     
% «title-page» (to ".title-page")
% (ntyp 1 "title-page")
% (nty    "title-page")
% (find-es "tex" "huge")
% (find-LATEX "2019logicday.tex" "title-page")

\begin{center}

\Large 

{\bf

An introduction to Type Theory

and to Pure Type Systems

% to the Calculus of Constructions,

\large

\ssk

\ColorGray{and to the ``Logic for Children'' project}

}

%\bsk
%
\normalsize
%
%(a part of the ``Logic for Children'' project)

\msk

Eduardo Ochs (UFF, Brazil)

\footnotesize

\url{http://angg.twu.net/math-b.html\#intro-tys-lfc}

\end{center}


\newpage

\noedrxfooter

%  ____            _       
% |  _ \ __ _ _ __| |_ ___ 
% | |_) / _` | '__| __/ __|
% |  __/ (_| | |  | |_\__ \
% |_|   \__,_|_|   \__|___/
%                          
% «parts» (to ".parts")
% (ntyp 2 "parts")
% (nty    "parts")

These slides are divided into...

\msk

{\bf Part 1: Discrete Mathematics}

How I teach DM to our first-semester CompSci students.

\msk

{\bf Part 2: Logics, $λ$-Calculus and Translations}

A course that some students attend on the second semester.

It introduces the \ColorRed{simply-typed} $λ$-calculus, Curry-Howard,

\ColorRed{Planar} Heyting Algebras, Intuitionistic \ColorRed{Propositional} Logic,

Cartesian Closed Categories, the adjunction $(×B)⊣(B→)$,

and two functional languages: Lisp and Lua.

\msk

{\bf Part 3: Dependent types and Pure Type Systems}

% Categories for Childen (using diagrams and $λ$-terms)}

\msk



\newpage

%  _____            _                                    _               
% | ____|__ _  __ _| | ___        ___ _   _  ___  __   _(_) _____      __
% |  _| / _` |/ _` | |/ _ \_____ / _ \ | | |/ _ \ \ \ / / |/ _ \ \ /\ / /
% | |__| (_| | (_| | |  __/_____|  __/ |_| |  __/  \ V /| |  __/\ V  V / 
% |_____\__,_|\__, |_|\___|      \___|\__, |\___|   \_/ |_|\___| \_/\_/  
%             |___/                   |___/                              
%
% «eagle-eye-view» (to ".eagle-eye-view")
% (ntyp 3 "eagle-eye-view")
% (nty    "eagle-eye-view")

{\bf Eagle-eye view}

In this set of slides we will learn how to interpret

``\ColorRed{judgments}'' and ``\ColorRed{pre-judgments}'' like these:

% (nty "judgments")

% (fooi "\\Sets" "Θ")

\msk

$\begin{array}{rl}
 1) & a⠆\{1,2\}, b⠆\{2,3\}, a<b ⊢ (10a+b)⠆\N \\
 2) & a⠆\{1,2\}, b⠆\{2,3\} ⊢ a<b   \qquad\text{\ColorRed{$⇐$ a false proposition!}} \\
 3) & A⠆Θ, B⠆Θ ⊢ A⠆Θ \\
 4) & A⠆Θ, B⠆Θ ⊢ A×B⠆Θ \\
 5) & A⠆Θ, B⠆Θ, a⠆A, f⠆A→B ⊢ fa⠆B \\
 6) & A⠆Θ, B⠆Θ, a⠆A, b⠆B ⊢ (a,b)⠆A×B \\
 7) & A⠆Θ, B⠆Θ, a⠆A ⊢ (λb⠆B.(a,b))⠆B→A×B \\
 \end{array}
$

\msk

in several type systems --- some of them concrete but informal,

some formal but very abstract...

A non-standard notion --- ``\ColorRed{informally valid}'' ---

will help us understand which judgments are \ColorRed{derivable}.

\newpage

%  _____            _                              ____  
% | ____|__ _  __ _| | ___        ___ _   _  ___  |___ \ 
% |  _| / _` |/ _` | |/ _ \_____ / _ \ | | |/ _ \   __) |
% | |__| (_| | (_| | |  __/_____|  __/ |_| |  __/  / __/ 
% |_____\__,_|\__, |_|\___|      \___|\__, |\___| |_____|
%             |___/                   |___/              
%
% «eagle-eye-view-2» (to ".eagle-eye-view-2")
% (ntyp 3 "eagle-eye-view-2")
% (nty    "eagle-eye-view-2")

{\bf Eagle-eye view (2)}

We will see:

\msk
\def\myitem{$\;\;•\;\;$}
\def\phitem{\phantom{\myitem}}
\def\mysubitem{$\;\;\;\;\;•\;\;$}

\myitem The simply-typed $λ$-calculus (``$λ1$'') as \ColorRed{a} PTS

\myitem Pure Type Systems in which we can represent:

\mysubitem Functors

\mysubitem Natural transformations

\mysubitem Truth-values, propositions, proofs

\msk

This is a preparation for:

\myitem \ColorRed{Interpreting categorical diagrams precisely}

\myitem Raising the status of CT diagrams from second-

\phitem class to first-class citizens

\myitem Formalizing the ``Logic for Children'' project



\newpage

%  __  __       _   _            _   _             
% |  \/  | ___ | |_(_)_   ____ _| |_(_) ___  _ __  
% | |\/| |/ _ \| __| \ \ / / _` | __| |/ _ \| '_ \ 
% | |  | | (_) | |_| |\ V / (_| | |_| | (_) | | | |
% |_|  |_|\___/ \__|_| \_/ \__,_|\__|_|\___/|_| |_|
%                                                  
% «motivation» (to ".motivation")
% (ntyp 3 "motivation")
% (nty    "motivation")

{\bf Motivation (for types)}

The \ColorRed{usual sales talk} for type systems is:

Type systems are at the base of languages like Coq,

that can be used to formalize a lot of mathematics,

and in some cases they can fill up some details of the proofs

themselves, automatically. \ColorRed{Proof assistants} have lots

of uses in academia and in industry, which means

jobs and grants...

\msk

\ColorRed{But Coq is hard to learn \frown, so:}

\msk

Alternative motivation, for people with little free time:

\ColorRed{Many} programming languages use types and lambdas,

even if in a primitive form; if we use types our objects

become Lego-ish pieces that \ColorRed{only match in a few ways}...


\newpage

%  __  __       _   _            _   _               ____  
% |  \/  | ___ | |_(_)_   ____ _| |_(_) ___  _ __   |___ \ 
% | |\/| |/ _ \| __| \ \ / / _` | __| |/ _ \| '_ \    __) |
% | |  | | (_) | |_| |\ V / (_| | |_| | (_) | | | |  / __/ 
% |_|  |_|\___/ \__|_| \_/ \__,_|\__|_|\___/|_| |_| |_____|
%                                                          
% «motivation-2» (to ".motivation-2")
% (ntyp 4 "motivation-2")
% (nty    "motivation-2")

{\bf Motivation (for types) (2)}

At one point, when I was an undergrad, I took a course on

Advanced Calculus that had a bit of Calculus of Variations...

The characterization of ``curves with minimal energy'' only

made sense to me when I discovered that I could draw it as:

%          5
%    y   j-->L
%    ^ 3 ^   ^
%     \->|4 /-->I
%  s-->\ | /6 7
%   1  2 x
%
% (find-LATEX "desenhos.014" "variac")

%D diagram variational
%D 2Dx     100 +16 +32 +32 +16
%D 2D  100     y   j   L
%D 2D           
%D 2D  +16 s -->           I
%D 2D
%D 2D  +16         x
%D 2D
%D (( s x y midpoint ->
%D    x y midpoint x j midpoint ->
%D    x L midpoint I ->
%D    x y -> x j -> j L -> x L ->
%D
%D ))
%D enddiagram
%D
\msk

\centerline{
\resizebox{!}{30pt}{%
$\pu
  \diag{variational}
$}
}

\msk

I just had to \ColorRed{name} the types --- and once I did that

there was a \ColorRed{single way} to make the objects match and

fit together! The construction became \ColorRed{natural}.

\newpage


%  __  __       _   _            _   _               _____ 
% |  \/  | ___ | |_(_)_   ____ _| |_(_) ___  _ __   |___ / 
% | |\/| |/ _ \| __| \ \ / / _` | __| |/ _ \| '_ \    |_ \ 
% | |  | | (_) | |_| |\ V / (_| | |_| | (_) | | | |  ___) |
% |_|  |_|\___/ \__|_| \_/ \__,_|\__|_|\___/|_| |_| |____/ 
%                                                          
% «motivation-3» (to ".motivation-3")
% (ntyp 7 "motivation-3")
% (nty    "motivation-3")

{\bf Motivation (for types) (3)}

We will use \ColorBook{Hindley/Seldin (2008):}

\ColorBook{``Lambda-Calculus and Combinators, an Introduction''.}

It presents several simple $λ$-calculi and type systems,

but looks too abstract at first... we will see a way to

understand some of its notations.

\msk

This book about Type Theory is \ColorRed{mind-blowing} and lots of

fun: \ColorBook{Kamareddine/Laan/Nederpelt (2004):}

\ColorBook{``A Modern Perspective on Type Theory ---

From its origins until today''}

\msk


We will use a book chapter by \ColorBook{Thorsten Altenkirch}, called

\ColorBook{``Naïve Type Theory''}, to complement the KLN book.

(\url{http://www.cs.nott.ac.uk/~psztxa/publ/fomus19.pdf})

% \msk
% 
% These slides will try to make these texts \ColorRed{more accessible}
% 
% to outsiders, and we will also use type theories to make
% 
% Category Theory \ColorRed{more diagrammatical} by showing a way
% 
% to interpret diagrams precisely (long story!)...

% (find-books "__logic/__logic.el" "altenkirch")
% (find-books "__logic/__logic.el" "typetheory")
% (find-books "__cats/__cats.el" "awodey")
% (find-awodeyctpage (+ 10 119) "6.5 lambda-calculus")


\newpage

%  ____            _     _ 
% |  _ \ __ _ _ __| |_  / |
% | |_) / _` | '__| __| | |
% |  __/ (_| | |  | |_  | |
% |_|   \__,_|_|   \__| |_|
%                          
% «part-1» (to ".part-1")
% (ntyp 8 "part-1")
% (nty    "part-1")
% (find-es "tex" "vskip")

\thispagestyle{empty}

\vspace*{20pt}

\begin{center}

\huge {\bf

\ColorBrown{Part 1}

Discrete Mathematics

\Large (At PURO/UFF)

}

\end{center}










\newpage

%  ____  _             _              _ _   _       ____  __  __ 
% / ___|| |_ __ _ _ __| |_  __      _(_) |_| |__   |  _ \|  \/  |
% \___ \| __/ _` | '__| __| \ \ /\ / / | __| '_ \  | | | | |\/| |
%  ___) | || (_| | |  | |_   \ V  V /| | |_| | | | | |_| | |  | |
% |____/ \__\__,_|_|   \__|   \_/\_/ |_|\__|_| |_| |____/|_|  |_|
%                                                                
% «start-with-DM» (to ".start-with-DM")
% (ntyp 9 "start-with-DM")
% (nty    "start-with-DM")

{\bf (Let's start with) Discrete Mathematics}

I teach in a city called Rio das Ostras, in the countryside of

the state of Rio de Janeiro, in a big federal university (``UFF''),

but in one of its smallest campi, away from the capital.

I sometimes teach Discrete Mathematics to Computer Science

students there.

\msk

Many of the students there --- even in CompSci --- enter the

university with very little knowledge of:

1) how to deal with variables,

2) how to write their calculations,

3) how to test their ideas.

\msk

Discrete Mathematics is a first-semester course there.

Let me explain my approach to fix (1), (2), and (3).


\newpage

%  ____  _   _ ____   ___  
% |  _ \| | | |  _ \ / _ \ 
% | |_) | | | | |_) | | | |
% |  __/| |_| |  _ <| |_| |
% |_|    \___/|_| \_\\___/ 
%                          
% «PURO» (to ".PURO")
% (ntyp 10 "PURO")
% (nty     "PURO")

{\bf Pólo Universitário de Rio das Ostras (PURO)}

\begin{tabular}[c]{c}
  % (xz                 "~/LATEX/2019logicday-PURO.jpg")
  \includegraphics[height=160pt]{2019logicday-PURO.jpg} \\
\end{tabular}
%
$⇐$
%
\begin{tabular}[c]{l}
The entrance of the \\
campus looks like this. \\
It feels like a nowhere. \\
I need to interact more \\
via the internets!!! \\
\end{tabular}


\newpage

%  ____  __  __     ____    ____  _   _ ____   ___  
% |  _ \|  \/  |   / __ \  |  _ \| | | |  _ \ / _ \ 
% | | | | |\/| |  / / _` | | |_) | | | | |_) | | | |
% | |_| | |  | | | | (_| | |  __/| |_| |  _ <| |_| |
% |____/|_|  |_|  \ \__,_| |_|    \___/|_| \_\\___/ 
%                  \____/                           
%
% «DM-PURO» (to ".DM-PURO")
% (ntyp 11 "DM-PURO")
% (nty     "DM-PURO")

{\bf Discrete Mathematics at PURO/UFF}

% ``PURO'' = Pólo Universitário de Rio das Ostras.

I structured the Discrete Mathematics (``DM'') course

in three layers.

\msk

{\bf Layer 1} consists of \ColorRed{calculating things} and learning

how to use \ColorRed{mathematical notation} and \ColorRed{definitions}.

Layer 2 introduces some infinite objects, like $\N$ and $\Z$.

Layer 3 introduces a \ColorRed{formal} language for doing proofs.

\msk

Everything in Layer 1 can be calculated in a \ColorRed{finite}

number of steps with \ColorRed{very little creativity}.

\msk

One of the basic things that we learn in Layer 1 is

{\bf set comprehensions} --- that {\color{DarkGreen!75!black}(ta-daaa! Magic!!!!!!)}

are the base for \ColorRed{$λ$-calculus} and \ColorRed{Type Theory}.

% (find-sh "dict comprehension")

\newpage

%  ____  __  __  ___      
% | __ )|  \/  |/ _ \ ___ 
% |  _ \| |\/| | | | / __|
% | |_) | |  | | |_| \__ \
% |____/|_|  |_|\___/|___/
%                         
% «BMOs» (to ".BMOs")
% (ntyp 12 "BMOs")
% (nty     "BMOs")

{\bf Basic Mathematical Objects}

Here's a definition (``for adults'') of the

mathematical objects that we deal with

in Level 1. Notation: $\mathcal{O}$ is the set of BMOs.

\msk

a) Numbers belong to $\O$; $\Z⊂\O$.

b) The truth-values belong to $\O$: $\{\T, \F\}⊂\O$.

c) $\O$ is closed by ``finite lists'' and ``finite sets''.

\ColorViolet{d) Finite strings belong to $\O$.}

\msk

\def\str#1{\ensuremath{\text{``{\tt#1}''}}}

Item (d) is only introduced at the end of the course,

when we show that ``valid expressions'' can be defined

formally... \str{1+2*(3+4)} is ``valid'', but \str{)+)} is not.

\msk

\ColorRed{Some graphical representations are allowed.}


\newpage

%   ____                 _     _           _ 
%  / ___|_ __ __ _ _ __ | |__ (_) ___ __ _| |
% | |  _| '__/ _` | '_ \| '_ \| |/ __/ _` | |
% | |_| | | | (_| | |_) | | | | | (_| (_| | |
%  \____|_|  \__,_| .__/|_| |_|_|\___\__,_|_|
%                 |_|                        
%
% «graphical-reprs» (to ".graphical-reprs")
% (ntyp 13 "graphical-reprs")
% (nty     "graphical-reprs")

{\bf Some graphical representations}

We define graphical representations for:

a) (finite) subsets of $\Z^2$,

b) functions whose domains are (a),

c) directed graphs...


% (lodp 8 "positional")
% (lod    "positional")

%D diagram 12345
%D 2Dx     100 +12 +12
%D 2D  100     1 
%D 2D
%D 2D  +12 2       3
%D 2D
%D 2D  +12     4
%D 2D
%D 2D  +15     5
%D 2D
%D (( 1 2 -> 1 3 -> 2 4 -> 3 4 -> 4 5 ->
%D ))
%D enddiagram
%D
\pu

\unitlength=8pt \def\closeddot{\circle*{0.4}}
\def\closeddot{\circle*{0.5}}

\msk

\resizebox{!}{55pt}{%
$\begin{array}{c}
  K =
  \csm{        & (1,3), &        \\
        (0,2), &        & (2,2), \\
               & (1,1), &        \\
               & (1,0)  &        \\
      }
  = \;\picturedotsa(0,0)(2,3){ 1,3 0,2 2,2 1,1 1,0 }\;
  = \;\picturedots (0,0)(2,3){ 1,3 0,2 2,2 1,1 1,0 }\;
  %
  \\[15pt]
  %
  f =
  \csm{            & ((1,3),1), &            \\
        ((0,2),0), &            & ((2,2),2), \\
                   & ((1,1),1), &            \\
                   & ((1,0),1)  &            \\
      }
  = 
  \sm{    & 1 &   \\
        0 &   & 2 \\
          & 1 &   \\
          & 1 &   \\
      }
  %
  \\
  %
  (V,A)
  = \left( \{1,2,3,4,5\}, \csm{(1,2),(1,3),\\(2,4),(3,4),\\(4,5)} \right)
  = \diag{12345}
  \\
  \end{array}
$}


\newpage

%   ____                               _                    _                 
%  / ___|___  _ __ ___  _ __  _ __ ___| |__   ___ _ __  ___(_) ___  _ __  ___ 
% | |   / _ \| '_ ` _ \| '_ \| '__/ _ \ '_ \ / _ \ '_ \/ __| |/ _ \| '_ \/ __|
% | |__| (_) | | | | | | |_) | | |  __/ | | |  __/ | | \__ \ | (_) | | | \__ \
%  \____\___/|_| |_| |_| .__/|_|  \___|_| |_|\___|_| |_|___/_|\___/|_| |_|___/
%                      |_|                                                    
%
% «set-comprehensions» (to ".set-comprehensions")
% (ntyp 14 "set-comprehensions")
% (nty     "set-comprehensions")

{\bf Layer 1: Set Comprehensions}

One of the first things that I present to students is

a syntax for \ColorRed{set comprehensions} using ``generators'',

``filters'' and a ``result expression''...

\unitlength=5pt \def\closeddot{\circle*{0.2}}

\bsk

$\begin{array}{lll}
  \{\uC{\ug{a∈\{1,2\}},
        \ug{b∈\{2,3\}},
        \uf{a<b}
    };
    \;
    \ue{(a,b)}
  \} 
  &=&
  \{(1,2),(1,3),(2,3)\} \\[-10pt]
  &=& \picturedotsa(0,0)(3,4){ 1,2 1,3 2,3 } \\
  \end{array}
$

\bsk


Note the `;' instead of a `$|$'!

These things can be calculated from left to right

using trees in a finite number of steps.

\newpage

%   ____                                 ____  
%  / ___|___  _ __ ___  _ __  _ __ ___  |___ \ 
% | |   / _ \| '_ ` _ \| '_ \| '__/ __|   __) |
% | |__| (_) | | | | | | |_) | |  \__ \  / __/ 
%  \____\___/|_| |_| |_| .__/|_|  |___/ |_____|
%                      |_|                     
%
% «set-comprehensions-2» (to ".set-comprehensions-2")
% (ntyp 15 "set-comprehensions-2")
% (nty     "set-comprehensions-2")

{\bf Layer 1: Set Comprehensions (2)}

I make the students work in groups, and they solve

the $5+19+16+9+16+7$ exercises quickly.

I suggest this table-ish way to draw the trees...

To calculate

$\setofsc {a∈\{1,2\}, b∈\{2,3\}, a<b} {10a+b} = \{12,13,23\}$

we draw:

\def\tbl#1#2{\fbox{$\begin{array}{#1}#2\end{array}$}}
\def\tbl#1#2{\fbox{$\sm{#2}$}}
\def\tbl#1#2{\fbox{$\mat{#2}$}}
\def\tbl#1#2{$\mat{#2}$}
% "Stop":
% (find-es "tex" "vrule")
\def\S{\omit\vrule\phantom{$\scriptstyle($}\hss}   % stop

\msk

\tbl{ccc}{
 a & b & a<b & 10a+b \\\hline
 1 & 2 & \V & 12 \\
 1 & 3 & \V & 13 \\
 2 & 2 & \F & \S \\
 2 & 3 & \V & 23 \\
}

\msk

the vertical bar means ``abort''.

Valid \ColorRed{values for the context}: $(1,2,\V)$, $(1,3,\V)$, $(2,3,\V)$. 

\newpage

%  ____              _ _           
% / ___| _ __   ___ (_) | ___ _ __ 
% \___ \| '_ \ / _ \| | |/ _ \ '__|
%  ___) | |_) | (_) | | |  __/ |   
% |____/| .__/ \___/|_|_|\___|_|   
%       |_|                        
%
% «spoiler» (to ".spoiler")
% (ntyp 16 "spoiler")
% (nty     "spoiler")

{\bf Layer 1: Set Comprehensions --- SPOILER}

Spoiler: the idea of \ColorRed{context} will be reused in many other

contexts later, but with slightly different notations...

Compare:

\msk

$\begin{array}{rl}
 1) & \setofsc {a∈\{1,2\}, b∈\{2,3\}, a<b} {10a+b} = \{12,13,23\} \\
 2) & a⠆\{1,2\}, b⠆\{2,3\}, a<b ⊢ (10a+b)⠆\N \\
 3) & a⠆\{1,2\}, b⠆\{2,3\} ⊢ a<b   \qquad\text{\ColorRed{$⇐$ this is false!}} \\
 4) & A⠆\Sets, B⠆\Sets ⊢ A⠆\Sets \\
 5) & A⠆\Sets, B⠆\Sets ⊢ A×B⠆\Sets \\
 6) & A⠆\Sets, B⠆\Sets, a⠆A, f⠆A→B ⊢ f(a)⠆B \\
 7) & A⠆\Sets, B⠆\Sets, a⠆A, b⠆B ⊢ (a,b)⠆A×B \\
 8) & A⠆\Sets, B⠆\Sets, a⠆A ⊢ (λb⠆B.(a,b))⠆B→A×B \\
 \end{array}
$


\newpage

%     _    _                         __            _      __  
%    / \  | |__  _   _ ___  ___ _   / /   __ _    | |__   \ \ 
%   / _ \ | '_ \| | | / __|/ _ (_) | |   / _` |   | '_ \   | |
%  / ___ \| |_) | |_| \__ \  __/_  | |  | (_| |_  | |_) |  | |
% /_/   \_\_.__/ \__,_|___/\___(_) | |   \__,_( ) |_.__/   | |
%                                   \_\       |/          /_/ 
%
% «abuse-of-language» (to ".abuse-of-language")
% (ntyp 17 "abuse-of-language")
% (nty     "abuse-of-language")

{\bf An abuse of language}

Remember that I make the students

do $5+19+16+9+16+7$ exercises about set comprehensions...

some of the exercises are about cartesian products, and

some introduce new notations, like:

\msk

$\{x∈\{2,3,4\} ,y∈\{2,3,4\}, y=3; (x,y)\}$

$\{\ColorRed{x,y}∈\{2,3,4\}, y=3; (x,y)\}$

$\{\ColorRed{(x,y)}∈\{2,3,4\}^2, y=3; (x,y)\}$

\msk

This abuse of language will be incredibly important later

when we discuss type systems. We will allow things like:

\msk

$A⠆\Sets, B⠆\Sets, \ColorRed{(a,b)}⠆A×B, f⠆A→B ⊢ fa⠆B$ 

\msk

How do we make $(a,b)$ behave as \ColorRed{a} variable?

(In the singular!)

\newpage

%     _    _                       ________  
%    / \  | |__  _   _ ___  ___   / /___ \ \ 
%   / _ \ | '_ \| | | / __|/ _ \ | |  __) | |
%  / ___ \| |_) | |_| \__ \  __/ | | / __/| |
% /_/   \_\_.__/ \__,_|___/\___| | ||_____| |
%                                 \_\    /_/ 
%
% «abuse-of-language-2» (to ".abuse-of-language-2")
% (ntyp 18 "abuse-of-language-2")
% (nty     "abuse-of-language-2")

{\bf An abuse of language (2)}

Short answer:

$\ColorRed{(a,b)}$ becomes a ``long name'' for a variable \ColorRed{$p$},

$\ColorRed{a}$ becomes an abbreviation for $\ColorRed{π(a,b)}$, i.e., $\ColorRed{πp}$,

$\ColorRed{b}$ becomes an abbreviation for $\ColorRed{π'(a,b)}$, i.e., $\ColorRed{π'p}$,

\msk

$A⠆\Sets, B⠆\Sets, \ColorRed{(a,b)}⠆A×B, f⠆A→B ⊢ f(\ColorRed{a})⠆B$

becomes:

$A⠆\Sets, B⠆\Sets, \ColorRed{p}⠆A×B, f⠆A→B ⊢ f(\ColorRed{πp})⠆B$

\msk

(More on ``long names'' later!)




\newpage

%  _                    _         _         _         ____  __  __ 
% | |    __ _ _ __ ___ | |__   __| | __ _  (_)_ __   |  _ \|  \/  |
% | |   / _` | '_ ` _ \| '_ \ / _` |/ _` | | | '_ \  | | | | |\/| |
% | |__| (_| | | | | | | |_) | (_| | (_| | | | | | | | |_| | |  | |
% |_____\__,_|_| |_| |_|_.__/ \__,_|\__,_| |_|_| |_| |____/|_|  |_|
%                                                                  
% «lambda-in-DM» (to ".lambda-in-DM")
% (ntyp 19 "lambda-in-DM")
% (nty     "lambda-in-DM")

{\bf $λ$-notation in Discrete Mathematics}

In DM we see \ColorRed{functions} as \ColorRed{sets of input-output pairs}...

If $\begin{array}[t]{rrcl} f: & \{1,2,3\} &→& \{10,20,30\} \\ & x & \mto & 10x \end{array}$

then $f = \csm{(1,10),\\ (2,20),\\ (3,30)\\ }$.

\msk

The students learn that, e.g.,

\msk

$\csm{(1,10),\\ (2,20),\\ (3,30)}(2) = 20$, and
$\csm{(1,10),\\ (2,20),\\ (3,30)}(4) = \ColorRed{\mathbf{ERROR}}$.

\msk

We see (in passing) that

$(\ColorRed{λ}x∈\{1,2,3\}.10x)
 = \{ x∈\{1,2,3\}; (x,10x) \}
 = \csm{(1,10),\\ (2,20),\\ (3,30)}
$.


\newpage

%  ____        _         _   _ _         _   _             
% / ___| _   _| |__  ___| |_(_) |_ _   _| |_(_) ___  _ __  
% \___ \| | | | '_ \/ __| __| | __| | | | __| |/ _ \| '_ \ 
%  ___) | |_| | |_) \__ \ |_| | |_| |_| | |_| | (_) | | | |
% |____/ \__,_|_.__/|___/\__|_|\__|\__,_|\__|_|\___/|_| |_|
%                                                          
% «substitution» (to ".substitution")
% (ntyp 20 "substitution")
% (nty     "substitution")
% (gam181p 3 "substituicao")
% (gam181    "substituicao")

{\bf (Simultaneous) substitution}

I also teach, right in the beginning of the course,

a \ColorRed{notation} for (simultaneous) substitution...

(Because I can't rely on the students' Portuguese!...)

Examples:

$$\def\newa{\psm{∫⊙\\◻}}
  \begin{array}{l}
  %
  ((x+y)·z) \subst{ 
    x:=a+y \\
    y:=b+z \\
    z:=c+x \\
  } \\
  =\;\;
  ((a+y)+(b+z))·(c+x) \\[20pt]
  %
  (\text{Vanessão 20 reais}) \bmat{\text{a} := \newa} \\
  =\;\;
  (\text{V$\newa$ness$\widetilde{\newa}$o 20 re$\newa$is}) \\[5pt]
  \end{array}
$$


\newpage

%  ____        _         _   _ _         _   _               ____  
% / ___| _   _| |__  ___| |_(_) |_ _   _| |_(_) ___  _ __   |___ \ 
% \___ \| | | | '_ \/ __| __| | __| | | | __| |/ _ \| '_ \    __) |
%  ___) | |_| | |_) \__ \ |_| | |_| |_| | |_| | (_) | | | |  / __/ 
% |____/ \__,_|_.__/|___/\__|_|\__|\__,_|\__|_|\___/|_| |_| |_____|
%                                                                  
% «substitution-2» (to ".substitution-2")
% (ntyp 21 "substitution-2")
% (nty     "substitution-2")
% (gam181p 3 "substituicao")
% (gam181    "substituicao")
% (gam181    "substituicao" "equações")

{\bf (Simultaneous) substitution (2)}

This is useful to test equations,

\msk

$\begin{array}{l}
  (x^2-4=0) \bmat{x:=3} = (9-4=0) = 𝐛F \\[2pt]
  (x^2-4=0) \bmat{x:=2} = (4-4=0) = 𝐛T \\
\end{array}
$

\msk

and to define a way to calculate expressions with quantifiers:

\msk

$\begin{array}{rcl}
  (∀a∈\{2,3,5\}.a^2<10) &=& (a^2<10)[a:=2] \;∧ \\&&
                            (a^2<10)[a:=3] \;∧ \\&&
                            (a^2<10)[a:=5] \\
                        &=& (2^2<10) ∧
                            (3^2<10) ∧
                            (4^2<10) \\
                        &=& (4<10) ∧
                            (9<10) ∧
                            (16<10) \\
                        &=& \V ∧ \V ∧ \F \\
                        &=& \F \\
  \end{array}
$

\newpage

%  ____        _         _     _                    _         _       
% / ___| _   _| |__  ___| |_  | |    __ _ _ __ ___ | |__   __| | __ _ 
% \___ \| | | | '_ \/ __| __| | |   / _` | '_ ` _ \| '_ \ / _` |/ _` |
%  ___) | |_| | |_) \__ \ |_  | |__| (_| | | | | | | |_) | (_| | (_| |
% |____/ \__,_|_.__/|___/\__| |_____\__,_|_| |_| |_|_.__/ \__,_|\__,_|
%                                                                     
% «substitution-and-lambda» (to ".substitution-and-lambda")
% (ntyp 22 "substitution-and-lambda")
% (nty     "substitution-and-lambda")

{\bf Substitution and $λ$-calculus}

...and I mention, \ColorRed{very} briefly, that we can use substitution

to calculate with $λ$-terms:

\msk

$\begin{array}{rcl}
  (λx∈\{1,2,3\}.10x)(2) &=& (10x)[x:=2] \\
  &=& 10·2 \\
  &=& 20 \\
 \end{array}
$

\msk

\ColorRed{Some} students later take an optional seminar course that is

a \ColorRed{very basic} introduction to $λ$-calculus and Category Theory...

In it they learn how to handle \ColorRed{untyped} $λ$-terms...



\newpage

%  ____            _     ____  
% |  _ \ __ _ _ __| |_  |___ \ 
% | |_) / _` | '__| __|   __) |
% |  __/ (_| | |  | |_   / __/ 
% |_|   \__,_|_|   \__| |_____|
%                              
% «part-2» (to ".part-2")
% (ntyp 23 "part-2")
% (nty     "part-2")

\thispagestyle{empty}

% \vspace*{20pt}

\begin{center}

\huge {\bf

\ColorBrown{Part 2}

$λ$-Calculus, Logics, \\

and Translations

\Large (At PURO/UFF)

}

\bsk

\normalsize

An optional, second-semester-ish,

hands-on seminar course...

\ColorBrown{($↑$ based on exercises)}

\ssk

I used it to \ColorRed{test} several ideas of the

``Logic for Children'' project!...


\end{center}


\newpage

%  ____          _            _   _             
% |  _ \ ___  __| |_   _  ___| |_(_) ___  _ __  
% | |_) / _ \/ _` | | | |/ __| __| |/ _ \| '_ \ 
% |  _ <  __/ (_| | |_| | (__| |_| | (_) | | | |
% |_| \_\___|\__,_|\__,_|\___|\__|_|\___/|_| |_|
%                                               
% «reduction» (to ".reduction")
% (ntyp 24 "reduction")
% (nty     "reduction")
% (lodp 16 "evaluating-exprs")
% (lod     "evaluating-exprs")

{\bf Reductions}

What happens if we forget all \ColorRed{algebra} that we know?

Suppose that we forget everything beyond basic arithmetic.

Now we only know how to add and multiply \ColorRed{numbers}.

What are the ways to calculate an expression ---

$2·3+4·5$, say --- step-by-step until we reach a final result?

%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
$$\resizebox{!}{30pt}{$
  \diag{2x4+4x5}
  $}
$$

We get a directed graph!


\newpage

%  ____          _            _   _                   ____  
% |  _ \ ___  __| |_   _  ___| |_(_) ___  _ __  ___  |___ \ 
% | |_) / _ \/ _` | | | |/ __| __| |/ _ \| '_ \/ __|   __) |
% |  _ <  __/ (_| | |_| | (__| |_| | (_) | | | \__ \  / __/ 
% |_| \_\___|\__,_|\__,_|\___|\__|_|\___/|_| |_|___/ |_____|
%                                                           
% «reductions-2» (to ".reductions-2")
% (ntyp 25 "reductions-2")
% (nty     "reductions-2")

{\bf Reductions (2)}
%
$$\resizebox{!}{30pt}{$
  \diag{2x4+4x5}
  $}
$$
%
The students draw graphs like these for \ColorRed{several}

initial expressions... each graph can be drawn in

several equivalent ways, and the students learn

to \ColorRed{debug their graphs} by working together,

comparing their drawings, and trying to find

more elegant shapes...

\newpage

%  ____          _                                 
% |  _ \ ___  __| |_   _  ___   ___  ___  __ _ ___ 
% | |_) / _ \/ _` | | | |/ __| / __|/ _ \/ _` / __|
% |  _ <  __/ (_| | |_| | (__  \__ \  __/ (_| \__ \
% |_| \_\___|\__,_|\__,_|\___| |___/\___|\__, |___/
%                                           |_|    
%
% «reduction-sequences» (to ".reduction-sequences")
% (ntyp 26 "reduction-sequences")
% (nty     "reduction-sequences")

{\bf Reduction sequences}

The arrows here show the \ColorRed{one-step reductions}

starting from $2·3+4·5$.

$$\resizebox{!}{30pt}{$
  \diag{2x4+4x5}
  $}
$$

After a bunch of similar exercices the students

get the feeling that all \ColorRed{reduction sequences} terminate,

and that we have ``confluence''.

These properties --- ``termination'' and ``confluence'' ---

are very important, and we want to keep them

as we \ColorRed{add} more ways to calculate things...


\newpage

%  _____                                     _                    __ _ 
% |_   _|__ _ __ _ __ ___     __ _ _ __   __| |   ___ ___  _ __  / _| |
%   | |/ _ \ '__| '_ ` _ \   / _` | '_ \ / _` |  / __/ _ \| '_ \| |_| |
%   | |  __/ |  | | | | | | | (_| | | | | (_| | | (_| (_) | | | |  _| |
%   |_|\___|_|  |_| |_| |_|  \__,_|_| |_|\__,_|  \___\___/|_| |_|_| |_|
%                                                                      
% «termination-and-confluence» (to ".termination-and-confluence")
% (ntyp 27 "termination-and-confluence")
% (nty     "termination-and-confluence")

{\bf Termination and confluence}

From \ColorBook{Hindley/Seldin (2008)}...

% (find-books "__logic/__logic.el" "hindley-seldin2")
% (find-hindleyseldin2page (+ 14 14) "confluence")
% (find-hindleyseldin2text (+ 14 14) "confluence")
% (find-hindleyseldin2page (+ 14 114) "completely safe")
% (find-hindleyseldin2text (+ 14 114) "completely safe")

\ssk

P.14:

{\bf Note} The property described in the Church-Rosser theorem, that
if a term can be \ColorRed{reduced to two different terms} then these
two terms can be \ColorRed{further reduced to one term}, is called
{\sl confluence}. The theorem states that {\sl $β$-reduction is
  confluent}.

\msk

P.114:

The above theorem and its corollaries contrast strongly with untyped
$λ$, in which reductions may be infinitely long and there is no
decision-procedure for the relation $=_β$ (Corollary 5.6.3). They say
that the world of typed terms is \ColorRed{completely safe}, in the
sense that \ColorRed{all computations terminate and their results are
  unique}.



\newpage

%  _   _       _                        _ 
% | | | |_ __ | |_ _   _ _ __   ___  __| |
% | | | | '_ \| __| | | | '_ \ / _ \/ _` |
% | |_| | | | | |_| |_| | |_) |  __/ (_| |
%  \___/|_| |_|\__|\__, | .__/ \___|\__,_|
%                  |___/|_|               
%
% «untyped-lambdas» (to ".untyped-lambdas")
% (ntyp 28 "untyped-lambdas")
% (nty     "untyped-lambdas")

{\bf Untyped `$λ$'s}

Typed `$λ$'s \ColorRed{can} be calculated using sets.

Untyped `$λ$'s \ColorRed{have to} be calculated using substituition.

\bsk

$\qquad
 \begin{array}{rcl}
  (λx∈\{1,2,3\}.10x)(2) &=& \csm{(1,10),\\ (2,20),\\ (3,30)}(2) \\
                        &=& 20 \\
  \\
            (λx.10x)(2) &=& (10x)[x:=2] \\
                        &=& 10·2 \\
                        &=& 20 \\
  \end{array}
$

\newpage


%  ____          _            _                __                 
% |  _ \ ___  __| |_   _  ___(_)_ __   __ _   / _|_   _ _ __  ___ 
% | |_) / _ \/ _` | | | |/ __| | '_ \ / _` | | |_| | | | '_ \/ __|
% |  _ <  __/ (_| | |_| | (__| | | | | (_| | |  _| |_| | | | \__ \
% |_| \_\___|\__,_|\__,_|\___|_|_| |_|\__, | |_|  \__,_|_| |_|___/
%                                     |___/                       
%                                                                             
% «reducing-funs-lambdas» (to ".reducing-funs-lambdas")
% (ntyp 29 "reducing-funs-lambdas")
% (nty     "reducing-funs-lambdas")
% (lodp 17 "evaluating-exprs-2")
% (lod     "evaluating-exprs-2")

{\bf Reducing functions and `$λ$'s}

We add \ColorRed{named functions} and \ColorRed{(untyped) `$λ$'s}...

If $g(a) = a·a+4$ and $h = λa.\,a·a+4$, then:

\msk

%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
$\resizebox{0.6\width}{!}{$
 \diag{reduce-g}
 \qquad
 \diag{reduce-h}
 $}
$

\newpage

%  ____          _            _                __                   ____  
% |  _ \ ___  __| |_   _  ___(_)_ __   __ _   / _|_   _ _ __  ___  |___ \ 
% | |_) / _ \/ _` | | | |/ __| | '_ \ / _` | | |_| | | | '_ \/ __|   __) |
% |  _ <  __/ (_| | |_| | (__| | | | | (_| | |  _| |_| | | | \__ \  / __/ 
% |_| \_\___|\__,_|\__,_|\___|_|_| |_|\__, | |_|  \__,_|_| |_|___/ |_____|
%                                     |___/                               
%
% «reducing-funs-lambdas-2» (to ".reducing-funs-lambdas-2")
% (ntyp 30 "reducing-funs-lambdas-2")
% (nty     "reducing-funs-lambdas-2")

% Zoom:

$\resizebox{0.76\width}{!}{$
 \diag{reduce-g}
 \quad
 \diag{reduce-h}
 $}
$

\newpage

%  _____                      
% |_   _|   _ _ __   ___  ___ 
%   | || | | | '_ \ / _ \/ __|
%   | || |_| | |_) |  __/\__ \
%   |_| \__, | .__/ \___||___/
%       |___/|_|              
%
% «types» (to ".types")
% (ntyp 31 "types")
% (nty     "types")
% (lam181p 8 "types")
% (lam181    "types")

{\bf Types}

Let's (re)introduce types, but with another notation (`:').

Let:

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

\ssk

If $f:A→B$, then $f$ is one of four functions...

$$\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 \ColorRed{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$

\ColorRed{means} $f∈(A→B)$.

\newpage

%  _____                        ____  
% |_   _|   _ _ __   ___  ___  |___ \ 
%   | || | | | '_ \ / _ \/ __|   __) |
%   | || |_| | |_) |  __/\__ \  / __/ 
%   |_| \__, | .__/ \___||___/ |_____|
%       |___/|_|                      
%
% «types-2» (to ".types-2")
% (ntyp 32 "types-2")
% (nty     "types-2")

{\bf Types (2)}

In Type Theory and $λ$-calculus ``$\ColorRed{a:A}$''

is pronounced ``\ColorRed{$a$ is of type $A$}'', and the meaning

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

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

\msk

Note that:

1) if $\ColorRed{f:A→B}$ and $\ColorRed{a:A}$ then $\ColorRed{f(a):B}$

2) if $\ColorRed{a:A}$ and $\ColorRed{b:B}$ then $\ColorRed{(a,b):A×B}$

3) if $\ColorRed{p:A×B}$ then $\ColorRed{πp:A}$ and $\ColorRed{π'p:B}$, where

4) `$\ColorRed{π}$' means `first projection' and

5) `$\ColorRed{π'}$' means `second projection'...

\msk

Example:

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

\newpage

%  _____                        _____ 
% |_   _|   _ _ __   ___  ___  |___ / 
%   | || | | | '_ \ / _ \/ __|   |_ \ 
%   | || |_| | |_) |  __/\__ \  ___) |
%   |_| \__, | .__/ \___||___/ |____/ 
%       |___/|_|                      
%
% «types-3» (to ".types-3")
% (ntyp 33 "types-3")
% (nty     "types-3")

{\bf Types (3)}

Let:

$\begin{array}{l}
 A = \{1,2\}, \\
 B = \{3,4\}, \\
 C = \{5,6\}. \\
 \end{array}
$

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})
$$

...because $A$, $B$, and $C$ are known sets!

\newpage

%  _____                        _  _   
% |_   _|   _ _ __   ___  ___  | || |  
%   | || | | | '_ \ / _ \/ __| | || |_ 
%   | || |_| | |_) |  __/\__ \ |__   _|
%   |_| \__, | .__/ \___||___/    |_|  
%       |___/|_|                       
%
% «types-4» (to ".types-4")
% (ntyp 34 "types-4")
% (nty     "types-4")

{\bf Types (4)}

More abstractly now, if $A$, $B$, $C$ are \ColorRed{known} sets, 

and $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})
$$

i.e., $(πp,g(π'p)):A×C$.



\newpage


%  _____                        ____  
% |_   _|   _ _ __   ___  ___  | ___| 
%   | || | | | '_ \ / _ \/ __| |___ \ 
%   | || |_| | |_) |  __/\__ \  ___) |
%   |_| \__, | .__/ \___||___/ |____/ 
%       |___/|_|                      
%
% «types-5» (to ".types-5")
% (ntyp 35 "types-5")
% (nty     "types-5")

{\bf Types (5)}

At the right we see \ColorRed{one of} the standard notations

for \ColorRed{type inference}:

\msk

%:
%:                      p⠆A{×}B
%:                      -------π'
%:   p⠆A{×}B   g⠆B{→}C  π'p⠆B
%:   -------π  --------------\app
%:    πp⠆A      g(π'p)⠆C
%:    -------------------\pair
%:     (πp,g(π'p))⠆A{×}C
%:
%:        ^types-5
%:
\pu
$ %\def\myvcenter#1{\begin{array}[t]{c}#1\end{array}}
  \myvcenter{
  \und{(\und{π\und{p}{:A×B}}{:A},\;\;
        \und{\und{g}{:B→C}(\und{π'\und{p}{:A×B}}{:B})}{:C})}{:A×C})
  }
  \quad
  \myvcenter{\cded{types-5}}
$

\msk

The tree at the right is a \ColorRed{derivation} of $(πp,g(π'p))⠆A{×}C$

from \ColorRed{hypotheses} $p⠆A{×}B$ and $g⠆B{→}C$

(in a type system that is still unnamed)

\newpage


%  _____                         __   
% |_   _|   _ _ __   ___  ___   / /_  
%   | || | | | '_ \ / _ \/ __| | '_ \ 
%   | || |_| | |_) |  __/\__ \ | (_) |
%   |_| \__, | .__/ \___||___/  \___/ 
%       |___/|_|                      
%
% «types-6» (to ".types-6")
% (ntyp 36 "types-6")
% (nty     "types-6")

{\bf Types (6)}

We had these rules in the slide ``Types (2)''...

\msk

\def\ru#1{\ColorGreen{$(#1)$}}
\def\ru#1{}
\begin{tabular}{ll}
1) if $\ColorRed{f:A→B}$ and $\ColorRed{a:A}$ then $\ColorRed{f(a):B}$  & \ru{\app} \\
2) if $\ColorRed{a:A}$ and $\ColorRed{b:B}$ then $\ColorRed{(a,b):A×B}$ & \ru{\pair} \\
3) if $\ColorRed{p:A×B}$ then $\ColorRed{πp:A}$ and $\ColorRed{π'p:B}$  & \ru{π, π'} \\
\end{tabular}

\msk

They become tree rules, written with bars:

%:
%:  f⠆A{→}B  a⠆A
%:  ------------\app
%:     f(a)
%:
%:     ^app
%:
%:  p⠆A{×}B    p⠆A{×}B      a⠆A  b⠆B  
%:  -------π   -------π'   ---------\pair
%:   πp⠆A       πp'⠆B      (a,b)⠆A{×}B
%:                        
%:    ^pi        ^pi        ^pair
%:
\pu
$$\ded{app}$$
$$\ded{pair} \qquad \ded{pi} \qquad \ded{pi}$$



\newpage


%  _____                        _____ 
% |_   _|   _ _ __   ___  ___  |___  |
%   | || | | | '_ \ / _ \/ __|    / / 
%   | || |_| | |_) |  __/\__ \   / /  
%   |_| \__, | .__/ \___||___/  /_/   
%       |___/|_|                      
%
% «types-7» (to ".types-7")
% (ntyp 37 "types-7")
% (nty     "types-7")

{\bf Types (7)}

Each bar in a valid derivation is a

substituition instance of one of the rules...

%:    πp⠆A      g(π'p)⠆C
%:    -------------------\pair
%:     (πp,g(π'p))⠆A{×}C
%:
%:        ^types-5-last-line
%:
\pu

\msk

$$\ded{types-5}$$

$$\left( \cded{pair} \right)
  \subst{
    a := πp \\
    b := g(π'p) \\
    B := C \\
  }
  =
  \left( \cded{types-5-last-line} \right)
$$




\newpage


%  __  __ _         _               _        __ 
% |  \/  (_)___ ___(_)_ __   __ _  (_)_ __  / _|
% | |\/| | / __/ __| | '_ \ / _` | | | '_ \| |_ 
% | |  | | \__ \__ \ | | | | (_| | | | | | |  _|
% |_|  |_|_|___/___/_|_| |_|\__, | |_|_| |_|_|  
%                           |___/               
%
% «missing-information» (to ".missing-information")
% (ntyp 38 "missing-information")
% (nty     "missing-information")

{\bf (Re)constructing missing information}

Students are very good to learn \ColorRed{syntax} from \ColorRed{examples}.

Exercise: I ask the students to reconstruct the

missing information in trees that have just a few

term names, types, and rule names...

%:
%:                      p⠆A{×}B
%:                      -------π'
%:   p⠆A{×}B   g⠆B{→}C  π'p⠆B
%:   -------π  --------------\app
%:    πp⠆A      g(π'p)⠆C
%:    -------------------\pair
%:     (πp,g(π'p))⠆A{×}C
%:
%:        ^types-5
%:
%:                          p⠆A{×}B
%:                          -------\r{π'}
%:   p⠆A{×}B       g⠆B{→}C  \n{π'p}{B}
%:   -------\r{π}  ----------------\r{\app}
%:   \n{πp}{A}        \n{g(π'p)}{C}
%:   ----------------------\r{\pair}
%:    \n{(πp,g(π'p))}{A{×}C}
%:
%:        ^types-5-marked
%:
\def\black     #1{#1}
\def\gray      #1{\ColorGray{#1}}
\def\gray      #1{\ColorGray{?}}
\def\nodetype#1#2{\ColorGray{#1⠆}#2}
\def\nodetype#1#2{\ColorGray{?⠆}#2}
\def\nodeterm#1#2{#1\ColorGray{⠆#2}}
\def\nodeterm#1#2{#1\ColorGray{⠆?}}
\def\nodenone#1#2{\ColorGray    {?}}
\def\nodeall #1#2{#1⠆#2}
\def\treetypes{
  \def\r{\gray}
  \def\n{\nodetype}
  \cded{types-5-marked}
}
\def\treeterms{
  \def\r{\gray}
  \def\n{\nodeterm}
  \cded{types-5-marked}
}
\def\treerules{
  \def\r{\black}
  \def\n{\nodenone}
  \cded{types-5-marked}
}
\def\treeorig{
  \def\r{\black}
  \def\n{\nodeall}
  \cded{types-5-marked}
}
%D diagram reconstruct
%D 2Dx     100 +120
%D 2D  100 A
%D 2D
%D 2D  +45 B   D
%D 2D
%D 2D  +45 C
%D 2D
%D (( A .tex= \treeterms
%D    B .tex= \treetypes
%D    C .tex= \treerules
%D    D .tex= \cded{types-5}
%D    A D -> B D -> C D ->
%D
%D ))
%D enddiagram
%D
\pu
$$\resizebox{0.65\textwidth}{!}{%
$\diag{reconstruct}
$}
$$

\newpage


%  __  __ _         _               _        __   ____  
% |  \/  (_)___ ___(_)_ __   __ _  (_)_ __  / _| |___ \ 
% | |\/| | / __/ __| | '_ \ / _` | | | '_ \| |_    __) |
% | |  | | \__ \__ \ | | | | (_| | | | | | |  _|  / __/ 
% |_|  |_|_|___/___/_|_| |_|\__, | |_|_| |_|_|   |_____|
%                           |___/                       
%
% «missing-information-2» (to ".missing-information-2")
% (ntyp 39 "missing-information-2")
% (nty     "missing-information-2")

% {\bf missing-information-2}

\resizebox{1.0\textwidth}{!}{%
$\diag{reconstruct}
$}


\newpage

%  _____               _                               _   _     
% | ____|_ __ __ _ ___(_)_ __   __ _    __ _ _ __   __| | | |    
% |  _| | '__/ _` / __| | '_ \ / _` |  / _` | '_ \ / _` | | |    
% | |___| | | (_| \__ \ | | | | (_| | | (_| | | | | (_| | | |___ 
% |_____|_|  \__,_|___/_|_| |_|\__, |  \__,_|_| |_|\__,_| |_____|
%                              |___/                             
%
% «erasing-and-lambda» (to ".erasing-and-lambda")
% (ntyp 40 "erasing-and-lambda")
% (nty     "erasing-and-lambda")

{\bf Erasing and reconstructing (and `$λ$'s)}

\ColorRed{Erasing} information is easy.

\ColorRed{Reconstructing} information is harder

(and may not be always possible)...

What if the tree below is the result of taking

something bigger, and erasing information from it?

$$\cded{types-5}$$

\msk

This is the key idea for 

understanding `$λ$'s and discharges!!!

\newpage


%  _____               _                               _   _       ____  
% | ____|_ __ __ _ ___(_)_ __   __ _    __ _ _ __   __| | | |     |___ \ 
% |  _| | '__/ _` / __| | '_ \ / _` |  / _` | '_ \ / _` | | |       __) |
% | |___| | | (_| \__ \ | | | | (_| | | (_| | | | | (_| | | |___   / __/ 
% |_____|_|  \__,_|___/_|_| |_|\__, |  \__,_|_| |_|\__,_| |_____| |_____|
%                              |___/                                     
%
% «erasing-and-lambda-2» (to ".erasing-and-lambda-2")
% (ntyp ?? "erasing-and-lambda-2")
% (nty     "erasing-and-lambda-2")

{\bf Erasing and reconstructing (and `$λ$'s) (2)}

What happens if we add to the left of each term,

or to the left of each ``term : type'',

a \ColorRed{list of free variables}, written as ``\ColorRed{free variables $⊢$}''?

% a \ColorRed{context} ``\ColorRed{free variables $⊢$}''?

\msk

%:
%:                 p
%:                ---\r{π'}
%:     p       g  π'p
%:    --\r{π}  ------\r{\app}
%:    πp       g(π'p)
%:    ---------------\r{\pair}
%:     (πp,g(π'p))
%:
%:     ^types-5-skel
%:
%:
%:                    p⊢p
%:                   -----\r{π'}
%:    p⊢p       g⊢g  p⊢π'p
%:    --\r{π}   ----------\r{\app}
%:    p⊢πp      g,p⊢g(π'p)
%:    -------------------\r{\pair}
%:     g,p⊢(πp,g(π'p))
%:
%:     ^types-5-skel-with-free-vars
%:
\pu
$\def\r#1{#1}
  \def\r#1{}
  \begin{array}{l}
  \cded{types-5-skel}
  \quad
  \two/<-`-->/<400>^{\text{erase}}_{\text{reconstruct}}
  \quad
  \cded{types-5}
  \\ \\
  \cded{types-5-skel-with-free-vars}
  \quad
  \two/<-`-->/<400>^{\text{erase}}_{\text{reconstruct}}
  \qquad
  ?
  \end{array}
$


\newpage


%  _____               _                               _   _       _____ 
% | ____|_ __ __ _ ___(_)_ __   __ _    __ _ _ __   __| | | |     |___ / 
% |  _| | '__/ _` / __| | '_ \ / _` |  / _` | '_ \ / _` | | |       |_ \ 
% | |___| | | (_| \__ \ | | | | (_| | | (_| | | | | (_| | | |___   ___) |
% |_____|_|  \__,_|___/_|_| |_|\__, |  \__,_|_| |_|\__,_| |_____| |____/ 
%                              |___/                                     
%
% «erasing-and-lambda-3» (to ".erasing-and-lambda-3")
% (ntyp ?? "erasing-and-lambda-3")
% (nty     "erasing-and-lambda-3")

{\bf Erasing and reconstructing (and `$λ$'s) (3)}

In all the ``\ColorRed{standard}'' rules the context of the conclusion

will be the \ColorRed{union} of the contexts of the hypotheses.

The new rule `$λ$' is not standard.

It ``\ColorRed{discharges}'' a variable from the list of free variables,

and \ColorRed{transfers it to the right} of the `$⊢$', into the `$λ$.

\bsk

%:
%:
%:  f⠆A{→}B  a⠆A       g⠆A{→}C  a⠆A   
%:  ------------\app   ------------\app
%:      fa⠆B               ga⠆C
%:      -----------------------\pair
%:            (fa,ga)⠆B{×}C
%:          ------------------------λ
%:          (λa⠆A.(fa,ga))⠆A{→}(B{×}C)
%:
%:          ^discharge-1
%:
%:   f⊢f  a⊢a   g⊢g  a⊢a   
%:   --------   --------
%:   f,a⊢fa     g,a⊢ga
%:   -----------------
%:    f,g,a⊢(fa,ga)
%:    ----------------λ
%:    f,g⊢λ\ColorRed{a}.(fa,ga)
%:
%:     ^discharge-2
%:
\pu
\resizebox{1.0\textwidth}{!}{%
$\ded{discharge-2}
  \quad
  \ded{discharge-1}
$}

\newpage


%  ____  _          _                                 __  __ 
% |  _ \(_)___  ___| |__   __ _ _ __ __ _  ___  ___  |  \/  |
% | | | | / __|/ __| '_ \ / _` | '__/ _` |/ _ \/ __| | |\/| |
% | |_| | \__ \ (__| | | | (_| | | | (_| |  __/\__ \ | |  | |
% |____/|_|___/\___|_| |_|\__,_|_|  \__, |\___||___/ |_|  |_|
%                                   |___/                    
%
% «how-discharges-are-marked» (to ".how-discharges-are-marked")
% (ntyp 43 "how-discharges-are-marked")
% (nty     "how-discharges-are-marked")

{\bf How discharges are marked}

Convention: the context is the list of undischarged hypotheses;

a bar marked as ``$λ;1$'' discharges the hypotheses marked ``$[·]^1$''.

%:   f⊢f  a⊢a   g⊢g  a⊢a   
%:   --------   --------
%:   f,a⊢fa     g,a⊢ga
%:   -----------------
%:    f,g,a⊢(fa,ga)
%:    ----------------λ
%:    f,g⊢λa.(fa,ga)
%:
%:     ^discharge-c
%:
%:   f  [a]^1   g  [a]^1   
%:   --------   --------
%:      fa        ga
%:      ------------
%:        (fa,ga)
%:       ----------λ;1
%:       λa.(fa,ga)
%:
%:       ^discharge-nonc
%:
\pu
$$\ded{discharge-nonc}
  \qquad
  \ded{discharge-c}
$$

\newpage

%  _   _ ____  
% | \ | |  _ \ 
% |  \| | | | |
% | |\  | |_| |
% |_| \_|____/ 
%              
% «ND» (to ".ND")
% (ntyp 44 "ND")
% (nty     "ND")

{\bf The connection with Natural Deduction}

Look at the tree below.

Each node of it is of the form ``term : type'',

The contexts {\sl (listing free variables)} are not shown,

the names of the rules are not shown {(\sl except for `$λ$')},

but the discharges are marked...


%:   f⠆A{→}B  [a⠆A]^1   g⠆A{→}C  [a⠆A]^1   
%:   ----------------   ----------------
%:          fa⠆B              ga⠆C
%:          ----------------------
%:               (fa,ga)⠆B{×}C
%:          -------------------------λ;1
%:          (λa⠆A.(fa,ga))⠆A{→}(B{×}C)
%:
%:           ^discharge-nonct
%:
%:   A{→}B  [A]^1   A{→}C  [A]^1   
%:   ------------   ------------
%:         B            C
%:         --------------
%:             B{×}C
%:          -----------1
%:          A{→}(B{×}C)
%:
%:          ^discharge-nonct-types
%:
%:   A{→}B⊢A{→}B  [A⊢A]^1   A{→}C⊢A{→}C  [A⊢A]^1   
%:   --------------------   --------------------
%:         A{→}B,A⊢B               A{→}C,A⊢C
%:         ---------------------------------
%:             A{→}B,A{→}C,A⊢B{×}C
%:          -------------------------1
%:          A{→}B,A{→}C⊢A{→}(B{×}C)
%:
%:          ^discharge-nonct-types-cont
%:
\pu
$$\ded{discharge-nonct}
$$

What happens if we erase the \ColorRed{terms} and leave only the types?

And if \ColorRed{after that} we display the contexts?

\newpage


%  _   _ ____    ____  
% | \ | |  _ \  |___ \ 
% |  \| | | | |   __) |
% | |\  | |_| |  / __/ 
% |_| \_|____/  |_____|
%                      
% «ND-2» (to ".ND-2")
% (ntyp 45 "ND-2")
% (nty     "ND-2")

{\bf The connection with Natural Deduction (2)}

After erasing the \ColorRed{terms} we get this,
%
$$\ded{discharge-nonct-types}
$$
%
After adding the contexts we get this:
%
$$\ded{discharge-nonct-types-cont}
$$


\newpage


%  _   _ ____    _____ 
% | \ | |  _ \  |___ / 
% |  \| | | | |   |_ \ 
% | |\  | |_| |  ___) |
% |_| \_|____/  |____/ 
%                      
% «ND-3» (to ".ND-3")
% (ntyp 46 "ND-3")
% (nty     "ND-3")

{\bf The connection with Natural Deduction (2)}

If we change the notation a bit we get trees that talk

about \ColorRed{propositions} and \ColorRed{logic}:

%:   P{→}Q  [P]^1   P{→}R  [P]^1   
%:   ------------   ------------
%:         Q            R
%:         --------------
%:             Q{∧}R
%:          -----------1
%:          P{→}(Q{∧}R)
%:
%:          ^ND-1
%:
%:   P{→}Q⊢P{→}Q  [P⊢P]^1   P{→}R⊢P{→}R  [P⊢P]^1   
%:   --------------------   --------------------
%:         P{→}Q,P⊢Q               P{→}R,P⊢R
%:         ---------------------------------
%:             P{→}Q,P{→}R,P⊢Q{∧}R
%:          -------------------------1
%:          P{→}Q,P{→}R⊢P{→}(Q{∧}R)
%:
%:          ^ND-SC-1
%:
\pu
$$\ded{ND-1}$$
$$\ded{ND-SC-1}$$

``If $P{→}Q$ and $P{→}R$ are \ColorRed{true} then $P{→}(Q{∧}R)$ is true''.


\newpage

{\bf Mixed judgments}

In the beginning (on Discrete Maths) we saw contexts

that mixed type declarations (working as \ColorRed{generators})

and propositions (working as \ColorRed{filters})...


\msk

We looked at \ColorRed{set comprehensions} in detail:

$\setofsc {a∈\{1,2\}, b∈\{2,3\}, a<b} {10a+b} = \{12,13,23\}$

\ssk

and I mentioned briefly ``mixed'' judgments like this one:

$a⠆\{1,2\}, b⠆\{2,3\}, a<b ⊢ (10a+b)⠆\N$


\msk

We can interpret these mixed judgments in $λ$-calculus

if we use a trick called ``propositions-as-types''.

\newpage


%  ____   _  _____ 
% |  _ \ / \|_   _|
% | |_) / _ \ | |  
% |  __/ ___ \| |  
% |_| /_/   \_\_|  
%                  
% «PAT» (to ".PAT")
% (ntyp 48 "PAT")
% (nty     "PAT")

{\bf Propositions-as-types}

We saw this tree (``in logic'') as having only \ColorRed{types}:

%:   P{→}Q  [P]^1   P{→}R  [P]^1   
%:   ------------   ------------
%:         Q            R
%:         --------------
%:             Q{∧}R
%:          -----------1
%:          P{→}(Q{∧}R)
%:
%:          ^ND-PAT-1
%:
$$\pu\ded{ND-PAT-1}$$

if we add ``terms'' to it we get:

%:   f⠆P{→}Q  [p⠆P]^1   g⠆P{→}R  [p⠆P]^1   
%:   ----------------   ----------------
%:         fp⠆Q                gp⠆R
%:         ------------------------
%:             (fp,gp)⠆Q{×}R
%:             -------------1
%:          (λp⠆P.(fp,gp))⠆P{→}(Q{×}R)
%:
%:          ^ND-PAT-2
%:
$$\pu\ded{ND-PAT-2}$$



%  ____   _  _____   ____  
% |  _ \ / \|_   _| |___ \ 
% | |_) / _ \ | |     __) |
% |  __/ ___ \| |    / __/ 
% |_| /_/   \_\_|   |_____|
%                          
% «PAT-2» (to ".PAT-2")
% (ntyp 49 "PAT-2")
% (nty     "PAT-2")

{\bf Propositions-as-types (2)}

We can unify the notations by doing this:
%
%:   f⠆⟦P{→}Q⟧  [p⠆⟦P⟧]^1   g⠆⟦P{→}R⟧  [p⠆⟦P⟧]^1   
%:   ----------------   ----------------
%:         fp⠆⟦Q⟧                gp⠆⟦R⟧
%:         ------------------------
%:             (fp,gp)⠆⟦Q{∧}R⟧
%:             -------------1
%:          (λp⠆P.(fp,gp))⠆⟦P{→}(Q{∧}R)⟧
%:
%:          ^ND-PAT-3
%:
$$\pu\ded{ND-PAT-3}$$

where $⟦P{→}Q⟧ := ⟦P⟧{→}⟦Q⟧$

and $⟦P{∧}Q⟧ := ⟦P⟧×⟦Q⟧$.

\msk

$⟦P⟧$ is the ``type of evidence'' for the proposition $P$.

\msk

In the \ColorRed{simplest model},

$⟦P⟧=∅$ when $P$ is false, and

$⟦P⟧$ is a singleton set when $⟦P⟧$ is true.

\newpage


%  ____   _  _____   _____ 
% |  _ \ / \|_   _| |___ / 
% | |_) / _ \ | |     |_ \ 
% |  __/ ___ \| |    ___) |
% |_| /_/   \_\_|   |____/ 
%                          
% «PAT-3» (to ".PAT-3")
% (ntyp 50 "PAT-3")
% (nty     "PAT-3")

{\bf Propositions-as-types (3)}

\ColorRed{Warning! Warning!}

\msk

In the \ColorRed{simplest model},

$⟦P⟧=∅$ when $P$ is false, and

$⟦P⟧$ is a singleton set when $⟦P⟧$ is true.

\msk

\ColorRed{However,} adults usually prefer the ``BHK interpretation'',

in which $⟦P⟧$ is the \ColorRed{set of proofs} for the proposition $P$...

See section 1.2.3 of \ColorBook{Hermógenes Oliveira's PhD Dissertation:}

\ColorBook{``Inference Rules and the Meaning of the Logical Constants''}

\ColorBook{(2019).}

% (find-books "__logic/__logic.el" "hermogenesoliveira")
% (find-hermogenesolivphdpage (+ 10 11) "1.2.3 The BHK interpretation")
% (find-hermogenesolivphdtext (+ 10 11) "1.2.3 The BHK interpretation")

\newpage

%  ____   _  _____   _  _   
% |  _ \ / \|_   _| | || |  
% | |_) / _ \ | |   | || |_ 
% |  __/ ___ \| |   |__   _|
% |_| /_/   \_\_|      |_|  
%                           
% «PAT-4» (to ".PAT-4")
% (ntyp 51 "PAT-4")
% (nty     "PAT-4")

{\bf Propositions-as-types (4)}

A set is \ColorRed{inhabited} when it has an element.

A set $⟦P⟧$ is inhabited iff $P$ is true.

A proof of $P{→}Q,P{→}R⊢P{→}(Q{∧}R)$ must show that

if $⟦P{→}Q⟧$ and $⟦P{→}R⟧$ are inhabited

then $⟦P{→}(Q{∧}R)⟧$ is inhabited.

Here is \ColorRed{a} proof of $P{→}Q,P{→}R⊢P{→}(Q{∧}R)$:
%
$$f⠆⟦P{→}Q⟧,g⠆⟦P{→}R⟧⊢\ColorRed{(λp⠆P.(fp,gp))}⠆⟦P{→}(Q{∧}R)⟧$$



This term $λp⠆P.(fp,gp)$ can obtained by

1) finding a proof in ND for $P{→}Q,P{→}R⊢P{→}(Q{∧}R)$,

2) interpreting that proof as ``types'',

3) reconstructing its ``terms''...

i.e., by \ColorRed{proof search} followed by \ColorRed{term inference}.





\newpage



%   ___  _          _                   _                      
%  / _ \| |____   _(_) ___  _   _ ___  | |_ ___ _ __ _ __ ___  
% | | | | '_ \ \ / / |/ _ \| | | / __| | __/ _ \ '__| '_ ` _ \ 
% | |_| | |_) \ V /| | (_) | |_| \__ \ | ||  __/ |  | | | | | |
%  \___/|_.__/ \_/ |_|\___/ \__,_|___/  \__\___|_|  |_| |_| |_|
%                                                              
% «obvious-term» (to ".obvious-term")
% (ntyp 52 "obvious-term")
% (nty     "obvious-term")

{\bf The obvious term of type such-and-such}

Suppose that we know a function $f:A→B$ and a set $C$.

Then ``$f$ \ColorRed{induces} a function $(f{×}C):A{×}C→B{×}C$

\ColorRed{in a natural way}''.

\msk

How do we discover the function that

``\ColorRed{deserves the name}'' $(f{×}C)$?

\msk

Trick: ``\ColorRed{in a natural way}'' usually means

``using only the operations from $λ$-calculus'', (!!!!!!!)

i.e., ``a $λ$-term''.


%:
%:      f⠆A{→}B
%:  ===============
%:  (f{×}C)⠆A{×}C{→}B{×}C
%:
%:    ^obvious-1
%:
%:   A{→}B
%:  =============
%:  A{×}C{→}B{×}C
%:
%:  ^obvious-2
%:
%:
%:   [A{×}C]^1
%:   ---------
%:     A        A{→}B    [A{×}C]^1
%:     --------------    ---------
%:         B               C
%:         -----------------
%:               B{×}C
%:          -------------1
%:          A{×}C{→}B{×}C
%:
%:          ^obvious-3
%:
%:   [p⠆A{×}C]^1
%:   ---------
%:     πp⠆A        f⠆A{→}B    [p⠆A{×}C]^1
%:     -------------------    -----------
%:         f(πp)⠆B               π'p⠆C
%:         ---------------------------
%:              (f(πp),π'p)⠆B{×}C
%:          -------------1
%:          (λp⠆A{×}C⠆(f(πp),π'p))⠆A{×}C{→}B{×}C
%:
%:          ^obvious-4
%:
\pu
$$\ded{obvious-1}
  \quad ⇒ \quad
  \ded{obvious-2}
  \quad ⇒ (...)
$$

$\begin{array}{c}
  \ded{obvious-2}
  \quad ⇒ \quad
  \ded{obvious-3}
  \\
  \\
  \quad ⇒ \quad
  \ded{obvious-4}
  \\
  \\
  \quad ⇒ \quad
  (f{×}C) := (λp⠆A{×}C⠆(f(πp),π'p))
 \end{array}
$

\newpage

%   ____ ____ ____     
%  / ___/ ___/ ___|___ 
% | |  | |  | |   / __|
% | |__| |__| |___\__ \
%  \____\____\____|___/
%                      
% «CCCs» (to ".CCCs")
% (ntyp 54 "CCCs")
% (nty     "CCCs")

{\bf Cartesian Closed Categories}

The ability to find

``the obvious term of type such-and-such''

is exactly what we need to learn Category Theory

starting by the ``archetypal CCC'', $\Set$...

\msk

% (lam181p 11 "type-inference")
% (lam181     "type-inference")

%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
\resizebox{0.8\textwidth}{!}{%
$\cdiag{CCC-adj}
 % \quad
 \begin{array}[c]{rcl}
  ({×}C)f &:=& λp{:}A{×}C.(f(πp),π'p) \\
      h^♭ &:=& λq{:}B{×}C.(h(πq))(π'q) \\
     g^♯  &:=& λb{:}B.λc{:}C.g(b,c) \\
 (C{→})k &:=& λφ{:}C{→}D.λc{:}C.k(φc) \\
 \end{array}
$}



%   ____ ____ ____       ____  
%  / ___/ ___/ ___|___  |___ \ 
% | |  | |  | |   / __|   __) |
% | |__| |__| |___\__ \  / __/ 
%  \____\____\____|___/ |_____|
%                              
% «CCCs-2» (to ".CCCs-2")
% (ntyp 55 "CCCs-2")
% (nty     "CCCs-2")

{\bf Cartesian Closed Categories (2)}

Fix an object $C$ of $\Set$. We have ``obvious''

functors $({×}C)$ and $(C{→})$, and an adjunction $({×}C)⊣(C{→})$...

(``obvious'' means ``definable in $λ$-calculus!'')

\msk

\resizebox{0.85\textwidth}{!}{%
$\cdiag{CCC-adj}
 % \quad
 \begin{array}[c]{rcl}
  ({×}C)f &:=& λp{:}A{×}C.(f(πp),π'p) \\
      h^♭ &:=& λq{:}B{×}C.(h(πq))(π'q) \\
     g^♯  &:=& λb{:}B.λc{:}C.g(b,c) \\
 (C{→})k &:=& λφ{:}C{→}D.λc{:}C.k(φc) \\
 \end{array}
$}



\newpage

%  _                _          
% | |    ___   __ _(_) ___ ___ 
% | |   / _ \ / _` | |/ __/ __|
% | |__| (_) | (_| | | (__\__ \
% |_____\___/ \__, |_|\___|___/
%             |___/            
%
% «logics» (to ".logics")
% (ntyp 56 "logics")
% (nty     "logics")

{\bf ``Logics''}

Remember that the (second-semester) course is called

``$λ$-Calculus, \ColorRed{Logics}, and Translations''...

The ``Logics'' is because the course also presents

\ColorRed{Planar Heyting Algebras}, like this one:

\msk

%L mpnew({def="foo",  scale="10pt"}, "12321L"):addcontour():addlrs():output()
%L mpnew({def="foo",  scale="7pt", meta="s"}, "12321L"):addcontour():addlrs():output()
{\pu
$B=\;\foo$
}

\msk

and we see that we can interpret Propositional

Intuitionistic Logic (``PIL'') in $B$ (and later in the course

in any topology!), and that we have a ``logical'' adjunction

$({∧}Q)⊣(Q{→})$... but this doesn't matter for these slides.




\newpage

%  ____            _     _____ 
% |  _ \ __ _ _ __| |_  |___ / 
% | |_) / _` | '__| __|   |_ \ 
% |  __/ (_| | |  | |_   ___) |
% |_|   \__,_|_|   \__| |____/ 
%                              
% «part-3» (to ".part-3")
% (ntyp 57 "part-3")
% (nty     "part-3")
% (ntyp 23 "part-2")
% (nty     "part-2")


\thispagestyle{empty}

% \vspace*{20pt}

\begin{center}

\huge {\bf

\ColorBrown{Part 3}

Dependent types and

Pure Type Systems

% \Large (At PURO/UFF)

}

% \bsk
% 
% \normalsize
% 
% An optional, second-semester-ish,
% 
% hands-on seminar course...
% 
% \ColorBrown{($↑$ based on exercises)}
% 
% \ssk
% 
% I used it to \ColorRed{test} several ideas of the
% 
% ``Logic for Children'' project!...


\end{center}


\newpage


\newpage



% «part-2» (to ".part-2")








Notation:

$A⠆Θ, B⠆Θ, C⠆Θ, p:A×B, g:B→C ⊢ (πp,g(π'p)):A×C$

\newpage

%      _           _                            _       
%     | |_   _  __| | __ _ _ __ ___   ___ _ __ | |_ ___ 
%  _  | | | | |/ _` |/ _` | '_ ` _ \ / _ \ '_ \| __/ __|
% | |_| | |_| | (_| | (_| | | | | | |  __/ | | | |_\__ \
%  \___/ \__,_|\__,_|\__, |_| |_| |_|\___|_| |_|\__|___/
%                    |___/                              
%
% «judgments» (to ".judgments")
% (ntyp 35 "judgments")
% (nty     "judgments")

{\bf Judgments}

Remember that in:

$\setofsc {a∈\{1,2\}, b∈\{2,3\}, a<b} {10a+b} = \{12,13,23\}$

We also have a ``context'' at the left of the `$⊢$',

and we can read

$A⠆Θ, B⠆Θ, C⠆Θ, p:A×B, g:B→C ⊢ (πp,g(π'p)):A×C$

as: for every choice of

\begin{tabular}{l}
a set $\ColorRed{A}$, \\
a set $\ColorRed{B}$, \\
a set $\ColorRed{C}$, \\
$\ColorRed{p}:A×B$, \\
$\ColorRed{g}:B→C$, \\
\end{tabular}

we can calculate $(πp,g(π'p))$ without errors,

and we will have $(πp,g(π'p)) ∈ A×C$.

\newpage

%      _           _                            _         ____  
%     | |_   _  __| | __ _ _ __ ___   ___ _ __ | |_ ___  |___ \ 
%  _  | | | | |/ _` |/ _` | '_ ` _ \ / _ \ '_ \| __/ __|   __) |
% | |_| | |_| | (_| | (_| | | | | | |  __/ | | | |_\__ \  / __/ 
%  \___/ \__,_|\__,_|\__, |_| |_| |_|\___|_| |_|\__|___/ |_____|
%                    |___/                                      
%
% «judgments-2» (to ".judgments-2")
% (ntyp 60 "judgments-2")
% (nty     "judgments-2")

{\bf Judgments (2)}

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

Remember that in

$\setofsc {\uC{\ug{a∈\{1,2\}}, \ug{b∈\{2,3\}}, \uf{a<b}}} {\ue{10a+b}}$

the context has ``generators'' (``{\sl var} $∈$ {\sl set}'')

and ``filters'' (``{\sl this expression must be true}'').

\msk

In

$\uC{\uvt{A⠆Θ}, \uvt{B⠆Θ}, \uvt{C⠆Θ}, \uvt{p:A×B}, \uvt{g:B→C}} ⊢
 \uconc{\uterm{(πp,g(π'p))}:\utype{A×C}}
$

the context is made of several declarations of the form

``variable : type''...

\newpage

%      _           _                            _         _____ 
%     | |_   _  __| | __ _ _ __ ___   ___ _ __ | |_ ___  |___ / 
%  _  | | | | |/ _` |/ _` | '_ ` _ \ / _ \ '_ \| __/ __|   |_ \ 
% | |_| | |_| | (_| | (_| | | | | | |  __/ | | | |_\__ \  ___) |
%  \___/ \__,_|\__,_|\__, |_| |_| |_|\___|_| |_|\__|___/ |____/ 
%                    |___/                                      
%
% «judgments-3» (to ".judgments-3")
% (ntyp 61 "judgments-3")
% (nty     "judgments-3")

{\bf Judgments (3)}

If we think --- \ColorRed{informally} --- that

$Θ$ is the ``set of all sets'' (mnemonic: Theta for ``Theths''),

then we can put these judgments for $λ$-calculus in

a very homogeneous form...

\msk

$\uC{\uvt{A⠆Θ}, \uvt{B⠆Θ}, \uvt{C⠆Θ}, \uvt{p:A×B}, \uvt{g:B→C}} ⊢
 \uconc{\uterm{(πp,g(π'p))}:\utype{A×C}}
$

\msk

the context is a series of declarations of the form ``var : type'',

and the conclusion is of the form ``term : type''.

\newpage



%  ____ _____    ____                                _   
% / ___|_   _|  / ___|   _ _ __ _ __ _   _       ___| |_ 
% \___ \ | |   | |  | | | | '__| '__| | | |_____/ __| __|
%  ___) || |   | |__| |_| | |  | |  | |_| |_____\__ \ |_ 
% |____/ |_|    \____\__,_|_|  |_|   \__, |     |___/\__|
%                                    |___/               
%
% «simple-typing-csla» (to ".simple-typing-csla")
% (ntyp 70 "simple-typing-csla")
% (nty     "simple-typing-csla")

{\bf ``Simple typing, Curry-style in $λ$''}

$(↑)$ This is the title of chapter 12 in Hindley/Seldin (2008).

Here is a derivation in their system $\TALA$, from p.161:
%
% (find-books "__logic/__logic.el" "hindley-seldin2")
% (find-hindleyseldin2page (+ 14 159) "12A The system TA")
%:
%:       1         2            3         2         
%:   .........   .....       .......   .....       
%:   [x:ρ→σ→τ]   [z:ρ]       [y:ρ→σ]   [z:ρ]       
%:   -----------------(→𝐫e)  ---------------(→𝐫e)   
%:        xz:σ→τ                  yz:σ             
%:        ----------------------------(→𝐫e)
%:                xz(yz):τ
%:            -----------------(→𝐫i-2)
%:            λz.xz(yz):(ρ→τ)
%:          --------------------(→𝐫i-3)
%:          λyz.xz(yz):(ρ→σ)→ρ→τ
%:       -----------------------------(→𝐫i-1)
%:       λxyz.xz(yz):(ρ→σ→τ)→(ρ→σ)→ρ→τ
%:
%:       ^p161-below
%:
\pu
$$\ded{p161-below}$$

\newpage

%  ____ _____    ____                                _     ____  
% / ___|_   _|  / ___|   _ _ __ _ __ _   _       ___| |_  |___ \ 
% \___ \ | |   | |  | | | | '__| '__| | | |_____/ __| __|   __) |
%  ___) || |   | |__| |_| | |  | |  | |_| |_____\__ \ |_   / __/ 
% |____/ |_|    \____\__,_|_|  |_|   \__, |     |___/\__| |_____|
%                                    |___/                       
%
% «simple-typing-csla-2» (to ".simple-typing-csla-2")
% (ntyp 39 "simple-typing-csla-2")
% (nty     "simple-typing-csla-2")

{\bf ``Simple typing, Curry-style in $λ$'' (2)}

If we take the previous derivation,

rename $\subst{ρ:=A \\ σ:=B \\ τ:=C \\ z:=a \\ y:=f \\ x:=g}$ in it,

add some parentheses, and rewrite $λgfa$ to $λg.λf.λa$, we get:

% (fooi "ρ" "A" "σ" "B" "τ" "C")
% (fooi "z" "a")
% (fooi "y" "f" "x" "g")
%:
%:       1         2            3         2         
%:   .........   .....       .......   .....       
%:   [g:A→(B→C)] [a:A]       [f:A→B]   [a:A]       
%:   -----------------(→𝐫e)  ---------------(→𝐫e)   
%:        ga:B→C                  fa:B             
%:        ----------------------------(→𝐫e)
%:                (ga)(fa):C
%:            -----------------(→𝐫i-2)
%:            λa.(ga)(fa):A→C
%:          --------------------(→𝐫i-3)
%:          λf.λa.(ga)(fa):(A→B)→(A→C)
%:       -----------------------------(→𝐫i-1)
%:       λg.λf.λa.(ga)(fa):(A→(B→C))→((A→B)→(A→C))
%:
%:       ^p161-below-2
%:

\msk

\pu
\resizebox{1.0\textwidth}{!}{%
$\ded{p161-below-2}
$}


\newpage

%  ____ _____    ____                                _     _____ 
% / ___|_   _|  / ___|   _ _ __ _ __ _   _       ___| |_  |___ / 
% \___ \ | |   | |  | | | | '__| '__| | | |_____/ __| __|   |_ \ 
%  ___) || |   | |__| |_| | |  | |  | |_| |_____\__ \ |_   ___) |
% |____/ |_|    \____\__,_|_|  |_|   \__, |     |___/\__| |____/ 
%                                    |___/                       
%
% «simple-typing-csla-3» (to ".simple-typing-csla-3")
% (ntyp 40 "simple-typing-csla-3")
% (nty     "simple-typing-csla-3")

{\bf ``Simple typing, Curry-style in $λ$'' (3)}

If we rename its rules to `$\app$' and `$λ$'

and change the notation for discharge of hypotheses a bit,

we get:

%:   [g:A→(B→C)]^1 [a:A]^2   [f:A→B]^3   [a:A]^2       
%:   -----------------\app   ---------------\app   
%:        ga:B→C                  fa:B             
%:        ----------------------------\app
%:                (ga)(fa):C
%:            -----------------λ;2
%:            λa.(ga)(fa):A→C
%:          --------------------λ;3
%:          λf.λa.(ga)(fa):(A→B)→(A→C)
%:       -----------------------------λ;1
%:       λg.λf.λa.(ga)(fa):(A→(B→C))→((A→B)→(A→C))
%:
%:       ^p161-below-3
%:

\msk

\pu
\resizebox{1.0\textwidth}{!}{%
$\ded{p161-below-3}
$}


\newpage

%  ____ _____    ____                                _     _  _   
% / ___|_   _|  / ___|   _ _ __ _ __ _   _       ___| |_  | || |  
% \___ \ | |   | |  | | | | '__| '__| | | |_____/ __| __| | || |_ 
%  ___) || |   | |__| |_| | |  | |  | |_| |_____\__ \ |_  |__   _|
% |____/ |_|    \____\__,_|_|  |_|   \__, |     |___/\__|    |_|  
%                                    |___/                        
%
% «simple-typing-csla-4» (to ".simple-typing-csla-4")
% (ntyp 41 "simple-typing-csla-4")
% (nty     "simple-typing-csla-4")

{\bf ``Simple typing, Curry-style in $λ$'' (4)}

If we interpret a rule like `$λ;2$' as

``introduce a `λ' and \ColorRed{discharge} the hypothesis `2' '',

and we use a $⊢$ to display the \ColorRed{undischarged hypotheses}

at \ColorRed{some} nodes starting from the bottom, we get:


%:   [g⠆A→(B→C)]^1 [a⠆A]^2   [f⠆A→B]^3   [a⠆A]^2       
%:   -----------------\app   ---------------\app   
%:        ga⠆B→C                  fa⠆B             
%:        ----------------------------\app
%:         \red{a⠆A,f⠆A→B,g⠆A→(B→C)⊢}(ga)(fa)⠆C
%:         -------------------------------λ;2
%:            \red{f⠆A→B,g⠆A→(B→C)⊢}λa.(ga)(fa)⠆A→C
%:       ------------------------------------λ;3
%:       \red{g⠆A→(B→C)⊢}λf.λa.(ga)(fa)⠆(A→B)→(A→C)
%:       -------------------------------------λ;1
%:       \red{⊢}λg.λf.λa.(ga)(fa)⠆(A→(B→C))→((A→B)→(A→C))
%:
%:       ^p161-below-4
%:

\msk

\pu
\resizebox{1.0\textwidth}{!}{%
\def→{{\to}}
\def\red#1{\ColorRed{#1}\,}
$\ded{p161-below-4}
$}

\msk

The undischarged hypotheses are exactly the \ColorRed{free variables}!

\newpage

%  ____ _____    ____                                _     ____  
% / ___|_   _|  / ___|   _ _ __ _ __ _   _       ___| |_  | ___| 
% \___ \ | |   | |  | | | | '__| '__| | | |_____/ __| __| |___ \ 
%  ___) || |   | |__| |_| | |  | |  | |_| |_____\__ \ |_   ___) |
% |____/ |_|    \____\__,_|_|  |_|   \__, |     |___/\__| |____/ 
%                                    |___/                       
%
% «simple-typing-csla-5» (to ".simple-typing-csla-5")
% (ntyp 42 "simple-typing-csla-5")
% (nty     "simple-typing-csla-5")

{\bf ``Simple typing, Curry-style in $λ$'' (5)}

If we extend the idea

``\ColorBrown{The undischarged hypotheses are exactly the free variables}''

to the nodes in the second line, inheriting the order

from below --- first $a$, then $f$, then $g$ --- we get:

%:   [g⠆A→(B→C)]^1 [a⠆A]^2        [f⠆A→B]^3   [a⠆A]^2       
%:   -----------------\app        ---------------\app   
%:   \red{a⠆A,g⠆A→(B→C)⊢}ga⠆B→C   \red{a⠆A,f⠆A→B⊢}fa⠆B             
%:        ----------------------------\app
%:         \red{a⠆A,f⠆A→B,g⠆A→(B→C)⊢}(ga)(fa)⠆C
%:         -------------------------------λ;2
%:            \red{f⠆A→B,g⠆A→(B→C)⊢}λa.(ga)(fa)⠆A→C
%:       ------------------------------------λ;3
%:       \red{g⠆A→(B→C)⊢}λf.λa.(ga)(fa)⠆(A→B)→(A→C)
%:       -------------------------------------λ;1
%:       \red{⊢}λg.λf.λa.(ga)(fa)⠆(A→(B→C))→((A→B)→(A→C))
%:
%:       ^p161-below-5
%:

\msk

\pu
\resizebox{1.0\textwidth}{!}{%
\def→{{\to}}
\def\red#1{\ColorRed{#1}\,}
$\ded{p161-below-5}
$}

\newpage

%  ____ _____    ____                                _      __   
% / ___|_   _|  / ___|   _ _ __ _ __ _   _       ___| |_   / /_  
% \___ \ | |   | |  | | | | '__| '__| | | |_____/ __| __| | '_ \ 
%  ___) || |   | |__| |_| | |  | |  | |_| |_____\__ \ |_  | (_) |
% |____/ |_|    \____\__,_|_|  |_|   \__, |     |___/\__|  \___/ 
%                                    |___/                       
%
% «simple-typing-csla-6» (to ".simple-typing-csla-6")
% (ntyp 43 "simple-typing-csla-6")
% (nty     "simple-typing-csla-6")

{\bf ``Simple typing, Curry-style in $λ$'' (6)}

The passage from the 2nd line to the 3rd line takes the contexts

``$a⠆...,g⠆...⊢$'' and ``$a⠆...,f⠆...⊢$'' above the line and produces

a context ``$a⠆...,f⠆...,g⠆...⊢$'' below, that is the \ColorRed{union}

of the the contexts above:

\msk 

\pu
\resizebox{1.0\textwidth}{!}{%
\def→{{\to}}
\def\red#1{\ColorRed{#1}\,}
$\ded{p161-below-5}
$}

\newpage
 
%  ____ _____    ____                                _     _____ 
% / ___|_   _|  / ___|   _ _ __ _ __ _   _       ___| |_  |___  |
% \___ \ | |   | |  | | | | '__| '__| | | |_____/ __| __|    / / 
%  ___) || |   | |__| |_| | |  | |  | |_| |_____\__ \ |_    / /  
% |____/ |_|    \____\__,_|_|  |_|   \__, |     |___/\__|  /_/   
%                                    |___/                       
%
% «simple-typing-csla-7» (to ".simple-typing-csla-7")
% (ntyp 44 "simple-typing-csla-7")
% (nty     "simple-typing-csla-7")

{\bf ``Simple typing, Curry-style in $λ$'' (7)}

If we extend these two ideas --- free variables and union ---

to the top line, we get this:

%:   [\red{g⠆A→(B→C)⊢}g⠆A→(B→C)]^1 [\red{a⠆A⊢}a⠆A]^2   [\red{f⠆A→B⊢}f⠆A→B]^3   [\red{a⠆A⊢}a⠆A]^2       
%:   -------------------------------------------\app   -------------------------------------\app   
%:            \red{a⠆A,g⠆A→(B→C)⊢}ga⠆B→C                 \red{a⠆A,f⠆A→B⊢}fa⠆B             
%:         ----------------------------------------------------------------\app
%:         \red{a⠆A,f⠆A→B,g⠆A→(B→C)⊢}(ga)(fa)⠆C
%:         -------------------------------λ;2
%:            \red{f⠆A→B,g⠆A→(B→C)⊢}λa.(ga)(fa)⠆A→C
%:       ------------------------------------λ;3
%:       \red{g⠆A→(B→C)⊢}λf.λa.(ga)(fa)⠆(A→B)→(A→C)
%:       -------------------------------------λ;1
%:       \red{⊢}λg.λf.λa.(ga)(fa)⠆(A→(B→C))→((A→B)→(A→C))
%:
%:       ^p161-below-7
%:

\msk

\pu
\resizebox{1.0\textwidth}{!}{%
\def→{{\to}}
\def\red#1{\ColorRed{#1}\,}
$\ded{p161-below-7}
$}

\newpage

%  ____ _____    ____                                _      ___  
% / ___|_   _|  / ___|   _ _ __ _ __ _   _       ___| |_   ( _ ) 
% \___ \ | |   | |  | | | | '__| '__| | | |_____/ __| __|  / _ \ 
%  ___) || |   | |__| |_| | |  | |  | |_| |_____\__ \ |_  | (_) |
% |____/ |_|    \____\__,_|_|  |_|   \__, |     |___/\__|  \___/ 
%                                    |___/                       
%
% «simple-typing-csla-8» (to ".simple-typing-csla-8")
% (ntyp 45 "simple-typing-csla-8")
% (nty     "simple-typing-csla-8")

{\bf ``Simple typing, Curry-style in $λ$'' (8)}

If we extend these two ideas to the top line

and we erase the things like `$[\;]^2$' and `$;2$',

we get something whose \ColorRed{intuitive semantics} is very simple,

and that will be our motivation for more advanced

type systems...

\msk

%:   -------------------------  -------------    -----------------   -------------
%:   \red{g⠆A→(B→C)⊢}g⠆A→(B→C)  \red{a⠆A⊢}a⠆A    \red{f⠆A→B⊢}f⠆A→B   \red{a⠆A⊢}a⠆A       
%:   --------------------------------------\app  ---------------------------------\app   
%:            \red{a⠆A,g⠆A→(B→C)⊢}ga⠆B→C                 \red{a⠆A,f⠆A→B⊢}fa⠆B             
%:         ----------------------------------------------------------------\app
%:         \red{a⠆A,f⠆A→B,g⠆A→(B→C)⊢}(ga)(fa)⠆C
%:         -------------------------------λ
%:            \red{f⠆A→B,g⠆A→(B→C)⊢}λa.(ga)(fa)⠆A→C
%:       ------------------------------------λ
%:       \red{g⠆A→(B→C)⊢}λf.λa.(ga)(fa)⠆(A→B)→(A→C)
%:       -------------------------------------λ
%:       \red{⊢}λg.λf.λa.(ga)(fa)⠆(A→(B→C))→((A→B)→(A→C))
%:
%:       ^p161-below-8
%:

\pu
\resizebox{1.0\textwidth}{!}{%
\def→{{\to}}
\def\red#1{\ColorRed{#1}\,}
$\ded{p161-below-8}
$}

\msk

...but this derivation \ColorRed{suggests} that the judgments in the
top line are \ColorRed{axioms}. Let's change this...

\newpage

%  ____ _____    ____                                _      ___  
% / ___|_   _|  / ___|   _ _ __ _ __ _   _       ___| |_   / _ \ 
% \___ \ | |   | |  | | | | '__| '__| | | |_____/ __| __| | (_) |
%  ___) || |   | |__| |_| | |  | |  | |_| |_____\__ \ |_   \__, |
% |____/ |_|    \____\__,_|_|  |_|   \__, |     |___/\__|    /_/ 
%                                    |___/                       
%
% «simple-typing-csla-9» (to ".simple-typing-csla-9")
% (ntyp 46 "simple-typing-csla-9")
% (nty     "simple-typing-csla-9")

{\bf ``Simple typing, Curry-style in $λ$'' (9)}

Let's create a rule `$𝐬v$' that works like this: ``if $A{→}B$ is a set
then we can introduce a variable whose domain is $A{→}B$'',

and a rule `$→$' that works like this: ``if $A$ is a set and $B{→}C$
is a set then $A{→}(B{→}C)$ is a set:

\msk

%:
%:               B⠆Θ  C⠆Θ
%:               --------→
%:        A⠆Θ     B→C⠆Θ                                A⠆Θ  B⠆Θ
%:        -------------→                               --------→
%:          A→(B→C)⠆Θ                 A⠆Θ                A→B⠆Θ             A⠆Θ
%:   -------------------------𝐬v  -------------𝐬v  -----------------   -------------
%:   \red{g⠆A→(B→C)⊢}g⠆A→(B→C)    \red{a⠆A⊢}a⠆A    \red{f⠆A→B⊢}f⠆A→B   \red{a⠆A⊢}a⠆A       
%:   --------------------------------------\app    ---------------------------------\app   
%:            \red{a⠆A,g⠆A→(B→C)⊢}ga⠆B→C                 \red{a⠆A,f⠆A→B⊢}fa⠆B             
%:         ----------------------------------------------------------------\app
%:         \red{a⠆A,f⠆A→B,g⠆A→(B→C)⊢}(ga)(fa)⠆C
%:         -------------------------------λ
%:            \red{f⠆A→B,g⠆A→(B→C)⊢}λa.(ga)(fa)⠆A→C
%:       ------------------------------------λ
%:       \red{g⠆A→(B→C)⊢}λf.λa.(ga)(fa)⠆(A→B)→(A→C)
%:       -------------------------------------λ
%:       \red{⊢}λg.λf.λa.(ga)(fa)⠆(A→(B→C))→((A→B)→(A→C))
%:
%:       ^p161-below-9
%:

\pu
\resizebox{1.0\textwidth}{!}{%
\def→{{\to}}
\def\red#1{\ColorRed{#1}\,}
$\ded{p161-below-9}
$}


\newpage

%  ____ _____    ____                                _     _  ___  
% / ___|_   _|  / ___|   _ _ __ _ __ _   _       ___| |_  / |/ _ \ 
% \___ \ | |   | |  | | | | '__| '__| | | |_____/ __| __| | | | | |
%  ___) || |   | |__| |_| | |  | |  | |_| |_____\__ \ |_  | | |_| |
% |____/ |_|    \____\__,_|_|  |_|   \__, |     |___/\__| |_|\___/ 
%                                    |___/                         
%
% «simple-typing-csla-10» (to ".simple-typing-csla-10")
% (ntyp 47 "simple-typing-csla-10")
% (nty     "simple-typing-csla-10")

{\bf ``Simple typing, Curry-style in $λ$'' (10)}

If we fold, as in an accordion,

the middle part of the last derivation, we get:

\bsk

%:
%:        A⠆Θ   B⠆Θ  C⠆Θ
%:       ==========================================
%:       ⊢λg.λf.λa.(ga)(fa)⠆(A→(B→C))→((A→B)→(A→C))
%:
%:       ^p161-below-10
%:
\pu
\resizebox{1.0\textwidth}{!}{%
\def→{{\to}}
\def\red#1{\ColorRed{#1}\,}
$\ded{p161-below-10}
$}

\bsk

and we can interpret this as:

if we know the values of $A,B,C$ (and they are ``$⠆Θ$'', i.e., sets),

then the judgement below the double bar is true.

For example, this holds when

$A=\{1,2\}$, $B=\{3,4\}$, $C=\{5,6\}$.


\newpage

%  ____             _      _          _                         
% | __ )  __ _  ___| | __ | |_ ___   | |_ _   _ _ __   ___  ___ 
% |  _ \ / _` |/ __| |/ / | __/ _ \  | __| | | | '_ \ / _ \/ __|
% | |_) | (_| | (__|   <  | || (_) | | |_| |_| | |_) |  __/\__ \
% |____/ \__,_|\___|_|\_\  \__\___/   \__|\__, | .__/ \___||___/
%                                         |___/|_|              
%
% «back-to-types» (to ".back-to-types")
% (ntyp 48 "back-to-types")
% (nty     "back-to-types")
% (nty "types-2")

{\bf Back to types}

Remember that we had:

\msk

1) if $\ColorRed{f:A→B}$ and $\ColorRed{a:A}$ then $\ColorRed{f(a):B}$

2) if $\ColorRed{a:A}$ and $\ColorRed{b:B}$ then $\ColorRed{(a,b):A×B}$

3) if $\ColorRed{p:A×B}$ then $\ColorRed{πp:A}$ and $\ColorRed{π'p:B}$

\msk

and:

\msk

$\def→{{\to}}
 \ded{p161-below-10}
$


\newpage



% «back-to-types-2» (to ".back-to-types-2")
% (ntyp ?? "back-to-types-2")
% (nty     "back-to-types-2")

{\bf back-to-types-2}


Let's try to list all the rules that we saw up to this point.

We have rules that produce new sets, and

rules that produce new elements of sets.

The only rules that do something strange to the context

are the rule `$λ$', that moves a hypothesis from the context

to the $λ$, and the rule `$𝐬v$', the introduces a new variable

at both sides of the `$⊢$'...


%:
%:  A⠆Θ  B⠆Θ    A⠆Θ  B⠆Θ    f⠆A{→}B  a⠆A
%:  --------×   --------→   ------------\app
%:  A{×}B:Θ     A{→}B:Θ        fa
%:
%:  ^rux        ^ru->          ^app
%:
%:
%:
%:
%:
%:



\newpage


%  ___                            _ _   _           
% |_ _|_ __ ___  _ __  _   _ _ __(_) |_(_) ___  ___ 
%  | || '_ ` _ \| '_ \| | | | '__| | __| |/ _ \/ __|
%  | || | | | | | |_) | |_| | |  | | |_| |  __/\__ \
% |___|_| |_| |_| .__/ \__,_|_|  |_|\__|_|\___||___/
%               |_|                                 
%
% «impurities» (to ".impurities")
% (ntyp 47 "impurities")
% (nty     "impurities")

{\bf Impurities}

We are using a non-standard trick here to present $λ$-calculus in a
way that feels concrete. I call it ``\ColorRed{impurities}''.

I learned \ColorRed{Pure Type Systems} ages ago (2002?) from Herman
Geuvers's PhD thesis. Everything was very abstract in it (no
semantics! No intuition!), and very syntactical. He didn't explain
what ``pure'' means...

Let me show an abstract of a talk that I gave in 2002.

\newpage

{\bf ``A System of Natural Deduction for Categories''}

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

% (find-LATEX "2002fmcs.tex" "abstract")

Abstract:

\ssk

We will present a logic (system DNC) whose terms represent categories,
objects, morphisms, functors, natural transformations, sets, points,
and functions, and whose rules of deduction represent certain
constructive operations involving those entities. Derivation trees in
this system only represent the ``T-part'' (for ``terms'' and
``types'') of the constructions, not the ``P-part'' (``proofs'' and
``propositions''): the rules that generate functors and natural
transformations do not check that they obey the necessary equations.
So, we can see derivations in this system either as constructions
happening in a ``syntactical world'', that should be related to the
``real world'' in some way (maybe through meta-theorems that are yet to
be found), or as being just ``skeletons'' of the real constructions,
with the P-parts having been omitted for briefness.

\ColorGray{(2nd paragraph deleted)}

The way to formalize DNC, and to provide a translation between terms
in its ``logic'' and the usual notations for Category Theory, is based
on the following idea. Take a derivation tree $D$ in the Calculus of
Constructions, and erase all the contexts and all the typings that
appear in it; also erase all the deduction steps that now look
redundant. Call the new tree $D'$. If the original derivation, $D$,
obeys some mild conditions, then it is possible to reconstruct it ---
modulo exchanges and unessential weakenings in the contexts --- from
$D'$, that is much shorter. The algorithm that does the reconstruction
generates as a by-product a ``dictionary'' that tells the type and the
``minimal context'' for each term that appears in $D'$; by extending
the language that the dictionary can deal with we get a way to
translate DNC terms and trees --- and also, curiously, with a few
tricks more, and with some minimal information to ``bootstrap'' the
dictionary, categorical diagrams written in a DNC-like language.

\ColorGray{(End of the abstract.)}

\msk

So


 I started to add ``impurities'' to PTSs an in
\ColorRed{informal} way, mixing PTS syntax and mathema


 to be able to present judgments in a





I gave some talks that 

To make a long story short, I added ``impurities'' to a Pure Type
System --- in an \ColorRed{informal} way! --- to be able to present
PTS 



Here is a part of the 


I was working on a kind of ``Curry-Howard for CT'' 



I gave some talks that year

I had to make some presentations in conferences that year 

Note that we started from expressions with `$λ$'s and types that were
quite concrete, like








% (lam181p 22 "exponentials")
% (find-LATEXgrep "grep --color -nH -e lam181p 2018-1-LA-material.tex")
% (lam181p 1 "introduction")
% (lam181p 2 "expressions-and-reductions")
% (lam181p 3 "expressions-with-vars")
% (lam181p 4 "subst-and-copy")
% (lam181p 5 "lambda")
% (lam181p 6 "lambda-exercises")
% (lam181p 7 "function-graphs")
% (lam181p 9 "typed-L1-trees")
% (lam181p 10 "types-exercises")
% (lam181p 11 "type-inference")
% (lam181p 12 "term-inference")
% (lam181p 13 "term-inference-answers")
% (lam181p 14 "contexts")
% (lam181p 15 "curry-howard-0")
% (lam181p 16 "curry-howard-1")
% (lam181p 17 "ZHAs-1")
% (lam181p 18 "algebraic-structures")
% (lam181p 19 "protocategories")
% (lam181p 20 "composition")
% (lam181p 21 "multiple-inverses")
% (lam181p 22 "exponentials")



%  ___                            _ _   _           
% |_ _|_ __ ___  _ __  _   _ _ __(_) |_(_) ___  ___ 
%  | || '_ ` _ \| '_ \| | | | '__| | __| |/ _ \/ __|
%  | || | | | | | |_) | |_| | |  | | |_| |  __/\__ \
% |___|_| |_| |_| .__/ \__,_|_|  |_|\__|_|\___||___/
%               |_|                                 
%




%  _      __  ____ 
% | |    / _|/ ___|
% | |   | |_| |    
% | |___|  _| |___ 
% |_____|_|  \____|
%                  
% «logic-for-children» (to ".logic-for-children")

{\bf Interlude: Logic for Children}

From the webpage of the LfC workshop at the UniLog 2018:

\msk

The \ColorRed{``children''} in ``logic for children'' means ``people
without mathematical maturity'', which in its turn \ColorRed{means
  people who:}

\def\myitem{$•$}
\def\myitem{$\;\;•\;\;$}

\msk

\myitem have trouble with very abstract definitions,

\myitem prefer to start from particular cases (and then generalize),

\myitem handle diagrams better than algebraic notations,

\myitem like to use diagrams and analogies.

\msk

If we say that \ColorRed{categorical definitions} are ``for adults''
--- because they may be very abstract --- and that
\ColorRed{particular cases, diagrams, and analogies} are ``for
children'', then our intent with this workshop becomes easy to state.
``Children'' are willing to use ``tools for children'' to do
mathematics, even if...

\newpage

%  _      __  ____   ____  
% | |    / _|/ ___| |___ \ 
% | |   | |_| |       __) |
% | |___|  _| |___   / __/ 
% |_____|_|  \____| |_____|
%                          
% «logic-for-children-2» (to ".logic-for-children-2")

{\bf Logic for Children (2)}

From the webpage of the LfC workshop at the UniLog 2018:

\msk

(...) ``Children'' are willing to use ``tools for children'' to do
mathematics, even if they will have to translate everything to a
language ``for adults'' to make their results dependable and
publishable, and even if the bridge between their tools ``for
children'' and ``for adults'' is somewhat defective, i.e., if the
translation only works on simple cases...

We are interested in that \ColorRed{bridge} between maths ``for
adults'' and ``for children'' in several areas. Maths ``for children''
are hard to publish, even informally as notes (see this thread in the
Categories mailing list), so often techniques are rediscovered over
and over, but kept restricted to the ``oral culture'' of the area.



\newpage

%  _      __  ____   _              _     
% | |    / _|/ ___| | |_ ___   ___ | |___ 
% | |   | |_| |     | __/ _ \ / _ \| / __|
% | |___|  _| |___  | || (_) | (_) | \__ \
% |_____|_|  \____|  \__\___/ \___/|_|___/
%                                         
% «logic-for-children-tools» (to ".logic-for-children-tools")

{\bf Logic for Children: tools}

We are going to use three ``tools for children here''...

1. Parallel diagrams: particular / general

% (vgmp 12 "parallel")
% (vgm     "parallel")
% (vivp 10 "children")
% (viv     "children")

\def\tm #1#2{       \begin{tabular}{#1}#2\end{tabular}}
\def\ptm#1#2{\left (\begin{tabular}{#1}#2\end{tabular}\right )}
\def\smm#1#2{\sm{\text{#1}\\\text{#2}}}
%
$$\ptm{c}{particular \\ case \\ ``for children''}
  \two/<-`->/<500>^{\smm{particularize}{(easy)}}_{\smm{generalize}{(hard)}}
  \ptm{c}{general \\ case \\ ``for adults''}
$$

The diagrams for the general case and for a particular case

have the same shape --- or have very similar shapes.


\newpage


%  _      __  ____   _              _       ____  
% | |    / _|/ ___| | |_ ___   ___ | |___  |___ \ 
% | |   | |_| |     | __/ _ \ / _ \| / __|   __) |
% | |___|  _| |___  | || (_) | (_) | \__ \  / __/ 
% |_____|_|  \____|  \__\___/ \___/|_|___/ |_____|
%                                                 
% «logic-for-children-tools-2» (to ".logic-for-children-tools-2")
% (vivp 22 "internal-views")
% (viv     "internal-views")

{\bf Logic for Children: tools (2)}

We are going to use three ``tools for children here''...

2. External / internal views (`$→$' / `$↦$')
%
\def\ooo(#1,#2){\begin{picture}(0,0)\put(0,0){\oval(#1,#2)}\end{picture}}
\def\oooo(#1,#2){{\setlength{\unitlength}{1ex}\ooo(#1,#2)}}
%
%D diagram second-blob-function
%D 2Dx     100 +20   +20   
%D 2D  100 a-1 |-->  b-1    
%D 2D  +08 a0  |-->  b0    
%D 2D  +08 a1  |-->  b1    
%D 2D  +08 a2  |-->  b2    
%D 2D  +08 a3  |-->  b3    
%D 2D  +08 a4  |-->  b4    
%D 2D  +14 a5  |-->  b5    
%D 2D  +25 \N  --->  \R
%D 2D
%D ren a-1 a0 a1 a2 a3 a4 a5 ==> -1 0 1 2 3 4 n
%D ren b-1 b0 b1 b2 b3 b4 b5 ==> -1 0 1 \sqrt{2} \sqrt{3} 2 \sqrt{n}
%D ((  a0 a5 midpoint .TeX= \oooo(7,23) y+= -2 place
%D    b-1 b5 midpoint .TeX= \oooo(7,25) y+= -2 place
%D       b-1 place
%D    a0 b0 |->
%D    a1 b1 |->
%D    a2 b2 |->
%D    a3 b3 |->
%D    a4 b4 |->
%D    a5 b5 |->
%D    \N \R -> .plabel= a \sqrt{\phantom{a}}
%D    a-1 relplace -7 -7 \phantom{foo}
%D    b5  relplace  7  7 \phantom{bar}
%D ))
%D enddiagram
%D
$$\pu
  \begin{array}[c]{rrcl}
  \sqrt{\phantom{a}}: & \N &→& \R \\
                      & n  &↦& \sqrt{n} \\
  \end{array}
  %
  \qquad
  %
  \resizebox{3.0cm}{!}{$\diag{second-blob-function}$}
  \qquad
$$

\newpage

%  _      __  ____   _              _       _____ 
% | |    / _|/ ___| | |_ ___   ___ | |___  |___ / 
% | |   | |_| |     | __/ _ \ / _ \| / __|   |_ \ 
% | |___|  _| |___  | || (_) | (_) | \__ \  ___) |
% |_____|_|  \____|  \__\___/ \___/|_|___/ |____/ 
%                                                 
% «logic-for-children-tools-3» (to ".logic-for-children-tools-3")
% (vivp 22 "internal-views")
% (viv     "internal-views")

{\bf Logic for Children: tools (3)}

We are going to use three ``tools for children here''...

3. \ColorRed{The} object ``deserving a name''


%D diagram xC
%D 2Dx     100 +30 +30 +30
%D 2D  100 A1  A2  B1  B2
%D 2D
%D 2D  +30 A3  A4  B3  B4
%D 2D
%D ren A1 A2 ==> A A{×}C
%D ren A3 A4 ==> B B{×}C
%D ren B1 B2 ==> a (a,c)
%D ren B3 B4 ==> b (b,c)
%D
%D (( A1 A2 |-> .plabel= a ({×}C)
%D    A1 A3  -> .plabel= l f
%D    A2 A4  -> .plabel= r (×C)f
%D    A1 A4 harrownodes nil 20 nil |->
%D    A3 A4 |->
%D
%D    B1 B2  =>
%D    B1 B3 |->
%D    B2 B4 |->
%D    B1 B4 harrownodes nil 20 nil |->
%D    B3 B4  =>
%D ))
%D enddiagram
%D
\pu

\bsk

\resizebox{1.0\textwidth}{!}{$
  \cdiag{xC}
  \quad
  \begin{array}[c]{rrl}
  ({×}C)(A) &:=& A×C \\
  ({×}C)(f) &:=& ((a,c)↦(b,c)) \\
             &=& (λ(a,c).(b,c)) \\
             &=& (λ(a,c).(f(a),c)) \\
             &=& (λ(a,c).(f(π(a,c)),π'(a,c))) \\
             &=& (λp.(f(πp),π'p)) \\
  \end{array}
$}

\bsk

{\scriptsize

\ColorBrown{

Note: I was \ColorRed{obsessed} by this idea for years, but it took me
a long time to formalize it... it was incredibly useful as a private
notation, but it seemed to work only in small examples. The trick to
make it work is to use \ColorRed{dictionaries}.

\ssk

Article: ``Internal Diagrams and Archetypal Reasoning in Category
Theory'' [Ochs2013]. I still love about 80\% of it, but I abandoned
the idea of ``downcasing types''.

\ssk

In the course about $λ$-Calculus, Logics, and Translation I don't even
mention to the students that that paper exists.

}

}


\newpage

{\bf End of the interlude}

Let's go back to what our (2nd-semester) students see in the course!


\newpage




%  ____                                     __    __                 
% / ___| _ __   __ _  ___ ___  ___    ___  / _|  / _|_   _ _ __  ___ 
% \___ \| '_ \ / _` |/ __/ _ \/ __|  / _ \| |_  | |_| | | | '_ \/ __|
%  ___) | |_) | (_| | (_|  __/\__ \ | (_) |  _| |  _| |_| | | | \__ \
% |____/| .__/ \__,_|\___\___||___/  \___/|_|   |_|  \__,_|_| |_|___/
%       |_|                                                          
%
% «spaces-of-functions» (to ".spaces-of-functions")

{\bf Spaces of functions}

Let: $A=\{1,2\}$, $B=\{3,4\}$, $C_1=\{5,6\}$, $C_2=\{7,8,9\}$.

If $f:A→B$ then there are four possible values for $f$...

Trick: our \ColorRed{first} interpretation for `:' is `$∈$',

and $A→B$ is $B^A$ --- the set of functions from $A$ to $B$.

\msk

$f:A→B$ means that $f$ can be

$\{(1,3),(2,3)\}$ or

$\{(1,3),(2,4)\}$ or

$\{(1,4),(2,3)\}$ or

$\{(1,4),(2,4)\}$, so

$(A→B) = B^A = \csm{
  \{(1,3),(2,3)\}, \\
  \{(1,3),(2,4)\}, \\
  \{(1,4),(2,3)\}, \\
  \{(1,4),(2,4)\}\phantom{,} \\
 }
$



\newpage

%  ____                                     __    __                   ____  
% / ___| _ __   __ _  ___ ___  ___    ___  / _|  / _|_   _ _ __  ___  |___ \ 
% \___ \| '_ \ / _` |/ __/ _ \/ __|  / _ \| |_  | |_| | | | '_ \/ __|   __) |
%  ___) | |_) | (_| | (_|  __/\__ \ | (_) |  _| |  _| |_| | | | \__ \  / __/ 
% |____/| .__/ \__,_|\___\___||___/  \___/|_|   |_|  \__,_|_| |_|___/ |_____|
%       |_|                                                                  
%
% «spaces-of-functions-2» (to ".spaces-of-functions-2")

{\bf Spaces of functions (2)}

Let: $A=\{1,2\}$, $B=\{3,4\}$, $C_1=\{5,6\}$, $C_2=\{7,8,9\}$.

If $f:A→B$ then $f$ takes each $a∈A$ to an element of $B$.

Let $g$ be a function that takes each $a∈A$ to an element of $C_\ColorRed{a}$.

\msk

This means that $g$ can be

$\{(1,5),(2,7)\}$ or

$\{(1,5),(2,8)\}$ or

$\{(1,5),(2,9)\}$ or

$\{(1,6),(2,7)\}$ or

$\{(1,6),(2,8)\}$ or

$\{(1,6),(2,9)\}$...

\msk

\def\setofsc#1#2{\{\,#1\;;\;#2\,\}}
\def\setofsc#1#2{\{\,#1;\;#2\,\}}

$f ∈ \setofsc{b_1∈B,   b_2∈B}  {\{(1,b_1),(2,b_2)\}} = Πa{:}A.B = (A→A)$

$g ∈ \setofsc{c_1∈C_1, c_2∈C_2}{\{(1,c_1),(2,c_2)\}} = Πa{:}A.C_a$

\newpage

%  ____                                     __    __                   _____ 
% / ___| _ __   __ _  ___ ___  ___    ___  / _|  / _|_   _ _ __  ___  |___ / 
% \___ \| '_ \ / _` |/ __/ _ \/ __|  / _ \| |_  | |_| | | | '_ \/ __|   |_ \ 
%  ___) | |_) | (_| | (_|  __/\__ \ | (_) |  _| |  _| |_| | | | \__ \  ___) |
% |____/| .__/ \__,_|\___\___||___/  \___/|_|   |_|  \__,_|_| |_|___/ |____/ 
%       |_|                                                                  
%
% «spaces-of-functions-3» (to ".spaces-of-functions-3")

{\bf Spaces of functions (3)}

From last page:

$f ∈ \setofsc{b_1∈B,   b_2∈B}  {\{(1,b_1),(2,b_2)\}} = Πa{:}A.B = (A→B)$

$g ∈ \setofsc{c_1∈C_1, c_2∈C_2}{\{(1,c_1),(2,c_2)\}} = Πa{:}A.C_a$

\msk

Compare:

$\setofsc{b_1∈B,   b_2∈B}  {\{(1,b_1),(2,b_2)\}} = Πa{:}\{1,2\}.B$

$\setofsc{c_1∈C_1, c_2∈C_2}{\{(1,c_1),(2,c_2)\}} = Πa{:}\{1,2\}.C_a$

$\setofsc{b_1∈B,   b_2∈B}  {    (b_1,    b_2)  } = B×B$

$\setofsc{c_1∈C_1, c_2∈C_2}{    (c_1,    c_2)  } = C_1×C_2$

\msk

$Πi{:}\{7,42,99,200\}.D_i$ is similar to

$D_7 × D_{42} × D_{99} × D_{200}$, but

the first returns \ColorRed{functions} and

the second return \ColorRed{4-uples}.

\newpage

%  ____                            _            _                         _     
% |  _ \  ___ _ __   ___ _ __   __| | ___ _ __ | |_   _ __  _ __ ___   __| |___ 
% | | | |/ _ \ '_ \ / _ \ '_ \ / _` |/ _ \ '_ \| __| | '_ \| '__/ _ \ / _` / __|
% | |_| |  __/ |_) |  __/ | | | (_| |  __/ | | | |_  | |_) | | | (_) | (_| \__ \
% |____/ \___| .__/ \___|_| |_|\__,_|\___|_| |_|\__| | .__/|_|  \___/ \__,_|___/
%            |_|                                     |_|                        
%
% «dependent-products» (to ".dependent-products")
% (ntyp 88 "dependent-products")
% (nty     "dependent-products")

{\bf Spaces of functions (4): dependent products}

$Πi{:}\{7,42,99,200\}.D_i$ is similar to

$D_7 × D_{42} × D_{99} × D_{200}$, but

the first returns \ColorRed{functions} and

the second return \ColorRed{4-uples}.

\msk

Terminology (half-weird):

$Πa{:}A.C_a$ and $Πi{:}I.D_i$ are \ColorRed{dependent products}.

Some type systems \ColorRed{define} $(A→B) = B^A := Πa{:}A.B$.

\msk

Dependent products generaliize \ColorRed{exponentials}!!! Yuck!!!!


\newpage



%  ____ _____ ____      
% |  _ \_   _/ ___| ___ 
% | |_) || | \___ \/ __|
% |  __/ | |  ___) \__ \
% |_|    |_| |____/|___/
%                       
% «pure-type-systems» (to ".pure-type-systems")
% (ntyp 89 "pure-type-systems")
% (nty     "pure-type-systems")

{\bf Pure Type Systems: first rules}

Kamareddine/Laan/Nederperlt (2004), p.117:

% (find-books "__logic/__logic.el" "typetheory")
% (find-mpottpage (+ 12 112) "4b Lambda calculus")
% (find-mpottpage (+ 12 116) "4c Pure Type Systems")
% (find-mpottpage (+ 12 118) "4c1 The Barendregt cube")
% (find-mpottpage (+ 12 121) "4c2 Metaproperties of PTSs")


%:  (fooi-t ":" "⠆")
%:
%:    \mathstrut              \mathstrut
%:    --------ax              --------a
%:    ⊢s_1⠆s_2                ⊢s_1⠆s_2                
%:                                                    
%:    ^ax                     ^ax-my                     
%:
%:       Γ⊢A⠆s                   Γ⊢A⠆s                
%:    ---------start          ---------v_s
%:    Γ,x⠆A⊢x⠆A               Γ,x⠆A⊢x⠆A               
%:                                                    
%:    ^start                  ^start-my              
%:
%:    Γ⊢A⠆B  Γ⊢C⠆s            Γ⊢A⠆B  Γ⊢C⠆s       
%:    ------------weak        ------------w_s
%:     Γ,x⠆C⊢A⠆B               Γ,x⠆C⊢A⠆B         
%:                                               
%:     ^weak                   ^weak-my
%:
%:
%:    Γ⊢A⠆s_1  Γ,x⠆A⊢B⠆s_2     Γ⊢A⠆s_1  Γ,x⠆A⊢B⠆s_2             
%:    --------------------Π    --------------------Π_{s_1s_2s_3}
%:       Γ⊢(Πx⠆A.B)⠆s_3           Γ⊢(Πx⠆A.B)⠆s_3                
%:                                                              
%:       ^Pi                      ^Pi-my
%:
%:    Γ,a⠆A⊢b⠆B   Γ⊢(Πa⠆A.B)⠆s
%:    ------------------------λ
%:    Γ⊢(λa⠆A.b)⠆(Πa⠆A.B)
%:    
%:    ^lambda
%:
\pu
\resizebox{!}{60pt}{%
$\begin{array}{cl}
  \cded{ax}     & (s_1,s_2)∈𝐛A \\[10pt]
  \cded{start}  & \\[10pt]
  \cded{weak}   & \\[10pt]
  \cded{Pi}     & (s_1,s_2,s_3)∈𝐛R \\[10pt]
  \cded{lambda} & \\
  \end{array}
$}

\msk

Specification: $(𝐛S,𝐛A,𝐛R)$ with $𝐛A⊆𝐛S^2$, $𝐛R⊆𝐛S^3$ 

For $λ1$: $𝐛S=\{*,□\}$, $𝐛A=\{(*,□)\}$, $𝐛R=\{(*,*,*)\}$

\newpage

%  ____ _____ ____        ____  
% |  _ \_   _/ ___| ___  |___ \ 
% | |_) || | \___ \/ __|   __) |
% |  __/ | |  ___) \__ \  / __/ 
% |_|    |_| |____/|___/ |_____|
%                               
% «pure-type-systems-2» (to ".pure-type-systems-2")

{\bf Pure Type Systems: first rules (2)}

We will change the notation slightly, to:

\resizebox{!}{60pt}{%
$\begin{array}{cl}
  \cded{ax-my}    & (s_1,s_2)∈𝐛A \\[10pt]
  \cded{start-my} & \\[10pt]
  \cded{weak-my}  & \\[10pt]
  \cded{Pi-my}    & (s_1,s_2,s_3)∈𝐛R \\[10pt]
  \cded{lambda}   & \\
  \end{array}
$}

\msk

Specification: $(𝐛S,𝐛A,𝐛R)$ with $𝐛A⊆𝐛S^2$, $𝐛R⊆𝐛S^3$ 

For $λ1$: $𝐛S=\{Θ,□\}$, $𝐛A=\{(Θ,□)\}$, $𝐛R=\{(Θ,Θ,Θ)\}$


\newpage

%  ____ _____ ____                    _ 
% |  _ \_   _/ ___| ___    _____  __ / |
% | |_) || | \___ \/ __|  / _ \ \/ / | |
% |  __/ | |  ___) \__ \ |  __/>  <  | |
% |_|    |_| |____/|___/  \___/_/\_\ |_|
%                                       
% «pts-derivation-1» (to ".pts-derivation-1")
% (ntyp 99 "pts-derivation-1")
% (nty     "pts-derivation-1")

{\bf Pure Type Systems: a derivation}

Derivations in a PTS have {\sl lots} of bureaucracy.

This is what we need to derive $A⠆Θ,B⠆Θ⊢(Πa⠆A.B)⠆Θ$:

\msk

%:  (fooi-t ":" "⠆")
%:
%:                                ----a  ----a      ----a      ----a  ----a
%:                                ⊢Θ⠆□   ⊢Θ⠆□       ⊢Θ⠆□       ⊢Θ⠆□   ⊢Θ⠆□ 
%:   ----a  ----a      ----a      -----------w    -------v     -----------w 
%:   ⊢Θ⠆□   ⊢Θ⠆□       ⊢Θ⠆□        A⠆Θ⊢Θ⠆□         A⠆Θ⊢A⠆Θ       A⠆Θ⊢Θ⠆□
%:   -----------w    -------v      -----------------------w    -----------v
%:    A⠆Θ⊢Θ⠆□         A⠆Θ⊢A⠆Θ            A⠆Θ,B⠆Θ⊢A⠆Θ           A⠆Θ,B⠆Θ⊢B⠆Θ
%:    -----------------------w           ---------------------------------w
%:          A⠆Θ,B⠆Θ⊢A⠆Θ                        A⠆Θ,B⠆Θ,a⠆A⊢B⠆Θ
%:              ----------------------------------------------Π_{ΘΘΘ}
%:              A⠆Θ,B⠆Θ⊢(Πa⠆A.B)⠆Θ
%:
%:              ^depprod1
%:
%:                                ----a  ----a      ----a      ----a  ----a
%:                                ⊢Θ⠆□   ⊢Θ⠆□       ⊢Θ⠆□       ⊢Θ⠆□   ⊢Θ⠆□ 
%:   ----a  ----a      ----a      -----------w_□   -------v_□   -----------w_□ 
%:   ⊢Θ⠆□   ⊢Θ⠆□       ⊢Θ⠆□        A⠆Θ⊢Θ⠆□         A⠆Θ⊢A⠆Θ       A⠆Θ⊢Θ⠆□
%:   -----------w_□   -------v_□   -----------------------w_□  -----------v_□
%:    A⠆Θ⊢Θ⠆□         A⠆Θ⊢A⠆Θ            A⠆Θ,B⠆Θ⊢A⠆Θ           A⠆Θ,B⠆Θ⊢B⠆Θ
%:    -----------------------w_□         ---------------------------------w_Θ
%:          A⠆Θ,B⠆Θ⊢A⠆Θ                        A⠆Θ,B⠆Θ,a⠆A⊢B⠆Θ
%:          --------------------------------------------------Π_{ΘΘΘ}
%:              A⠆Θ,B⠆Θ⊢(Πa⠆A.B)⠆Θ
%:
%:              ^depprod1
%:
%:
%:                                                  ----a      ----a  ----a
%:                                                  ⊢Θ⠆□       ⊢Θ⠆□   ⊢Θ⠆□ 
%:                                 =======        -------v_□   -----------w_□ 
%:                                 A⠆Θ⊢Θ⠆□         A⠆Θ⊢A⠆Θ       A⠆Θ⊢Θ⠆□
%:                                 -----------------------w_□  -----------v_□
%:                                       A⠆Θ,B⠆Θ⊢A⠆Θ           A⠆Θ,B⠆Θ⊢B⠆Θ
%:          ===========                  ---------------------------------w_Θ
%:          A⠆Θ,B⠆Θ⊢A⠆Θ                        A⠆Θ,B⠆Θ,a⠆A⊢B⠆Θ
%:          ---------------------------------------------------Π_{ΘΘΘ}
%:              A⠆Θ,B⠆Θ⊢(Πa⠆A.B)⠆Θ
%:
%:              ^depprod2
%:
\pu
\resizebox{1.0\textwidth}{!}{%
$\ded{depprod1}
$}

\msk

i.e.:

\resizebox{1.0\textwidth}{!}{%
$\ded{depprod2}
$}

\newpage

%  ____ _____ ____                ____  
% |  _ \_   _/ ___|    _____  __ |___ \ 
% | |_) || | \___ \   / _ \ \/ /   __) |
% |  __/ | |  ___) | |  __/>  <   / __/ 
% |_|    |_| |____/   \___/_/\_\ |_____|
%                                       
% «pts-derivation-2» (to ".pts-derivation-2")

{\bf Pure Type Systems: a derivation (2)}

This is what we need to derive $A⠆Θ⊢(λa⠆A.a)⠆(Πa⠆A.A)$:

\msk

%:                                                  
%:                                                  
%:                                          ----a
%:                                          ⊢Θ⠆□ 
%:                               =======   -------v_□
%:                               A⠆Θ⊢A⠆Θ   A⠆Θ⊢A⠆Θ
%:    =======         =======   -----------------w_Θ
%:    A⠆Θ⊢A⠆Θ         A⠆Θ⊢A⠆Θ     A⠆Θ,a⠆A⊢A⠆Θ
%:  -----------v_Θ    -----------------------Π_{ΘΘΘ}
%:  A⠆Θ,a⠆A⊢a⠆A            A⠆Θ⊢(Πa⠆A.A)⠆Θ
%:  -------------------------------------λ
%:        A⠆Θ⊢(λa⠆A.a)⠆(Πa⠆A.A)
%:
%:              ^depprod3
%:
\pu
\resizebox{1.0\textwidth}{!}{%
$\ded{depprod3}
$}


\newpage

%                      
% __   __  _   _   ___ 
% \ \ / / (_) (_) / __|
%  \ V /   _   _  \__ \
%   \_/   (_) (_) |___/
%                      
% «two-levels-below-a-sort» (to ".two-levels-below-a-sort")

{\bf Every variable is two levels below a sort}

We had $A⠆Θ⠆□$, $B⠆Θ⠆□$ \;\;---\;\; $A$ and $B$ are \ColorRed{sets},

and  $a⠆A⠆Θ$ \;\;---\;\; $a$ is an \ColorRed{element} of a set.

We had $(A{→}B) = (Πa⠆A.B)$, and $f⠆(Πa⠆A.B)⠆Θ$.

Convention on names of variables:

$A$, $B$ (uppercase) for \ColorRed{sets},
$a$, $b$, $f$ (lowercase) for \ColorRed{elements}.

The rules $v_□$ and $w_□$ introduce variables two levels below $□$.

the rules $v_Θ$ and $w_Θ$ introduce variables two levels below $Θ$.

\msk

\resizebox{1.0\textwidth}{!}{%
$\ded{depprod3}
$}


\newpage

%  __  __                                 _       
% |  \/  | ___  _ __ ___   ___  ___  _ __| |_ ___ 
% | |\/| |/ _ \| '__/ _ \ / __|/ _ \| '__| __/ __|
% | |  | | (_) | | |  __/ \__ \ (_) | |  | |_\__ \
% |_|  |_|\___/|_|  \___| |___/\___/|_|   \__|___/
%                                                 
% «more-sorts» (to ".more-sorts")
% (ntyp 63 "more-sorts")
% (nty     "more-sorts")

{\bf More sorts}

Some of the Pure Type Systems that we will see later will have

specifications like $(𝐛S,𝐛A,𝐛R) = (\{Ω,Θ,□\}, \, \{(Ω,□),(Θ,□)\}, \, ...)$.

Their axioms are $Ω⠆Θ$ and $Θ⠆□$ \;\;---\;\; i.e., they have $Ω⠆Θ⠆□$.

Their variables are of four kinds:

\msk

$\begin{array}{ccccccccc}
                & & \text{element}     &:& \text{set} &:& Θ &:& □ \\
 \text{witness} &:& \text{proposition} &:& Ω          &:& Θ \\
 \end{array}
$

\msk

I prefer to think on that as:

\msk

$\begin{array}{ccccccc}
                & & \text{element}     &:& \text{set} &:& Θ \\
 \text{witness} &:& \text{proposition} &:& Ω \\
 \end{array}
$

\msk

Convention on names of variables:

\msk

$\begin{array}{ccccccc}
     & & a,b,f &:& A,B &:& Θ \\
 p,q &:& P,Q   &:& Ω \\
 \end{array}
$

\newpage

%  ____   _  _____ 
% |  _ \ / \|_   _|
% | |_) / _ \ | |  
% |  __/ ___ \| |  
% |_| /_/   \_\_|  
%                  
% «PAT» (to ".PAT")
% (find-books "__logic/__logic.el" "altenkirch")
% (find-altenkirchnttpage  3   "type of its evidence")

{\bf PAT: Propositions As Types / Proofs As Terms}

See Kamareddine/Laan/Nederperlt (2004), chapter 4, for PAT,

Hermogenes Oliveira's PhD Thesis for the BHK interpretation.

The standard way to think of

\msk

$\begin{array}{ccccccc}
                & & \text{element}     &:& \text{set} &:& Θ \\
 \text{witness} &:& \text{proposition} &:& Ω \\
 \end{array}
$

\msk

is to interpret each proposition $P$ as the set of its proofs,

and a witness $p⠆P$ as an element of $P$; propositions that are

false have no proofs.


I believe that we develop intuition about PAT quicker if we start with
a \ColorRed{model} in which $Ω=\{𝐛F,𝐛T\}$, $𝐛F$ is an empty set, $𝐛T$
is a singleton set; each proposition is interpreted as its
truth-value, and all proofs/witnesses of a true proposition (i.e.,
elements of $𝐛T$!) are identified.


\newpage

{\bf $Θ$ in the naïve model}

[The most common error]

Lambda notation

Propositions and very small sets

\newpage




% (find-lshortpage (+ 14  2) "1.2 Basics")
% (find-lshortpage (+ 14  2) "1.2.1 Author, Book Designer, and Typesetter")
% (find-lshortpage (+ 14  2) "1.2.2 Layout Design")
% (find-lshortpage (+ 14  3) "1.2.3 Advantages and Disadvantages")



% https://en.wikipedia.org/wiki/Hindley%E2%80%93Milner_type_system



% (lodp)




% (find-LATEX "2002fmcs.tex")




\end{document}

% Local Variables:
% coding: utf-8-unix
% ee-tla: "nty"
% End:
