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