curryhoward-2020-short.lyx

#LyX 2.3 created this file. For more info see http://www.lyx.org/
\lyxformat 544
\begin_document
\begin_header
\save_transient_properties true
\origin unavailable
\textclass beamer
\begin_preamble
\usetheme[secheader]{Boadilla}
\usecolortheme{seahorse}
\title[Curry-Howard correspondence]{A brief tutorial on the Curry-Howard correspondence}
\subtitle{For programmers, with code examples in Scala}
\author{Sergei Winitzki}
\date{September 19, 2020}
\institute[ABTB]{Academy By the Bay}
\setbeamertemplate{headline}{} % disable headline at top
\setbeamertemplate{navigation symbols}{}

% Double-stroked fonts to replace the non-working \mathbb{1}.
\usepackage{bbold}
\DeclareMathAlphabet{\bbnumcustom}{U}{BOONDOX-ds}{m}{n} % Use BOONDOX-ds or bbold.
\newcommand{\custombb}[1]{\bbnumcustom{#1}}
% The LyX document will define a macro \bbnum{#1} that calls \custombb{#1}.

\usepackage{relsize} % make math symbols larger or smaller
\usepackage{stmaryrd} % some extra symbols such as \fatsemi
% Note: using \forwardcompose inside a \text{} will cause a LaTeX error!
\newcommand{\forwardcompose}{\hspace{1.5pt}\ensuremath\mathsmaller{\fatsemi}\hspace{1.5pt}}


% Make underline green.
\definecolor{greenunder}{rgb}{0.1,0.6,0.2}
%\newcommand{\munderline}[1]{{\color{greenunder}\underline{{\color{black}#1}}\color{black}}}
\def\mathunderline#1#2{\color{#1}\underline{{\color{black}#2}}\color{black}}
% The LyX document will define a macro \gunderline{#1} that will use \mathunderline with the color `greenunder`.
%\def\gunderline#1{\mathunderline{greenunder}{#1}} % This is now defined by LyX itself with GUI support.

% Scala syntax highlighting. See https://tex.stackexchange.com/questions/202479/unable-to-define-scala-language-with-listings
%\usepackage[T1]{fontenc}
%\usepackage[utf8]{inputenc}
%\usepackage{beramono}
%\usepackage{listings}
% The listing settings are now supported by LyX in a separate section "Listings".
\usepackage{xcolor}

\definecolor{scalakeyword}{rgb}{0.16,0.07,0.5}
\definecolor{dkgreen}{rgb}{0,0.6,0}
\definecolor{gray}{rgb}{0.5,0.5,0.5}
\definecolor{mauve}{rgb}{0.58,0,0.82}
\definecolor{aqua}{rgb}{0.9,0.96,0.999}
\definecolor{scalatype}{rgb}{0.2,0.3,0.2}
\end_preamble
\use_default_options true
\maintain_unincluded_children false
\language english
\language_package default
\inputencoding auto
\fontencoding global
\font_roman "default" "default"
\font_sans "default" "default"
\font_typewriter "default" "default"
\font_math "auto" "auto"
\font_default_family default
\use_non_tex_fonts false
\font_sc false
\font_osf false
\font_sf_scale 100 100
\font_tt_scale 100 100
\use_microtype false
\use_dash_ligatures true
\graphics default
\default_output_format default
\output_sync 0
\bibtex_command default
\index_command default
\paperfontsize default
\spacing single
\use_hyperref true
\pdf_bookmarks true
\pdf_bookmarksnumbered false
\pdf_bookmarksopen false
\pdf_bookmarksopenlevel 1
\pdf_breaklinks false
\pdf_pdfborder false
\pdf_colorlinks true
\pdf_backref false
\pdf_pdfusetitle true
\papersize default
\use_geometry true
\use_package amsmath 1
\use_package amssymb 1
\use_package cancel 1
\use_package esint 1
\use_package mathdots 1
\use_package mathtools 1
\use_package mhchem 1
\use_package stackrel 1
\use_package stmaryrd 1
\use_package undertilde 1
\cite_engine basic
\cite_engine_type default
\biblio_style plain
\use_bibtopic false
\use_indices false
\paperorientation portrait
\suppress_date false
\justification true
\use_refstyle 1
\use_minted 0
\index Index
\shortcut idx
\color #008000
\end_index
\secnumdepth 3
\tocdepth 3
\paragraph_separation indent
\paragraph_indentation default
\is_math_indent 0
\math_numbering_side default
\quotes_style english
\dynamic_quotes 0
\papercolumns 1
\papersides 1
\paperpagestyle default
\tracking_changes false
\output_changes false
\html_math_output 0
\html_css_as_file 0
\html_be_strict false
\end_header

\begin_body

\begin_layout Standard
\begin_inset ERT
status open

\begin_layout Plain Layout


\backslash
frame{
\backslash
titlepage}
\end_layout

\end_inset


\begin_inset FormulaMacro
\newcommand{\gunderline}[1]{\mathunderline{greenunder}{#1}}
{\underline{#1}}
\end_inset


\begin_inset FormulaMacro
\newcommand{\bef}{\forwardcompose}
{\fatsemi}
\end_inset


\begin_inset FormulaMacro
\newcommand{\bbnum}[1]{\custombb{#1}}
{\underline{#1}}
\end_inset


\end_layout

\begin_layout Frame
\begin_inset Argument 4
status open

\begin_layout Plain Layout
What problems does Curry-Howard correspondence solve?
\end_layout

\end_inset


\begin_inset Separator latexpar
\end_inset


\end_layout

\begin_deeper
\begin_layout Standard
The CH correspondence is a theory that answers these questions:
\end_layout

\begin_layout Enumerate
Can a program compute a value of type 
\begin_inset Formula $X$
\end_inset

 given values of some types 
\begin_inset Formula $A$
\end_inset

, 
\begin_inset Formula $B$
\end_inset

, 
\begin_inset Formula $C$
\end_inset

, ...? Example:
\begin_inset VSpace -80baselineskip%
\end_inset


\end_layout

\begin_layout LyX-Code

\family typewriter
\size footnotesize
\color blue
def f[A, B, C](x: A => Option[B], y: Either[A, C], z: C => B): B = {
\end_layout

\begin_layout LyX-Code

\family typewriter
\size footnotesize
\color blue
   val t: Either[B, C] = ???
\family default
\color darkgray
 // Can we implement `t` here?
\end_layout

\begin_layout LyX-Code

\family typewriter
\size footnotesize
\color blue
   t.map(z).merge
\end_layout

\begin_layout LyX-Code

\family typewriter
\size footnotesize
\color blue
}
\end_layout

\begin_layout Enumerate
\begin_inset ERT
status open

\begin_layout Plain Layout

[]
\backslash
addtocounter{enumi}{1}
\backslash
vspace*{-0.5cm}
\end_layout

\end_inset


\end_layout

\begin_layout Enumerate
Can we infer the code of a function from its type signature?
\begin_inset Newline newline
\end_inset

Examples:
\begin_inset VSpace -80baselineskip%
\end_inset


\end_layout

\begin_layout LyX-Code

\family typewriter
\size footnotesize
\color blue
def f[A, B, C]: (A => Either[B, C]) => Either[A, C] => Either[B, C]
\end_layout

\begin_layout LyX-Code

\family typewriter
\size footnotesize
\color blue
def g[A, B, C]: (A => Either[B, C]) => Either[A => B, A => C]
\end_layout

\begin_layout LyX-Code

\family typewriter
\size footnotesize
\color blue
def h[A, B]: ((((A => B) => A) => A) => B) => B
\end_layout

\begin_layout Standard
Theory gives an algorithm for writing code 
\begin_inset Quotes eld
\end_inset

guided by the types
\begin_inset Quotes erd
\end_inset


\end_layout

\begin_layout Itemize
The 
\begin_inset CommandInset href
LatexCommand href
name "curryhoward"
target "https://github.com/Chymyst/curryhoward"
literal "false"

\end_inset

 library generates Scala code from type signatures
\end_layout

\begin_deeper
\begin_layout Itemize
Often, there is only one 
\begin_inset Quotes eld
\end_inset

useful
\begin_inset Quotes erd
\end_inset

 implementation out of many
\end_layout

\begin_deeper
\begin_layout Itemize
The 
\family typewriter
\size footnotesize
\color blue
curryhoward
\family default
\size default
\color inherit
 library tries to find that implementation
\end_layout

\end_deeper
\end_deeper
\begin_layout LyX-Code

\family typewriter
\size footnotesize
\color blue
def h[A, B]: ((((A => B) => A) => A) => B) => B  =  implement
\end_layout

\end_deeper
\begin_layout Standard
\begin_inset Separator parbreak
\end_inset


\end_layout

\begin_layout Frame
\begin_inset Argument 4
status open

\begin_layout Plain Layout
From types to logical propositions I.
 
\begin_inset Formula $\mathcal{CH}$
\end_inset

-propositions
\end_layout

\end_inset


\begin_inset Separator latexpar
\end_inset


\end_layout

\begin_deeper
\begin_layout Itemize
How to 
\emph on
prove
\emph default
 that this function is not implementable?
\begin_inset VSpace -80baselineskip%
\end_inset


\end_layout

\begin_layout LyX-Code

\family typewriter
\size footnotesize
\color blue
def bad[A, B, C](x: A => Option[B], y: Either[A, C], z: C => B): B
\end_layout

\begin_layout Standard
The idea is to build a system of logical derivation rules and axioms (a
 
\series bold
logic
\series default
)
\end_layout

\begin_layout Standard
The logic should be able to prove rigorously whether any code expression
 in the body of the function 
\family typewriter
\size footnotesize
\color blue
bad
\family default
\size default
\color inherit
 can compute values of type 
\family typewriter
\size footnotesize
\color blue
B
\family default
\size default
\color inherit
 
\end_layout

\begin_layout Itemize
Denote such 
\emph on
propositions
\emph default
 by 
\begin_inset Formula ${\cal CH}(B)$
\end_inset

 – 
\begin_inset Quotes eld
\end_inset


\begin_inset Formula $\mathcal{C}$
\end_inset

ode 
\begin_inset Formula $\mathcal{H}$
\end_inset

as a value of type 
\family typewriter
\size footnotesize
\color blue
B
\family default
\size default
\color inherit

\begin_inset Quotes erd
\end_inset


\end_layout

\begin_layout Standard
How to obtain rules for reasoning about 
\begin_inset Formula $\mathcal{CH}$
\end_inset

-propositions?
\end_layout

\begin_layout Itemize
The code of 
\family typewriter
\size footnotesize
\color blue
bad
\family default
\size default
\color inherit
 might contain expressions such as 
\family typewriter
\size footnotesize
\color blue
y.map(z)
\family default
\size default
\color inherit
 
\end_layout

\begin_deeper
\begin_layout Itemize
This computes a value of type 
\family typewriter
\size footnotesize
\color blue
Either[A, B]
\family default
\size default
\color inherit
 from values of types 
\family typewriter
\size footnotesize
\color blue
Either[A, C]
\family default
\size default
\color inherit
 and 
\family typewriter
\size footnotesize
\color blue
(C => B)
\end_layout

\end_deeper
\begin_layout Itemize
Code expressions create
\begin_inset ERT
status open

\begin_layout Plain Layout


\backslash
,
\end_layout

\end_inset


\emph on
logical relationships
\emph default
 between 
\begin_inset Formula $\mathcal{CH}$
\end_inset

-propositions
\end_layout

\begin_deeper
\begin_layout Itemize
\begin_inset Quotes eld
\end_inset

Logical relationship
\begin_inset Quotes erd
\end_inset

: 
\begin_inset Formula $X$
\end_inset

 can be proved true if 
\begin_inset Formula $A$
\end_inset

, 
\begin_inset Formula $B$
\end_inset

, 
\begin_inset Formula $C$
\end_inset

 are true
\end_layout

\begin_layout Itemize
In logic, such a proof task is represented by a 
\series bold
sequent
\end_layout

\begin_deeper
\begin_layout Itemize
Notation: 
\begin_inset Formula $A,B,C\vdash X$
\end_inset

; the 
\series bold
premises
\series default
 are 
\begin_inset Formula $A,B,C$
\end_inset

 and the 
\series bold
goal
\series default
 is 
\begin_inset Formula $X$
\end_inset


\end_layout

\end_deeper
\begin_layout Itemize
Proofs are achieved via axioms and derivation rules
\end_layout

\begin_deeper
\begin_layout Itemize
Axioms: sequents that are true without proof
\end_layout

\begin_layout Itemize
Derivation rules: prove a sequent given proofs of some other sequent(s)
\end_layout

\end_deeper
\end_deeper
\end_deeper
\begin_layout Standard
\begin_inset Separator parbreak
\end_inset


\end_layout

\begin_layout Frame
\begin_inset Argument 4
status open

\begin_layout Plain Layout
From types to logical propositions II.
 Fully parametric code
\end_layout

\end_inset


\begin_inset Separator latexpar
\end_inset


\end_layout

\begin_deeper
\begin_layout Standard
\begin_inset ERT
status open

\begin_layout Plain Layout


\backslash
vspace{-0.1cm}
\end_layout

\end_inset

To determine the logical relationships between types, we need to know 
\emph on
all possible code snippets
\end_layout

\begin_layout Standard
\begin_inset Quotes eld
\end_inset

Fully parametric
\begin_inset Quotes erd
\end_inset

 code allows only combinations of these snippets:
\end_layout

\begin_layout Itemize
Use an existing value 
\family typewriter
\size footnotesize
\color blue
x
\family default
\size default
\color inherit
 of type 
\family typewriter
\size footnotesize
\color blue
A
\family default
\size default
\color inherit
.
 Scala code: 
\family typewriter
\size footnotesize
\color blue
val y:
\begin_inset space ~
\end_inset

A = x
\end_layout

\begin_layout Itemize
Tuple type: 
\family typewriter
\size footnotesize
\color blue
(A, B)
\end_layout

\begin_deeper
\begin_layout Itemize
Create: 
\family typewriter
\size footnotesize
\color blue
val pair:
\begin_inset space \space{}
\end_inset

(A, B) = (a, b)
\family default
\size default
\color inherit
 
\end_layout

\begin_layout Itemize
Use: 
\family typewriter
\size footnotesize
\color blue
val y:
\begin_inset space \space{}
\end_inset

B = pair._2
\end_layout

\end_deeper
\begin_layout Itemize
Function type: 
\family typewriter
\size footnotesize
\color blue
A => B
\end_layout

\begin_deeper
\begin_layout Itemize
Create: 
\family typewriter
\size footnotesize
\color blue
def f:
\begin_inset space \space{}
\end_inset

(A => B) = { x: A => ...
 /*
\family default
\size default
\color inherit
(may use 
\family typewriter
\size footnotesize
\color blue
x
\family default
\size default
\color inherit
 here)
\family typewriter
\size footnotesize
\color blue
*/ }
\family default
\size default
\color inherit
 
\end_layout

\begin_layout Itemize
Use: 
\family typewriter
\size footnotesize
\color blue
val y:
\begin_inset space \space{}
\end_inset

B = f(a)
\end_layout

\end_deeper
\begin_layout Itemize
Disjunctive type: 
\family typewriter
\size footnotesize
\color blue
Either[A, B]
\family default
\size default
\color inherit
 
\end_layout

\begin_deeper
\begin_layout Itemize
Create:
\begin_inset Newline newline
\end_inset

 
\family typewriter
\size footnotesize
\color blue

\begin_inset space \space{}
\end_inset

val x:
\begin_inset space \space{}
\end_inset

Either[A, B] = Left(a); val y:
\begin_inset space \space{}
\end_inset

Either[A, B] = Right(b)
\end_layout

\begin_layout Itemize
Use: 
\family typewriter
\size footnotesize
\color blue
val z:
\begin_inset space \space{}
\end_inset

C = x match {
\begin_inset Newline newline
\end_inset

 case Left(a) => ...
\begin_inset Newline newline
\end_inset

 case Right(b) => ...
\begin_inset Newline newline
\end_inset

}
\end_layout

\end_deeper
\begin_layout Itemize
Unit type: 
\family typewriter
\size footnotesize
\color blue
Unit
\end_layout

\begin_deeper
\begin_layout Itemize
Create: 
\family typewriter
\size footnotesize
\color blue
val x:
\begin_inset space \space{}
\end_inset

Unit = ()
\end_layout

\end_deeper
\end_deeper
\begin_layout Standard
\begin_inset Separator parbreak
\end_inset


\end_layout

\begin_layout Frame
\begin_inset Argument 4
status open

\begin_layout Plain Layout
From types to logical propositions III.
 Sequents
\end_layout

\end_inset


\begin_inset Separator latexpar
\end_inset


\end_layout

\begin_deeper
\begin_layout Itemize
Sequents correspond to code fragments that have specified types
\end_layout

\begin_layout Itemize
A sequent 
\begin_inset Formula $\mathcal{CH}(X),\mathcal{CH}(Y)\vdash\mathcal{CH}(Z)$
\end_inset

 corresponds to an 
\emph on
expression
\emph default
 of type 
\family typewriter
\size footnotesize
\color blue
Z
\family default
\size default
\color inherit
 that uses some previously defined values 
\family typewriter
\size footnotesize
\color blue
x:X
\family default
\size default
\color inherit
 and 
\family typewriter
\size footnotesize
\color blue
y:Y
\family default
\size default
\color inherit
 
\end_layout

\begin_deeper
\begin_layout Itemize
Sequents only describe the 
\emph on
types
\emph default
 of expressions and their parts
\end_layout

\end_deeper
\begin_layout Itemize
Each allowed code snippet means that we can compute a value of some type
 given value(s) of other type(s)
\end_layout

\begin_layout Standard
Express this in sequent notation as 
\series bold
derivation rules
\series default
:
\end_layout

\begin_layout Itemize
Use an existing value:
\size small
 
\begin_inset Formula $\mathcal{CH}(A)\vdash\mathcal{CH}(A)$
\end_inset


\end_layout

\begin_layout Itemize
Create tuple:
\size small
 
\begin_inset Formula $\mathcal{CH}(A),\mathcal{CH}(B)\vdash\mathcal{CH}($
\end_inset


\family typewriter
\color blue
Tuple2(A,B)
\family default
\color inherit

\begin_inset Formula $)$
\end_inset


\end_layout

\begin_layout Itemize
Use tuple: 
\size small

\begin_inset Formula $\mathcal{CH}($
\end_inset


\family typewriter
\color blue
Tuple2(A,B)
\family default
\color inherit

\begin_inset Formula $)\vdash\mathcal{CH}(A)$
\end_inset


\size default
 and 
\size small

\begin_inset Formula $\mathcal{CH}($
\end_inset


\family typewriter
\color blue
Tuple2(A,B)
\family default
\color inherit

\begin_inset Formula $)\vdash\mathcal{CH}(B)$
\end_inset

 
\end_layout

\begin_layout Itemize
Create function:
\size small
 
\begin_inset Formula $\emptyset\vdash\mathcal{CH}($
\end_inset


\family typewriter
\color blue
A => B
\family default
\color inherit

\begin_inset Formula $)$
\end_inset


\size default
 if given 
\size small

\begin_inset Formula $\mathcal{CH}(A)\vdash\mathcal{CH}(B)$
\end_inset


\family typewriter
\color blue
 
\end_layout

\begin_deeper
\begin_layout Itemize
Function body is an expression of type 
\family typewriter
\size footnotesize
\color blue
B
\family default
\size default
\color inherit
 that uses 
\family typewriter
\size footnotesize
\color blue
x
\family default
\size default
\color inherit
 of type 
\family typewriter
\size footnotesize
\color blue
A
\end_layout

\end_deeper
\begin_layout Itemize
Use function:
\size small
 
\begin_inset Formula $\mathcal{CH}($
\end_inset


\family typewriter
\color blue
A => B
\family default
\color inherit

\begin_inset Formula $),\mathcal{CH}(A)\vdash\mathcal{CH}(B)$
\end_inset


\end_layout

\begin_layout Itemize
Create disjunctive value:
\size small
 
\begin_inset Formula $\mathcal{CH}(A)\vdash\mathcal{CH}($
\end_inset


\family typewriter
\color blue
Either[A, B]
\family default
\color inherit

\begin_inset Formula $)$
\end_inset


\size default
 and
\size small
 
\begin_inset Formula $\mathcal{CH}(B)\vdash\mathcal{CH}($
\end_inset


\family typewriter
\color blue
Either[A, B]
\family default
\color inherit

\begin_inset Formula $)$
\end_inset


\end_layout

\begin_layout Itemize
Use disjunctive value:
\begin_inset Newline newline
\end_inset


\begin_inset space ~
\end_inset

 
\begin_inset space ~
\end_inset


\size small
 
\begin_inset Formula $\mathcal{CH}($
\end_inset


\family typewriter
\color blue
A => C
\family default
\color inherit

\begin_inset Formula $),\mathcal{CH}($
\end_inset


\family typewriter
\color blue
B => C
\family default
\color inherit

\begin_inset Formula $),\mathcal{CH}($
\end_inset


\family typewriter
\color blue
Either[A, B]
\family default
\color inherit

\begin_inset Formula $)\vdash\mathcal{CH}(C)$
\end_inset


\end_layout

\begin_layout Itemize
Create unit value: 
\size small

\begin_inset Formula $\emptyset\vdash\mathcal{CH}($
\end_inset


\family typewriter
\color blue
Unit
\family default
\color inherit

\begin_inset Formula $)$
\end_inset


\end_layout

\end_deeper
\begin_layout Standard
\begin_inset Separator parbreak
\end_inset


\end_layout

\begin_layout Frame
\begin_inset Argument 4
status open

\begin_layout Plain Layout
Translating language constructions into the logic I
\end_layout

\end_inset


\begin_inset Separator latexpar
\end_inset


\end_layout

\begin_deeper
\begin_layout Itemize
If there are no other allowed code snippets, we can summarize the correspondence
 between type constructors and propositions:
\end_layout

\begin_layout Standard
\align center
\begin_inset Tabular
<lyxtabular version="3" rows="7" columns="3">
<features tabularvalignment="middle">
<column alignment="center" valignment="top">
<column alignment="center" valignment="top">
<column alignment="center" valignment="top">
<row>
<cell alignment="center" valignment="top" topline="true" bottomline="true" leftline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\series bold
Scala type
\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" bottomline="true" leftline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\series bold
Proposition in logic
\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" bottomline="true" leftline="true" rightline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\series bold
Short type notation
\end_layout

\end_inset
</cell>
</row>
<row>
<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\family typewriter
\size footnotesize
\color blue
A
\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout
\begin_inset Formula ${\cal CH}(A)$
\end_inset


\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" leftline="true" rightline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout
\begin_inset Formula $A$
\end_inset


\end_layout

\end_inset
</cell>
</row>
<row>
<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\family typewriter
\size footnotesize
\color blue
(A, B)
\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout
\begin_inset Formula ${\cal CH}(A)\wedge\mathcal{CH}(B)$
\end_inset


\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" leftline="true" rightline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout
\begin_inset Formula $A\times B$
\end_inset


\end_layout

\end_inset
</cell>
</row>
<row>
<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\family typewriter
\size footnotesize
\color blue
Either[A, B]
\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout
\begin_inset Formula ${\cal CH}(A)\vee\mathcal{CH}(B)$
\end_inset


\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" leftline="true" rightline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout
\begin_inset Formula $A+B$
\end_inset


\end_layout

\end_inset
</cell>
</row>
<row>
<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\family typewriter
\size footnotesize
\color blue
A => B
\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout
\begin_inset Formula ${\cal CH}(A)\Rightarrow\mathcal{CH}(B)$
\end_inset


\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" leftline="true" rightline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout
\begin_inset Formula $A\rightarrow B$
\end_inset


\end_layout

\end_inset
</cell>
</row>
<row>
<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\family typewriter
\size footnotesize
\color blue
()
\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\emph on
True
\emph default
 ; 
\emph on

\begin_inset Formula $\top$
\end_inset


\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" leftline="true" rightline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout
\begin_inset Formula $\bbnum 1$
\end_inset


\end_layout

\end_inset
</cell>
</row>
<row>
<cell alignment="center" valignment="top" topline="true" bottomline="true" leftline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\family typewriter
\size footnotesize
\color blue
Nothing
\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" bottomline="true" leftline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\emph on
False
\emph default
 ; 
\emph on

\begin_inset Formula $\bot$
\end_inset


\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" bottomline="true" leftline="true" rightline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout
\begin_inset Formula $\bbnum 0$
\end_inset


\end_layout

\end_inset
</cell>
</row>
</lyxtabular>

\end_inset


\end_layout

\begin_layout Standard
We can now translate types into logic formulas and back
\end_layout

\begin_layout Itemize
Example: 
\family typewriter
\size footnotesize
\color blue
def duplicate[A]: A => (A, A)
\end_layout

\begin_deeper
\begin_layout Itemize
The type of this function in the short type notation is 
\begin_inset Formula $A\rightarrow A\times A$
\end_inset


\end_layout

\begin_layout Itemize
This corresponds to the logical formula 
\begin_inset Formula $\forall A.~\mathcal{CH}(A)\Rightarrow\mathcal{CH}(A)\wedge\mathcal{CH}(A)$
\end_inset


\end_layout

\end_deeper
\begin_layout Itemize
The question about the function 
\family typewriter
\size footnotesize
\color blue
bad
\family default
\size default
\color inherit
 is written in logic as this sequent:
\size small

\begin_inset Formula 
\[
{\cal CH}(A\rightarrow\bbnum 1+B),{\cal CH}(A+C),{\cal CH}(C\rightarrow B)\vdash{\cal CH}(B)
\]

\end_inset


\end_layout

\end_deeper
\begin_layout Standard
\begin_inset Separator parbreak
\end_inset


\end_layout

\begin_layout Frame
\begin_inset Argument 4
status open

\begin_layout Plain Layout
Translating language constructions into the logic II
\end_layout

\end_inset


\begin_inset Separator latexpar
\end_inset


\end_layout

\begin_deeper
\begin_layout FrameSubtitle
What are the axioms and the derivation rules in the logic of types?
\end_layout

\begin_layout Standard
\begin_inset VSpace -40baselineskip%
\end_inset

The set of 
\emph on
all well-typed fully parametric programs
\emph default
 
\begin_inset Formula $\cong$
\end_inset

 the set of 
\emph on
all valid derivations in the logic of types
\end_layout

\begin_layout Itemize
Write just 
\begin_inset Formula $A$
\end_inset

 instead of 
\begin_inset Formula $\mathcal{CH}(A)$
\end_inset

 and use short type notation
\end_layout

\begin_layout Itemize
Axioms:
\end_layout

\begin_deeper
\begin_layout Itemize
\begin_inset Formula $\emptyset\vdash\top$
\end_inset

 – create the value of unit type
\end_layout

\begin_layout Itemize
\begin_inset Formula $A\vdash A$
\end_inset

 – use variable
\end_layout

\begin_layout Itemize
\begin_inset Formula $A,B\vdash(A\times B)$
\end_inset

 – create tuple
\end_layout

\begin_layout Itemize
\begin_inset Formula $(A\times B)\vdash A$
\end_inset

 – use left part of tuple
\end_layout

\begin_layout Itemize
\begin_inset Formula $(A\times B)\vdash B$
\end_inset

 – use right part of tuple
\end_layout

\begin_layout Itemize
\begin_inset Formula $A,(A\rightarrow B)\vdash B$
\end_inset

 – apply function to argument
\end_layout

\begin_layout Itemize
\begin_inset Formula $A\vdash(A+B)$
\end_inset

 – create left part of 
\family typewriter
\size footnotesize
\color blue
Either
\end_layout

\begin_layout Itemize
\begin_inset Formula $B\vdash(A+B)$
\end_inset

 – create right part of 
\family typewriter
\size footnotesize
\color blue
Either
\end_layout

\begin_layout Itemize
\begin_inset Formula $(A+B),(A\rightarrow C),(B\rightarrow C)\vdash C$
\end_inset

 – use 
\family typewriter
\size footnotesize
\color blue
Either
\family default
\size default
\color inherit
 via match/case
\end_layout

\end_deeper
\begin_layout Itemize
Derivation rules:
\end_layout

\begin_deeper
\begin_layout Itemize
\begin_inset Quotes eld
\end_inset

create function
\begin_inset Quotes erd
\end_inset

: we can prove 
\begin_inset Formula $\emptyset\vdash(A\rightarrow B)$
\end_inset

 given 
\begin_inset Formula $A\vdash B$
\end_inset


\end_layout

\begin_layout Itemize
\begin_inset Quotes eld
\end_inset

add premise
\begin_inset Quotes erd
\end_inset

: we can prove 
\begin_inset Formula $A,...,C,D\vdash G$
\end_inset

 given 
\begin_inset Formula $A,...,C\vdash G$
\end_inset

 
\end_layout

\begin_layout Itemize
\begin_inset Quotes eld
\end_inset

reorder
\begin_inset Quotes erd
\end_inset

: we can prove 
\begin_inset Formula $B,A,C,...\vdash G$
\end_inset

 given 
\begin_inset Formula $A,B,C,...\vdash G$
\end_inset

 
\end_layout

\end_deeper
\end_deeper
\begin_layout Standard
\begin_inset Separator parbreak
\end_inset


\end_layout

\begin_layout Frame
\begin_inset Argument 4
status open

\begin_layout Plain Layout
The logic of types I
\end_layout

\end_inset


\begin_inset Separator latexpar
\end_inset


\end_layout

\begin_deeper
\begin_layout Standard
Now we have all the axioms and the derivation rules of the logic of types.
\end_layout

\begin_layout Itemize
What theorems can we derive in this logic?
\end_layout

\begin_layout Itemize
Example theorem: 
\begin_inset Formula $\forall A.~\forall B.~A\rightarrow B\rightarrow A$
\end_inset

 or 
\begin_inset Formula $\emptyset\vdash A\rightarrow B\rightarrow A$
\end_inset


\end_layout

\begin_deeper
\begin_layout Itemize
Start with an axiom 
\begin_inset Formula $A\vdash A$
\end_inset

; add an unused premise 
\begin_inset Formula $B$
\end_inset

, get 
\begin_inset Formula $A,B\vdash A$
\end_inset


\end_layout

\begin_layout Itemize
Use the 
\begin_inset Quotes eld
\end_inset

create function
\begin_inset Quotes erd
\end_inset

 rule with 
\begin_inset Formula $B$
\end_inset

 and 
\begin_inset Formula $A$
\end_inset

, get 
\begin_inset Formula $A\vdash B\rightarrow A$
\end_inset


\end_layout

\begin_layout Itemize
Use the 
\begin_inset Quotes eld
\end_inset

create function
\begin_inset Quotes erd
\end_inset

 rule with 
\begin_inset Formula $A$
\end_inset

 and 
\begin_inset Formula $B\rightarrow A$
\end_inset

, get the final sequent 
\begin_inset Formula $\emptyset\vdash A\rightarrow B\rightarrow A$
\end_inset

 showing that 
\begin_inset Formula $\forall A.~\forall B.~A\rightarrow B\rightarrow A$
\end_inset

 is a 
\series bold
theorem
\series default
 since 
\begin_inset Formula $\emptyset\vdash A\rightarrow B\rightarrow A$
\end_inset

 was derived from no premises for all 
\begin_inset Formula $A$
\end_inset

 and 
\begin_inset Formula $B$
\end_inset


\end_layout

\end_deeper
\begin_layout Itemize
What code does this describe?
\end_layout

\begin_deeper
\begin_layout Itemize
The axiom 
\begin_inset Formula $A\vdash A$
\end_inset

 represents the expression 
\family typewriter
\size footnotesize
\color blue
x:
\begin_inset space ~
\end_inset

A
\family default
\size default
\color inherit
 
\end_layout

\begin_layout Itemize
The unused premise 
\begin_inset Formula $B$
\end_inset

 corresponds to unused variable 
\family typewriter
\size footnotesize
\color blue
y:
\begin_inset space ~
\end_inset

B
\family default
\size default
\color inherit
 
\end_layout

\begin_layout Itemize
The 
\begin_inset Quotes eld
\end_inset

create function
\begin_inset Quotes erd
\end_inset

 rule gives the function 
\family typewriter
\size footnotesize
\color blue
{ y:
\begin_inset space ~
\end_inset

B => x }
\family default
\size default
\color inherit
 
\end_layout

\begin_layout Itemize
The second 
\begin_inset Quotes eld
\end_inset

create function
\begin_inset Quotes erd
\end_inset

 rule gives 
\family typewriter
\size footnotesize
\color blue
{ x:
\begin_inset space ~
\end_inset

A => y:
\begin_inset space ~
\end_inset

B => x }
\family default
\size default
\color inherit
 
\end_layout

\begin_layout Itemize
Complete code:
\end_layout

\begin_layout LyX-Code

\family typewriter
\size footnotesize
\color blue
def f[A, B]: A => B => A = { (x: A) => (y: B) => x }
\end_layout

\end_deeper
\begin_layout Itemize
Any code expression's type can be translated into a sequent
\end_layout

\begin_layout Itemize
A proof of a theorem directly guides us in writing code for that type
\end_layout

\begin_layout Itemize
The code can be used to find a proof (every code snippet gives a rule)
\end_layout

\end_deeper
\begin_layout Standard
\begin_inset Separator parbreak
\end_inset


\end_layout

\begin_layout Frame
\begin_inset Argument 4
status open

\begin_layout Plain Layout
Correspondence between programs and proofs
\end_layout

\end_inset


\begin_inset Separator latexpar
\end_inset


\end_layout

\begin_deeper
\begin_layout Itemize
By construction, any theorem can be implemented in code
\end_layout

\begin_layout Standard
\align center
\begin_inset Tabular
<lyxtabular version="3" rows="6" columns="2">
<features tabularvalignment="middle">
<column alignment="center" valignment="top">
<column alignment="center" valignment="top">
<row>
<cell alignment="center" valignment="top" topline="true" bottomline="true" leftline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\series bold
Proposition
\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" bottomline="true" leftline="true" rightline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\series bold
Scala code
\end_layout

\end_inset
</cell>
</row>
<row>
<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout
\begin_inset Formula $\forall A.~A\rightarrow A$
\end_inset


\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" leftline="true" rightline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\family typewriter
\size footnotesize
\color blue
{ x:
\begin_inset space ~
\end_inset

A => x }
\end_layout

\end_inset
</cell>
</row>
<row>
<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout
\begin_inset Formula $\forall A.~A\rightarrow1$
\end_inset


\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" leftline="true" rightline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\family typewriter
\size footnotesize
\color blue
{ x:
\begin_inset space ~
\end_inset

A => () }
\end_layout

\end_inset
</cell>
</row>
<row>
<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout
\begin_inset Formula $\forall A.~\forall B.~A\rightarrow A+B$
\end_inset


\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" leftline="true" rightline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\family typewriter
\size footnotesize
\color blue
Left.apply
\end_layout

\end_inset
</cell>
</row>
<row>
<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout
\begin_inset Formula $\forall A.~\forall B.~A\times B\rightarrow A$
\end_inset


\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" leftline="true" rightline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\family typewriter
\size footnotesize
\color blue
_._1
\end_layout

\end_inset
</cell>
</row>
<row>
<cell alignment="center" valignment="top" topline="true" bottomline="true" leftline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout
\begin_inset Formula $\forall A.~\forall B.~A\rightarrow B\rightarrow A$
\end_inset


\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" bottomline="true" leftline="true" rightline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\family typewriter
\size footnotesize
\color blue
{ x:
\begin_inset space ~
\end_inset

A => y:
\begin_inset space ~
\end_inset

B => x }
\end_layout

\end_inset
</cell>
</row>
</lyxtabular>

\end_inset


\end_layout

\begin_layout Itemize
\begin_inset Quotes eld
\end_inset

Types are propositions, programs are proofs
\begin_inset Quotes erd
\end_inset


\end_layout

\begin_layout Itemize
Also, non-theorems 
\emph on
cannot be implemented
\emph default
 in code 
\end_layout

\begin_deeper
\begin_layout Itemize
Examples of non-theorems:
\begin_inset Newline newline
\end_inset

 
\begin_inset Formula $\forall A.~1\rightarrow A$
\end_inset

; 
\begin_inset space \space{}
\end_inset

 
\begin_inset space \space{}
\end_inset

 
\begin_inset Formula $\quad\forall A.~\forall B.~A+B\rightarrow A$
\end_inset

; 
\begin_inset Newline newline
\end_inset


\begin_inset Formula $\forall A.~\forall B.~A\rightarrow A\times B$
\end_inset

; 
\begin_inset space \space{}
\end_inset

 
\begin_inset Formula $\quad\forall A.~\forall B.~(A\rightarrow B)\rightarrow A$
\end_inset


\end_layout

\end_deeper
\begin_layout Itemize
Given a type's formula, can we implement it in code? Not obvious.
\end_layout

\begin_deeper
\begin_layout Itemize
Example: 
\begin_inset Formula $\forall A.~\forall B.~((((A\rightarrow B)\rightarrow A)\rightarrow A)\rightarrow B)\rightarrow B$
\end_inset


\end_layout

\begin_deeper
\begin_layout Itemize
Can we write a function with this type? Can we prove this formula?
\end_layout

\end_deeper
\end_deeper
\end_deeper
\begin_layout Standard
\begin_inset Separator parbreak
\end_inset


\end_layout

\begin_layout Frame
\begin_inset Argument 4
status open

\begin_layout Plain Layout
The logic of types II
\end_layout

\end_inset


\begin_inset Separator latexpar
\end_inset


\end_layout

\begin_deeper
\begin_layout FrameSubtitle
What kind of logic is this? What do mathematicians call this logic?
\end_layout

\begin_layout Standard
This is called 
\begin_inset Quotes eld
\end_inset

intuitionistic propositional logic
\begin_inset Quotes erd
\end_inset

, IPL (also 
\begin_inset Quotes eld
\end_inset

constructive
\begin_inset Quotes erd
\end_inset

)
\end_layout

\begin_layout Itemize
This is a 
\begin_inset Quotes eld
\end_inset

nonclassical
\begin_inset Quotes erd
\end_inset

 logic because it is different from Boolean logic
\end_layout

\begin_layout Itemize
Disjunction works differently from Boolean logic
\end_layout

\begin_deeper
\begin_layout Itemize
Example: 
\begin_inset Formula $(A\rightarrow B+C)\vdash(A\rightarrow B)+(A\rightarrow C)$
\end_inset

 does not hold in IPL
\end_layout

\begin_layout Itemize
This is counter-intuitive!
\end_layout

\begin_layout Itemize
We cannot implement a function with this type:
\begin_inset VSpace -75baselineskip%
\end_inset


\end_layout

\begin_layout LyX-Code

\family typewriter
\size footnotesize
\color blue
def q[A, B, C]: (A => Either[B, C]) => Either[A => B, A => C]
\end_layout

\begin_layout Itemize
Disjunction is 
\begin_inset Quotes eld
\end_inset

constructive
\begin_inset Quotes erd
\end_inset

: need to supply one of the parts
\end_layout

\begin_deeper
\begin_layout Itemize
...but cannot compute 
\family typewriter
\size footnotesize
\color blue
A => B
\family default
\size default
\color inherit
 or 
\family typewriter
\size footnotesize
\color blue
A => C
\family default
\size default
\color inherit
 from 
\family typewriter
\size footnotesize
\color blue
A => Either[B, C]
\family default
\size default
\color inherit
 
\end_layout

\end_deeper
\end_deeper
\begin_layout Itemize
Implication works differently
\end_layout

\begin_deeper
\begin_layout Itemize
Example: 
\begin_inset Formula $\left(\left(A\rightarrow B\right)\rightarrow A\right)\rightarrow A$
\end_inset

 holds in Boolean logic but not in IPL
\end_layout

\begin_layout Itemize
Cannot compute an 
\family typewriter
\size footnotesize
\color blue
x:
\begin_inset space ~
\end_inset

A
\family default
\size default
\color inherit
 because of insufficient data
\end_layout

\end_deeper
\begin_layout Itemize
Conjunction works the same as in Boolean logic
\end_layout

\begin_deeper
\begin_layout Itemize
Example: 
\begin_inset Formula $(A\rightarrow B\times C)\vdash\left(A\rightarrow B\right)\times\left(A\rightarrow C\right)$
\end_inset

 
\end_layout

\end_deeper
\end_deeper
\begin_layout Standard
\begin_inset Separator parbreak
\end_inset


\end_layout

\begin_layout Frame
\begin_inset Argument 4
status open

\begin_layout Plain Layout
The logic of types III
\end_layout

\end_inset


\begin_inset Separator latexpar
\end_inset


\end_layout

\begin_deeper
\begin_layout FrameSubtitle
How to determine whether a given IPL formula is a theorem?
\end_layout

\begin_layout Itemize
In Boolean logic, we can compute the 
\begin_inset Quotes eld
\end_inset

truth value
\begin_inset Quotes erd
\end_inset

 of a formula and decide whether the formula is a theorem
\end_layout

\begin_layout Itemize
The IPL cannot have a truth table with a fixed number of truth values
\end_layout

\begin_deeper
\begin_layout Itemize
This was proved by G
\begin_inset ERT
status open

\begin_layout Plain Layout


\backslash
"
\end_layout

\end_inset

odel in 1932 (see 
\begin_inset CommandInset href
LatexCommand href
name "Wikipedia page"
target "https://en.wikipedia.org/wiki/Many-valued_logic"
literal "false"

\end_inset

)
\end_layout

\end_deeper
\begin_layout Itemize
The IPL has a decision procedure (algorithm) that either finds a proof for
 a given IPL formula, or determines that there is no proof
\end_layout

\begin_layout Itemize
There may be several inequivalent proofs of an IPL theorem
\end_layout

\begin_layout Itemize
Each proof can be 
\emph on
automatically translated
\emph default
 into code
\end_layout

\begin_deeper
\begin_layout Itemize
The 
\begin_inset CommandInset href
LatexCommand href
name "djinn-ghc"
target "https://hackage.haskell.org/package/djinn-ghc"
literal "false"

\end_inset

 compiler plugin and the 
\begin_inset CommandInset href
LatexCommand href
name "JustDoIt plugin"
target "https://github.com/nomeata/ghc-justdoit"
literal "false"

\end_inset

 implement an IPL prover in Haskell, and generate Haskell code from types
\end_layout

\begin_layout Itemize
The 
\begin_inset CommandInset href
LatexCommand href
name "curryhoward"
target "https://github.com/Chymyst/curryhoward"
literal "false"

\end_inset

 library implements an IPL prover as a Scala macro, and generates Scala
 code from types
\end_layout

\end_deeper
\begin_layout Itemize
All these IPL provers use the same basic algorithm called LJT 
\end_layout

\begin_deeper
\begin_layout Itemize
presented in the paper 
\size footnotesize

\begin_inset CommandInset href
LatexCommand href
name "[Dyckhoff 1992]"
target "https://rd.host.cs.st-andrews.ac.uk/publications/jsl57.pdf"
literal "false"

\end_inset


\end_layout

\end_deeper
\end_deeper
\begin_layout Standard
\begin_inset Separator parbreak
\end_inset


\end_layout

\begin_layout Frame
\begin_inset Argument 4
status open

\begin_layout Plain Layout
Proof search I: looking for an algorithm
\end_layout

\end_inset


\begin_inset Separator latexpar
\end_inset


\end_layout

\begin_deeper
\begin_layout FrameSubtitle
Why our initial presentation of IPL does not give a proof search algorithm
\end_layout

\begin_layout Standard
The FP type constructions give nine axioms and three derivation rules:
\end_layout

\begin_layout Standard
\begin_inset Box Frameless
position "t"
hor_pos "c"
has_inner_box 1
inner_pos "t"
use_parbox 0
use_makebox 0
width "49col%"
special "none"
height "1in"
height_special "totalheight"
thickness "0.4pt"
separation "3pt"
shadowsize "4pt"
framecolor "black"
backgroundcolor "none"
status open

\begin_layout Itemize
\begin_inset Formula $\Gamma,A,B\vdash A\times B$
\end_inset

 
\end_layout

\begin_layout Itemize
\begin_inset Formula $\Gamma,A\times B\vdash A$
\end_inset

 
\end_layout

\begin_layout Itemize
\begin_inset Formula $\Gamma,A\times B\vdash B$
\end_inset


\end_layout

\begin_layout Itemize
\begin_inset Formula $\Gamma,A\rightarrow B,A\vdash B$
\end_inset


\end_layout

\begin_layout Itemize
\begin_inset Formula $\Gamma,A\vdash A+B$
\end_inset

 
\end_layout

\begin_layout Itemize
\begin_inset Formula $\Gamma,B\vdash A+B$
\end_inset


\end_layout

\begin_layout Itemize
\begin_inset Formula $\Gamma,A+B,A\rightarrow C,B\rightarrow C\vdash C$
\end_inset


\end_layout

\begin_layout Itemize
\begin_inset Formula $\Gamma\vdash1$
\end_inset


\end_layout

\begin_layout Itemize
\begin_inset Formula $\Gamma,A\vdash A$
\end_inset


\end_layout

\end_inset


\begin_inset Box Frameless
position "t"
hor_pos "c"
has_inner_box 1
inner_pos "t"
use_parbox 0
use_makebox 0
width "49col%"
special "none"
height "1in"
height_special "totalheight"
thickness "0.4pt"
separation "3pt"
shadowsize "4pt"
framecolor "black"
backgroundcolor "none"
status open

\begin_layout Plain Layout
\begin_inset Formula 
\[
\frac{\Gamma,A\vdash B}{\Gamma\vdash A\rightarrow B}
\]

\end_inset


\begin_inset Formula 
\[
\frac{\Gamma\vdash G}{\Gamma,D\vdash G}
\]

\end_inset


\begin_inset Formula 
\[
\frac{\Gamma,A,B\vdash G}{\Gamma,B,A\vdash G}
\]

\end_inset


\end_layout

\end_inset


\end_layout

\begin_layout Standard
\begin_inset VSpace defskip
\end_inset

Can we use these rules to obtain a finite and complete search tree? No.
\end_layout

\begin_layout Itemize
Try proving 
\begin_inset Formula $A,B+C\vdash A\times B+C$
\end_inset

: cannot find matching rules
\end_layout

\begin_deeper
\begin_layout Itemize
Need a better formulation of the logic
\end_layout

\end_deeper
\end_deeper
\begin_layout Standard
\begin_inset Separator parbreak
\end_inset


\end_layout

\begin_layout Frame
\begin_inset Argument 4
status open

\begin_layout Plain Layout
Proof search II: Gentzen's calculus LJ (1935)
\end_layout

\end_inset


\begin_inset Separator latexpar
\end_inset


\end_layout

\begin_deeper
\begin_layout Itemize
A 
\begin_inset Quotes eld
\end_inset

complete and sound calculus
\begin_inset Quotes erd
\end_inset

 is a set of axioms and derivation rules that will yield all (and only!)
 theorems of the logic
\begin_inset Formula 
\begin{align*}
\text{(}A\text{ is atomic)\,}\frac{}{\Gamma,{\color{blue}A}\vdash A}\:Id & \qquad\frac{}{\Gamma\vdash{\color{blue}\top}}\,\top\\
\frac{\Gamma,A\rightarrow B\vdash A\quad\;\Gamma,B\vdash C}{\Gamma,{\color{blue}A\rightarrow B}\vdash C}\:L_{\rightarrow} & \qquad\frac{\Gamma,A\vdash B}{\Gamma\vdash{\color{blue}A\rightarrow B}}\,R_{\rightarrow}\\
\frac{\Gamma,A\vdash C\quad\;\Gamma,B\vdash C}{\Gamma,{\color{blue}A+B}\vdash C}\:L_{+} & \qquad\frac{\Gamma\vdash A_{i}}{\Gamma\vdash{\color{blue}A_{1}+A_{2}}}\,R_{+_{i}}\\
\frac{\Gamma,A_{i}\vdash C}{\Gamma,{\color{blue}A_{1}\times A_{2}}\vdash C}\:L_{\times_{i}} & \qquad\frac{\Gamma\vdash A\quad\;\Gamma\vdash B}{\Gamma\vdash{\color{blue}A\times B}}\,R_{\times}
\end{align*}

\end_inset


\end_layout

\begin_layout Itemize
Two axioms and eight derivation rules
\end_layout

\begin_deeper
\begin_layout Itemize
Each derivation rule says: The sequent at bottom will be proved if proofs
 are given for sequent(s) at top
\end_layout

\begin_layout Itemize
The symbol 
\begin_inset Formula $\Gamma$
\end_inset

 means 
\begin_inset Quotes eld
\end_inset

any number of premises, or 
\begin_inset Formula $\emptyset$
\end_inset


\begin_inset Quotes erd
\end_inset


\end_layout

\end_deeper
\begin_layout Itemize
Use these rules 
\begin_inset Quotes eld
\end_inset

bottom-up
\begin_inset Quotes erd
\end_inset

 to perform a proof search
\end_layout

\begin_deeper
\begin_layout Itemize
Sequents are nodes and proofs are edges in the tree of proof search
\end_layout

\end_deeper
\end_deeper
\begin_layout Standard
\begin_inset Separator parbreak
\end_inset


\end_layout

\begin_layout Frame
\begin_inset Argument 4
status open

\begin_layout Plain Layout
Proof search example I
\end_layout

\end_inset


\begin_inset Separator latexpar
\end_inset


\end_layout

\begin_deeper
\begin_layout Standard
Example: to prove 
\begin_inset Formula $\forall R.\,\forall Q.\,\left(\left(R\rightarrow R\right)\rightarrow Q\right)\rightarrow Q$
\end_inset


\end_layout

\begin_layout Itemize
Root sequent 
\begin_inset Formula $S_{0}:\emptyset\vdash\left(\left(R\rightarrow R\right)\rightarrow Q\right)\rightarrow Q$
\end_inset


\end_layout

\begin_layout Itemize
\begin_inset Formula $S_{0}$
\end_inset

 with rule 
\begin_inset Formula $R_{\rightarrow}$
\end_inset

 yields 
\begin_inset Formula $S_{1}:\left(R\rightarrow R\right)\rightarrow Q\vdash Q$
\end_inset


\end_layout

\begin_layout Itemize
\begin_inset Formula $S_{1}$
\end_inset

 with rule 
\begin_inset Formula $L_{\rightarrow}$
\end_inset

 yields 
\begin_inset Formula $S_{2}:\left(R\rightarrow R\right)\rightarrow Q\vdash R\rightarrow R$
\end_inset

 and 
\begin_inset Formula $S_{3}:Q\vdash Q$
\end_inset


\end_layout

\begin_layout Itemize
Sequent 
\begin_inset Formula $S_{3}$
\end_inset

 follows from the 
\begin_inset Formula $Id$
\end_inset

 axiom; it remains to prove 
\begin_inset Formula $S_{2}$
\end_inset


\end_layout

\begin_layout Itemize
\begin_inset Formula $S_{2}$
\end_inset

 with rule 
\begin_inset Formula $L_{\rightarrow}$
\end_inset

 yields 
\begin_inset Formula $S_{4}:\left(R\rightarrow R\right)\rightarrow Q\vdash R\rightarrow R$
\end_inset

 and 
\begin_inset Formula $S_{5}:Q\vdash R\rightarrow R$
\end_inset


\end_layout

\begin_deeper
\begin_layout Itemize
We are stuck here because 
\begin_inset Formula $S_{4}=S_{2}$
\end_inset

 (we are in a loop)
\end_layout

\begin_layout Itemize
We can prove 
\begin_inset Formula $S_{5}$
\end_inset

 but that will not help
\end_layout

\begin_layout Itemize
So we backtrack (erase 
\begin_inset Formula $S_{4}$
\end_inset

, 
\begin_inset Formula $S_{5}$
\end_inset

) and apply another rule to 
\begin_inset Formula $S_{2}$
\end_inset


\end_layout

\end_deeper
\begin_layout Itemize
\begin_inset Formula $S_{2}$
\end_inset

 with rule 
\begin_inset Formula $R_{\rightarrow}$
\end_inset

 yields 
\begin_inset Formula $S_{6}:\left(R\rightarrow R\right)\rightarrow Q;R\vdash R$
\end_inset


\end_layout

\begin_layout Itemize
Sequent 
\begin_inset Formula $S_{6}$
\end_inset

 follows from the 
\begin_inset Formula $Id$
\end_inset

 axiom
\end_layout

\begin_layout Standard
Therefore we have proved 
\begin_inset Formula $S_{0}$
\end_inset


\end_layout

\begin_layout Standard
Since 
\begin_inset Formula $\left(\left(R\rightarrow R\right)\rightarrow Q\right)\rightarrow Q$
\end_inset

 is derived from no premises, it is a theorem
\end_layout

\begin_layout Standard
\begin_inset Formula $Q.E.D.$
\end_inset


\end_layout

\end_deeper
\begin_layout Standard
\begin_inset Separator parbreak
\end_inset


\end_layout

\begin_layout Frame
\begin_inset Argument 4
status open

\begin_layout Plain Layout
Proof search III: The calculus LJT
\end_layout

\end_inset


\begin_inset Separator latexpar
\end_inset


\end_layout

\begin_deeper
\begin_layout FrameSubtitle
Gentzen-Vorobieff-Hudelmaier-Dyckhoff, 1935–1990
\end_layout

\begin_layout Itemize
The Gentzen calculus LJ will loop if rule 
\begin_inset Formula $L_{\rightarrow}$
\end_inset

 is applied 
\begin_inset Formula $\geq2$
\end_inset

 times
\end_layout

\begin_layout Itemize
The calculus LJT keeps all rules of LJ except rule 
\begin_inset Formula $L_{\rightarrow}$
\end_inset


\end_layout

\begin_layout Itemize
Replace rule 
\begin_inset Formula $L_{\rightarrow}$
\end_inset

 by pattern-matching on 
\begin_inset Formula $A$
\end_inset

 in the premise 
\begin_inset Formula $A\rightarrow B$
\end_inset

:
\begin_inset Formula 
\begin{align*}
\text{(if }A\text{ is atomic)\,}\frac{\Gamma,A,B\vdash D}{\Gamma,A,{\color{blue}A\rightarrow B}\vdash D}\:L_{\rightarrow_{1}}\\
\frac{\Gamma,A\rightarrow B\rightarrow C\vdash D}{\Gamma,{\color{blue}(A\times B)\rightarrow C}\vdash D}\:L_{\rightarrow_{2}}\\
\frac{\Gamma,A\rightarrow C,B\rightarrow C\vdash D}{\Gamma,{\color{blue}(A+B)\rightarrow C}\vdash D}\:L_{\rightarrow_{3}}\\
\frac{\Gamma,B\rightarrow C\vdash A\rightarrow B\quad\quad\Gamma,C\vdash D}{\Gamma,{\color{blue}(A\rightarrow B)\rightarrow C}\vdash D}\:L_{\rightarrow_{4}}
\end{align*}

\end_inset


\end_layout

\begin_layout Itemize
When using LJT rules, the proof tree has no loops and terminates
\end_layout

\begin_deeper
\begin_layout Itemize
See 
\begin_inset CommandInset href
LatexCommand href
name "this paper"
target "http://citeseer.ist.psu.edu/viewdoc/summary?doi=10.1.1.35.2618"
literal "false"

\end_inset

 for an explicit decreasing measure on the proof tree
\end_layout

\end_deeper
\end_deeper
\begin_layout Standard
\begin_inset Separator parbreak
\end_inset


\end_layout

\begin_layout Frame
\begin_inset Argument 4
status open

\begin_layout Plain Layout
Proof search IV: From deduction rules to code
\end_layout

\end_inset


\begin_inset Separator latexpar
\end_inset


\end_layout

\begin_deeper
\begin_layout Itemize
The new rules are equivalent to the old rules, therefore...
\end_layout

\begin_deeper
\begin_layout Itemize
Proof of a sequent 
\begin_inset Formula $A,B,C\vdash G$
\end_inset

 
\begin_inset Formula $\Leftrightarrow$
\end_inset

 code snippet 
\begin_inset Formula $t(a,b,c):G$
\end_inset


\end_layout

\begin_layout Itemize
Also can be seen as a function 
\begin_inset Formula $t$
\end_inset

 from 
\begin_inset Formula $A,B,C$
\end_inset

 to 
\begin_inset Formula $G$
\end_inset


\end_layout

\end_deeper
\begin_layout Itemize
Sequent in a proof follows from an axiom or from a transforming rule
\end_layout

\begin_deeper
\begin_layout Itemize
The two axioms are fixed expressions, 
\begin_inset Formula $x^{:A}\rightarrow x$
\end_inset

 and 
\begin_inset Formula $1$
\end_inset


\end_layout

\begin_layout Itemize
Each rule has a 
\emph on
proof transformer
\emph default
 function: 
\begin_inset Formula $\text{PT}_{R_{\rightarrow}}$
\end_inset

 , 
\begin_inset Formula $\text{PT}_{L_{+}}$
\end_inset

 , etc.
\end_layout

\end_deeper
\begin_layout Itemize
Examples of proof transformer functions:
\end_layout

\begin_layout Standard
\begin_inset Formula 
\[
\frac{\Gamma,A\vdash C\quad\;\Gamma,B\vdash C}{\Gamma,{\color{blue}A+B}\vdash C}\:L_{+}
\]

\end_inset


\begin_inset VSpace -100baselineskip%
\end_inset


\begin_inset Formula 
\[
PT_{L_{+}}(t_{1}^{:A\rightarrow C},t_{2}^{:B\rightarrow C})=x^{:A+B}\rightarrow\ x\ \text{match}\begin{cases}
a^{:A}\rightarrow t_{1}(a)\\
b^{:B}\rightarrow t_{2}(b)
\end{cases}=\,\begin{array}{|c||c|}
 & C\\
\hline A & t_{1}\\
B & t_{2}
\end{array}
\]

\end_inset


\begin_inset VSpace -40baselineskip%
\end_inset


\begin_inset Formula 
\begin{align*}
\frac{\Gamma,A\rightarrow B\rightarrow C\vdash D}{\Gamma,{\color{blue}(A\times B)\rightarrow C}\vdash D}\:L_{\rightarrow_{2}}\\
PT_{L_{\rightarrow_{2}}}(f^{:\left(A\rightarrow B\rightarrow C\right)\rightarrow D})=g^{:A\times B\rightarrow C}\rightarrow & f\,(x^{:A}\rightarrow y^{:B}\rightarrow g(x,y))
\end{align*}

\end_inset


\end_layout

\begin_layout Itemize
Verify that we can indeed produce PTs for every rule of LJT
\end_layout

\end_deeper
\begin_layout Standard
\begin_inset Separator parbreak
\end_inset


\end_layout

\begin_layout Frame
\begin_inset Argument 4
status open

\begin_layout Plain Layout
Proof search example II: code inference
\end_layout

\end_inset


\begin_inset Separator latexpar
\end_inset


\end_layout

\begin_deeper
\begin_layout Standard
Once a proof tree is found, start from leaves and apply PTs
\end_layout

\begin_layout Itemize
For each sequent 
\begin_inset Formula $S_{i}$
\end_inset

, this will derive a 
\series bold
proof expression
\series default
 
\begin_inset Formula $t_{i}$
\end_inset


\end_layout

\begin_layout Itemize
Example: to prove 
\begin_inset Formula $S_{0}$
\end_inset

, start from 
\begin_inset Formula $S_{6}$
\end_inset

 backwards:
\size footnotesize

\begin_inset Formula 
\begin{align*}
S_{6}:\left(R\rightarrow R\right)\rightarrow Q;R\vdash R\quad(\text{axiom }Id)\quad & \text{\texttt{def t6(rrq, r) = r}}\\
S_{2}:\left(R\rightarrow R\right)\rightarrow Q\vdash\left(R\rightarrow R\right)\quad\text{PT}_{R_{\rightarrow}}(t_{6})\quad & \text{\texttt{def t2(rrq) = r => t6(rrq, r)}}\\
S_{3}:Q\vdash Q\quad(\text{axiom }Id)\quad & \text{\texttt{def t3(q) = q}}\\
S_{1}:\left(R\rightarrow R\right)\rightarrow Q\vdash Q\quad\text{PT}_{L_{\rightarrow}}(t_{2},t_{3})\quad & \text{\texttt{def t1(rrq) = t3(rrq(t2(rrq)))}}\\
S_{0}:\emptyset\vdash\left(\left(R\rightarrow R\right)\rightarrow Q\right)\rightarrow Q\quad\text{PT}_{R_{\rightarrow}}(t_{1})\quad & \text{\texttt{def t0 = rrq => t1(rrq)}}
\end{align*}

\end_inset


\end_layout

\begin_layout Itemize
The proof expression for 
\begin_inset Formula $S_{0}$
\end_inset

 is then obtained as
\begin_inset Formula 
\begin{align*}
\text{\texttt{def t0 = \{ rrq => t3(rrq(t2(rrq))) \}}}\\
\text{\texttt{= \{ rrq => rrq(r => t6(rrq, r)) \}}}\\
\text{\texttt{= \{ rrq => rrq(r => r) \}}}
\end{align*}

\end_inset

Simplified final code having the required type: 
\end_layout

\begin_layout LyX-Code

\family typewriter
\size footnotesize
\color blue
def t0[R, Q]: ((R => R) => Q) => Q = { x => x(y => y) }
\end_layout

\end_deeper
\begin_layout Standard
\begin_inset Separator parbreak
\end_inset


\end_layout

\begin_layout Frame
\begin_inset Argument 4
status open

\begin_layout Plain Layout
Using the 
\family typewriter
curryhoward
\family default
 library for code inference
\end_layout

\end_inset


\begin_inset Separator latexpar
\end_inset


\end_layout

\begin_deeper
\begin_layout Standard
Two main use cases:
\end_layout

\begin_layout Enumerate
Define a type signature and derive an implementation automatically
\end_layout

\begin_layout LyX-Code

\family typewriter
\size footnotesize
\color blue
def map[E, A, B](reader: E => A, f: A => B): E => B = implement
\end_layout

\begin_layout Enumerate
Automatically build an expression from previously computed values
\end_layout

\begin_layout LyX-Code

\family typewriter
\size footnotesize
\color blue
val f(a: String, b: Boolean): Int = {...}
\end_layout

\begin_layout LyX-Code

\family typewriter
\size footnotesize
\color blue
case class Result(x: Int, name: String)
\end_layout

\begin_layout LyX-Code

\family typewriter
\size footnotesize
\color blue
val result = ofType[Result]("abc", f, true)
\end_layout

\begin_layout Standard
Fixed types (
\family typewriter
\size footnotesize
\color blue
Int
\family default
\size default
\color inherit
, 
\family typewriter
\size footnotesize
\color blue
String
\family default
\size default
\color inherit
, etc.) are treated as type parameters
\end_layout

\begin_layout Itemize
This is a practical application of the Curry-Howard correspondence
\end_layout

\begin_layout Itemize
The CH correspondence works only for 
\begin_inset Quotes eld
\end_inset

fully parametric
\begin_inset Quotes erd
\end_inset

 code
\end_layout

\end_deeper
\begin_layout Standard
\begin_inset Separator parbreak
\end_inset


\end_layout

\begin_layout Frame
\begin_inset Argument 4
status open

\begin_layout Plain Layout
Summary
\end_layout

\end_inset


\begin_inset Separator latexpar
\end_inset


\end_layout

\begin_deeper
\begin_layout Itemize
The CH correspondence maps the type system of each programming language
 into a certain system of logical propositions 
\end_layout

\begin_layout Itemize
Proof of logical propositions corresponds to implementation of the type
\end_layout

\begin_layout Itemize
If the logic of types is decidable, we can automatically produce code from
 type signatures
\end_layout

\begin_layout Itemize
Simple fully parametric code corresponds to IPL, which is decidable
\end_layout

\begin_layout Itemize
Algorithms exist for proof search (and for disproof search) in IPL
\end_layout

\begin_deeper
\begin_layout Itemize
See the book by R.
\begin_inset space ~
\end_inset

Bornat: 
\emph on
Proof and Disproof in Formal Logic
\emph default
 (2005)
\end_layout

\end_deeper
\begin_layout Itemize
The CH correspondence provides powerful type-directed reasoning about code,
 as long as we work with fully parametric functions
\end_layout

\begin_layout Itemize
Software engineers need to develop intuition for this reasoning
\end_layout

\begin_deeper
\begin_layout Itemize
The decision procedures are not easy to use 
\end_layout

\begin_layout Itemize
Software can help, e.g., the 
\family typewriter
\size footnotesize
\color blue
curryhoward
\family default
\size default
\color inherit
 library
\end_layout

\end_deeper
\begin_layout Itemize
CH is a mathematical theory that helps programmers write code
\end_layout

\begin_deeper
\begin_layout Itemize
Functional programming is an engineering discipline
\end_layout

\end_deeper
\end_deeper
\end_body
\end_document