Natural Deduction and Normalization Proofs for the Intersection Type   Discipline

Federico Aschieri

arXiv:1904.10106·cs.LO·April 24, 2019·DCM/ITRS

Natural Deduction and Normalization Proofs for the Intersection Type Discipline

Federico Aschieri

PDF

Open Access

TL;DR

This paper develops a systematic approach to intersection types using natural deduction, linking beta reduction steps to Prawitz reductions, and proves normalization theorems for systems D and Omega.

Contribution

It introduces a new natural deduction framework for intersection types and derives normalization results directly from typing derivations.

Findings

01

Beta reduction corresponds to Prawitz reductions in derivations

02

System D is strongly normalizing

03

System Omega terminates leftmost reductions for typable terms

Abstract

Refining and extending previous work by Retor\'e, we develop a systematic approach to intersection types via natural deduction. We show how a step of beta reduction can be seen as performing, at the level of typing derivations, Prawitz reductions in parallel. Then we derive as immediate consequences of Subject Reduction the main theorems about normalization for intersection types: for system D, strong normalization, for system Omega, the leftmost reduction termination for terms typable without Omega.

Tables1

Table 1. Table 1: Reduction relation on typing derivations

: x A D : u B : ⁢ λ x u → A B E : t A : ⁢ (⁢ λ x u) t B

Equations70

x : A

x : A

x : A

x : A

t : A \land B

t : A \land B

x : A

x : A

E

E

x : A

x : A

E

E

t = (λ x u) v t_{1} \dots t_{n}

t = (λ x u) v t_{1} \dots t_{n}

t^{'} = u [v / x] t_{1} \dots t_{n}

t^{'} = u [v / x] t_{1} \dots t_{n}

\ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 70.97774 pt \vbox \vbox \vbox D_{1} \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip t : A_{1} \vbox D_{2} \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip t : A_{2} \vskip 2.0pt \nointerlineskip \lower -0.2ptto74.94244pt \xleaders \hrule \hfill \lower -0.2pt \vskip 2.0pt \nointerlineskip t : A_{1} \land A_{2} \vskip 2.0pt \nointerlineskip \lower -0.2ptto49.43321pt \xleaders \hrule \hfill \lower -0.2pt \vskip 2.0pt \nointerlineskip t : A_{i} \ignorespaces ⇝ \ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 25.33998 pt \vbox D_{i} \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip t : A_{i} \ignorespaces

\ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 70.97774 pt \vbox \vbox \vbox D_{1} \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip t : A_{1} \vbox D_{2} \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip t : A_{2} \vskip 2.0pt \nointerlineskip \lower -0.2ptto74.94244pt \xleaders \hrule \hfill \lower -0.2pt \vskip 2.0pt \nointerlineskip t : A_{1} \land A_{2} \vskip 2.0pt \nointerlineskip \lower -0.2ptto49.43321pt \xleaders \hrule \hfill \lower -0.2pt \vskip 2.0pt \nointerlineskip t : A_{i} \ignorespaces ⇝ \ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 25.33998 pt \vbox D_{i} \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip t : A_{i} \ignorespaces

\ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 24.41666 pt \vbox D \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip t : B \ignorespaces ⇝ \ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 24.85316 pt \vbox D^{'} \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip t^{'} : B \ignorespaces \Rightarrow \ignorespaces \ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 46.48888 pt \vbox \vbox D \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip t : B \vskip 2.0pt \nointerlineskip \lower -0.2ptto59.30183pt \xleaders \hrule \hfill \lower -0.2pt \vskip 2.0pt \nointerlineskip λ x t : A \to B \ignorespaces ⇝ \ignorespaces \ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 47.20634 pt \vbox \vbox D^{'} \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip t^{'} : B \vskip 2.0pt \nointerlineskip \lower -0.2ptto58.06412pt \xleaders \hrule \hfill \lower -0.2pt \vskip 2.0pt \nointerlineskip λ x t^{'} : A \to B \ignorespaces

\ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 24.41666 pt \vbox D \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip t : B \ignorespaces ⇝ \ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 24.85316 pt \vbox D^{'} \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip t^{'} : B \ignorespaces \Rightarrow \ignorespaces \ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 46.48888 pt \vbox \vbox D \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip t : B \vskip 2.0pt \nointerlineskip \lower -0.2ptto59.30183pt \xleaders \hrule \hfill \lower -0.2pt \vskip 2.0pt \nointerlineskip λ x t : A \to B \ignorespaces ⇝ \ignorespaces \ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 47.20634 pt \vbox \vbox D^{'} \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip t^{'} : B \vskip 2.0pt \nointerlineskip \lower -0.2ptto58.06412pt \xleaders \hrule \hfill \lower -0.2pt \vskip 2.0pt \nointerlineskip λ x t^{'} : A \to B \ignorespaces

\ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 25.31888 pt \vbox D \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip t : A_{1} \land A_{2} \ignorespaces ⇝ \ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 25.75539 pt \vbox D^{'} \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip t^{'} : A_{1} \land A_{2} \ignorespaces \Rightarrow \ignorespaces \ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 48.15886 pt \vbox \vbox D \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip t : A_{1} \land A_{2} \vskip 2.0pt \nointerlineskip \lower -0.2ptto49.43321pt \xleaders \hrule \hfill \lower -0.2pt \vskip 2.0pt \nointerlineskip t : A_{i} \ignorespaces ⇝ \ignorespaces \ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 49.03189 pt \vbox \vbox D^{'} \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip t^{'} : A_{1} \land A_{2} \vskip 2.0pt \nointerlineskip \lower -0.2ptto48.1955pt \xleaders \hrule \hfill \lower -0.2pt \vskip 2.0pt \nointerlineskip t^{'} : A_{i} \ignorespaces

\ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 25.31888 pt \vbox D \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip t : A_{1} \land A_{2} \ignorespaces ⇝ \ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 25.75539 pt \vbox D^{'} \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip t^{'} : A_{1} \land A_{2} \ignorespaces \Rightarrow \ignorespaces \ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 48.15886 pt \vbox \vbox D \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip t : A_{1} \land A_{2} \vskip 2.0pt \nointerlineskip \lower -0.2ptto49.43321pt \xleaders \hrule \hfill \lower -0.2pt \vskip 2.0pt \nointerlineskip t : A_{i} \ignorespaces ⇝ \ignorespaces \ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 49.03189 pt \vbox \vbox D^{'} \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip t^{'} : A_{1} \land A_{2} \vskip 2.0pt \nointerlineskip \lower -0.2ptto48.1955pt \xleaders \hrule \hfill \lower -0.2pt \vskip 2.0pt \nointerlineskip t^{'} : A_{i} \ignorespaces

\ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 24.41666 pt \vbox D \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip t : A \ignorespaces ⇝ \ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 24.85316 pt \vbox D^{'} \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip t^{'} : A \ignorespaces, \ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 24.41666 pt \vbox E \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip t : B \ignorespaces ⇝ \ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 24.85316 pt \vbox E^{'} \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip t^{'} : B \ignorespaces \Rightarrow \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 46.33331 pt \vbox \vbox D \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip t : A \vbox E \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip t : B \vskip 2.0pt \nointerlineskip \lower -0.2ptto69.92923pt \xleaders \hrule \hfill \lower -0.2pt \vskip 2.0pt \nointerlineskip t : A \land B \ignorespaces ⇝ \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 47.20634 pt \vbox \vbox D^{'} \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip t^{'} : A \vbox E^{'} \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip t^{'} : B \vskip 2.0pt \nointerlineskip \lower -0.2ptto67.4538pt \xleaders \hrule \hfill \lower -0.2pt \vskip 2.0pt \nointerlineskip t^{'} : A \land B \ignorespaces

\ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 24.41666 pt \vbox D \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip t : A \ignorespaces ⇝ \ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 24.85316 pt \vbox D^{'} \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip t^{'} : A \ignorespaces, \ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 24.41666 pt \vbox E \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip t : B \ignorespaces ⇝ \ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 24.85316 pt \vbox E^{'} \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip t^{'} : B \ignorespaces \Rightarrow \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 46.33331 pt \vbox \vbox D \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip t : A \vbox E \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip t : B \vskip 2.0pt \nointerlineskip \lower -0.2ptto69.92923pt \xleaders \hrule \hfill \lower -0.2pt \vskip 2.0pt \nointerlineskip t : A \land B \ignorespaces ⇝ \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 47.20634 pt \vbox \vbox D^{'} \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip t^{'} : A \vbox E^{'} \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip t^{'} : B \vskip 2.0pt \nointerlineskip \lower -0.2ptto67.4538pt \xleaders \hrule \hfill \lower -0.2pt \vskip 2.0pt \nointerlineskip t^{'} : A \land B \ignorespaces

\ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 24.41666 pt \vbox D \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip t : A \ignorespaces ⇝ \ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 24.85316 pt \vbox D^{'} \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip t^{'} : A \ignorespaces \Rightarrow \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 46.48888 pt \vbox \vbox D \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip t : A \to B \vbox E \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip u : A \vskip 2.0pt \nointerlineskip \lower -0.2ptto90.09814pt \xleaders \hrule \hfill \lower -0.2pt \vskip 2.0pt \nointerlineskip t u : B \ignorespaces ⇝ \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 47.20634 pt \vbox \vbox D^{'} \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip t^{'} : A \to B \vbox E \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip u : A \vskip 2.0pt \nointerlineskip \lower -0.2ptto88.86043pt \xleaders \hrule \hfill \lower -0.2pt \vskip 2.0pt \nointerlineskip t^{'} u : B \ignorespaces

\ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 24.41666 pt \vbox D \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip t : A \ignorespaces ⇝ \ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 24.85316 pt \vbox D^{'} \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip t^{'} : A \ignorespaces \Rightarrow \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 46.48888 pt \vbox \vbox D \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip t : A \to B \vbox E \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip u : A \vskip 2.0pt \nointerlineskip \lower -0.2ptto90.09814pt \xleaders \hrule \hfill \lower -0.2pt \vskip 2.0pt \nointerlineskip t u : B \ignorespaces ⇝ \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 47.20634 pt \vbox \vbox D^{'} \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip t^{'} : A \to B \vbox E \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip u : A \vskip 2.0pt \nointerlineskip \lower -0.2ptto88.86043pt \xleaders \hrule \hfill \lower -0.2pt \vskip 2.0pt \nointerlineskip t^{'} u : B \ignorespaces

\ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 24.41666 pt \vbox E \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip u : A \ignorespaces ⇝ \ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 24.41666 pt \vbox E^{'} \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip u^{'} : A \ignorespaces \Rightarrow \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 46.48888 pt \vbox \vbox D \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip t : A \to B \vbox E \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip u : A \vskip 2.0pt \nointerlineskip \lower -0.2ptto90.09814pt \xleaders \hrule \hfill \lower -0.2pt \vskip 2.0pt \nointerlineskip t u : B \ignorespaces ⇝ \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 46.48888 pt \vbox \vbox D \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip t : A \to B \vbox E^{'} \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip u^{'} : A \vskip 2.0pt \nointerlineskip \lower -0.2ptto88.86043pt \xleaders \hrule \hfill \lower -0.2pt \vskip 2.0pt \nointerlineskip t u^{'} : B \ignorespaces

\ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 24.41666 pt \vbox E \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip u : A \ignorespaces ⇝ \ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 24.41666 pt \vbox E^{'} \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip u^{'} : A \ignorespaces \Rightarrow \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 46.48888 pt \vbox \vbox D \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip t : A \to B \vbox E \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip u : A \vskip 2.0pt \nointerlineskip \lower -0.2ptto90.09814pt \xleaders \hrule \hfill \lower -0.2pt \vskip 2.0pt \nointerlineskip t u : B \ignorespaces ⇝ \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 46.48888 pt \vbox \vbox D \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip t : A \to B \vbox E^{'} \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip u^{'} : A \vskip 2.0pt \nointerlineskip \lower -0.2ptto88.86043pt \xleaders \hrule \hfill \lower -0.2pt \vskip 2.0pt \nointerlineskip t u^{'} : B \ignorespaces

D = \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 69.1833 pt \vbox \vbox \vbox x : A \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip D^{'} \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip u : B \vskip 2.0pt \nointerlineskip \lower -0.2ptto61.4153pt \xleaders \hrule \hfill \lower -0.2pt \vskip 2.0pt \nointerlineskip λ x u : A \to B \ignorespaces

D = \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 69.1833 pt \vbox \vbox \vbox x : A \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip D^{'} \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip u : B \vskip 2.0pt \nointerlineskip \lower -0.2ptto61.4153pt \xleaders \hrule \hfill \lower -0.2pt \vskip 2.0pt \nointerlineskip λ x u : A \to B \ignorespaces

t \mapsto t^{'} \Rightarrow \ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 24.41666 pt \vbox D \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip t : A \ignorespaces ⇝^{+} \ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 24.85316 pt \vbox D^{'} \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip t^{'} : A \ignorespaces

t \mapsto t^{'} \Rightarrow \ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 24.41666 pt \vbox D \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip t : A \ignorespaces ⇝^{+} \ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 24.85316 pt \vbox D^{'} \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip t^{'} : A \ignorespaces

\ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 24.41666 pt \vbox D \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip t : A \ignorespaces ⇝^{+} \ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 24.85316 pt \vbox D^{'} \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip t^{'} : A \ignorespaces

\ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 24.41666 pt \vbox D \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip t : A \ignorespaces ⇝^{+} \ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 24.85316 pt \vbox D^{'} \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip t^{'} : A \ignorespaces

\ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 24.41666 pt \vbox D \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip t : A \ignorespaces ⇝^{+} \ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 24.85316 pt \vbox D^{'} \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip t^{'} : A \ignorespaces

\ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 24.41666 pt \vbox D \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip t : A \ignorespaces ⇝^{+} \ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 24.85316 pt \vbox D^{'} \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip t^{'} : A \ignorespaces

\ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 24.41666 pt \vbox D^{'} \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip u : C \ignorespaces ⇝^{+} \ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 24.41666 pt \vbox D^{''} \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip u^{'} : C \ignorespaces

\ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 24.41666 pt \vbox D^{'} \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip u : C \ignorespaces ⇝^{+} \ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 24.41666 pt \vbox D^{''} \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip u^{'} : C \ignorespaces

D = \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 69.1833 pt \vbox \vbox \vbox x : B \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip D^{'} \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip u : C \vskip 2.0pt \nointerlineskip \lower -0.2ptto61.77777pt \xleaders \hrule \hfill \lower -0.2pt \vskip 2.0pt \nointerlineskip λ x u : B \to C \ignorespaces ⇝^{+} \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 69.1833 pt \vbox \vbox \vbox x : B \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip D^{''} \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip u^{'} : C \vskip 2.0pt \nointerlineskip \lower -0.2ptto60.54005pt \xleaders \hrule \hfill \lower -0.2pt \vskip 2.0pt \nointerlineskip λ x u^{'} : B \to C \ignorespaces

D = \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 69.1833 pt \vbox \vbox \vbox x : B \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip D^{'} \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip u : C \vskip 2.0pt \nointerlineskip \lower -0.2ptto61.77777pt \xleaders \hrule \hfill \lower -0.2pt \vskip 2.0pt \nointerlineskip λ x u : B \to C \ignorespaces ⇝^{+} \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 69.1833 pt \vbox \vbox \vbox x : B \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip D^{''} \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip u^{'} : C \vskip 2.0pt \nointerlineskip \lower -0.2ptto60.54005pt \xleaders \hrule \hfill \lower -0.2pt \vskip 2.0pt \nointerlineskip λ x u^{'} : B \to C \ignorespaces

\ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 24.57222 pt \vbox E \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip u : B \to A \ignorespaces ⇝^{+} \ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 24.57222 pt \vbox E^{'} \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip u^{'} : B \to A \ignorespaces

\ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 24.57222 pt \vbox E \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip u : B \to A \ignorespaces ⇝^{+} \ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 24.57222 pt \vbox E^{'} \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip u^{'} : B \to A \ignorespaces

\ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 46.48888 pt \vbox \vbox E \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip u : B \to A \vbox F \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip v : B \vskip 2.0pt \nointerlineskip \lower -0.2ptto92.27983pt \xleaders \hrule \hfill \lower -0.2pt \vskip 2.0pt \nointerlineskip u v : A \ignorespaces ⇝^{+} \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 46.48888 pt \vbox \vbox E^{'} \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip u^{'} : B \to A \vbox F \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip v : B \vskip 2.0pt \nointerlineskip \lower -0.2ptto91.04211pt \xleaders \hrule \hfill \lower -0.2pt \vskip 2.0pt \nointerlineskip u^{'} v : A \ignorespaces

\ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 46.48888 pt \vbox \vbox E \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip u : B \to A \vbox F \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip v : B \vskip 2.0pt \nointerlineskip \lower -0.2ptto92.27983pt \xleaders \hrule \hfill \lower -0.2pt \vskip 2.0pt \nointerlineskip u v : A \ignorespaces ⇝^{+} \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 46.48888 pt \vbox \vbox E^{'} \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip u^{'} : B \to A \vbox F \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip v : B \vskip 2.0pt \nointerlineskip \lower -0.2ptto91.04211pt \xleaders \hrule \hfill \lower -0.2pt \vskip 2.0pt \nointerlineskip u^{'} v : A \ignorespaces

E = \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 69.1833 pt \vbox \vbox \vbox x : B \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip E^{'} \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip w : A \vskip 2.0pt \nointerlineskip \lower -0.2ptto63.11897pt \xleaders \hrule \hfill \lower -0.2pt \vskip 2.0pt \nointerlineskip λ x w : B \to A \ignorespaces

E = \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 69.1833 pt \vbox \vbox \vbox x : B \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip E^{'} \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip w : A \vskip 2.0pt \nointerlineskip \lower -0.2ptto63.11897pt \xleaders \hrule \hfill \lower -0.2pt \vskip 2.0pt \nointerlineskip λ x w : B \to A \ignorespaces

\ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 46.48888 pt \vbox \vbox E \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip u : B \to A \vbox F \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip v : B \vskip 2.0pt \nointerlineskip \lower -0.2ptto92.27983pt \xleaders \hrule \hfill \lower -0.2pt \vskip 2.0pt \nointerlineskip u v : A \ignorespaces = \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 92.6833 pt \vbox \vbox \vbox \vbox x : B \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip E^{'} \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip w : A \vskip 2.0pt \nointerlineskip \lower -0.2ptto63.11897pt \xleaders \hrule \hfill \lower -0.2pt \vskip 2.0pt \nointerlineskip λ x w : B \to A \vbox F \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip v : B \vskip 2.0pt \nointerlineskip \lower -0.2ptto107.19876pt \xleaders \hrule \hfill \lower -0.2pt \vskip 2.0pt \nointerlineskip (λ x w) v : A \ignorespaces ⇝^{+} \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 71.86108 pt \vbox \vbox \vbox F \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip v : B \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip E^{'} [v / x] \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip w [v / x] : A \ignorespaces

\ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 46.48888 pt \vbox \vbox E \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip u : B \to A \vbox F \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip v : B \vskip 2.0pt \nointerlineskip \lower -0.2ptto92.27983pt \xleaders \hrule \hfill \lower -0.2pt \vskip 2.0pt \nointerlineskip u v : A \ignorespaces = \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 92.6833 pt \vbox \vbox \vbox \vbox x : B \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip E^{'} \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip w : A \vskip 2.0pt \nointerlineskip \lower -0.2ptto63.11897pt \xleaders \hrule \hfill \lower -0.2pt \vskip 2.0pt \nointerlineskip λ x w : B \to A \vbox F \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip v : B \vskip 2.0pt \nointerlineskip \lower -0.2ptto107.19876pt \xleaders \hrule \hfill \lower -0.2pt \vskip 2.0pt \nointerlineskip (λ x w) v : A \ignorespaces ⇝^{+} \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 71.86108 pt \vbox \vbox \vbox F \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip v : B \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip E^{'} [v / x] \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip w [v / x] : A \ignorespaces

\ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 24.57222 pt \vbox E \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip u : B \to A \ignorespaces ⇝^{+} \ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 24.57222 pt \vbox E^{'} \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip u^{'} : B \to A \ignorespaces

\ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 24.57222 pt \vbox E \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip u : B \to A \ignorespaces ⇝^{+} \ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 24.57222 pt \vbox E^{'} \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip u^{'} : B \to A \ignorespaces

\ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 24.41666 pt \vbox F \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip v : B \ignorespaces ⇝^{+} \ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 24.41666 pt \vbox F^{'} \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip v^{'} : B \ignorespaces

\ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 24.41666 pt \vbox F \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip v : B \ignorespaces ⇝^{+} \ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 24.41666 pt \vbox F^{'} \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip v^{'} : B \ignorespaces

\ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 46.48888 pt \vbox \vbox E \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip u : B \to A \vbox F \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip v : B \vskip 2.0pt \nointerlineskip \lower -0.2ptto92.27983pt \xleaders \hrule \hfill \lower -0.2pt \vskip 2.0pt \nointerlineskip u v : A \ignorespaces ⇝^{+} \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 46.48888 pt \vbox \vbox E^{'} \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip u^{'} : B \to A \vbox F \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip v : B \vskip 2.0pt \nointerlineskip \lower -0.2ptto91.04211pt \xleaders \hrule \hfill \lower -0.2pt \vskip 2.0pt \nointerlineskip u^{'} v : A \ignorespaces

\ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 46.48888 pt \vbox \vbox E \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip u : B \to A \vbox F \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip v : B \vskip 2.0pt \nointerlineskip \lower -0.2ptto92.27983pt \xleaders \hrule \hfill \lower -0.2pt \vskip 2.0pt \nointerlineskip u v : A \ignorespaces ⇝^{+} \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 46.48888 pt \vbox \vbox E^{'} \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip u^{'} : B \to A \vbox F \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip v : B \vskip 2.0pt \nointerlineskip \lower -0.2ptto91.04211pt \xleaders \hrule \hfill \lower -0.2pt \vskip 2.0pt \nointerlineskip u^{'} v : A \ignorespaces

\ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 46.48888 pt \vbox \vbox E \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip u : B \to A \vbox F \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip v : B \vskip 2.0pt \nointerlineskip \lower -0.2ptto92.27983pt \xleaders \hrule \hfill \lower -0.2pt \vskip 2.0pt \nointerlineskip u v : A \ignorespaces ⇝^{+} \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 46.48888 pt \vbox \vbox E \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip u : B \to A \vbox F^{'} \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip v^{'} : B \vskip 2.0pt \nointerlineskip \lower -0.2ptto91.04211pt \xleaders \hrule \hfill \lower -0.2pt \vskip 2.0pt \nointerlineskip u v^{'} : A \ignorespaces

\ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 46.48888 pt \vbox \vbox E \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip u : B \to A \vbox F \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip v : B \vskip 2.0pt \nointerlineskip \lower -0.2ptto92.27983pt \xleaders \hrule \hfill \lower -0.2pt \vskip 2.0pt \nointerlineskip u v : A \ignorespaces ⇝^{+} \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 46.48888 pt \vbox \vbox E \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip u : B \to A \vbox F^{'} \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip v^{'} : B \vskip 2.0pt \nointerlineskip \lower -0.2ptto91.04211pt \xleaders \hrule \hfill \lower -0.2pt \vskip 2.0pt \nointerlineskip u v^{'} : A \ignorespaces

\ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 24.41666 pt \vbox E \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip t : C \ignorespaces ⇝^{+} \ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 24.85316 pt \vbox E^{'} \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip t^{'} : C \ignorespaces

\ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 24.41666 pt \vbox E \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip t : C \ignorespaces ⇝^{+} \ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 24.85316 pt \vbox E^{'} \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip t^{'} : C \ignorespaces

Peer Reviews

No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.

Videos

No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.

Taxonomy

TopicsLogic, programming, and type systems · Polynomial and algebraic computation · Mathematics, Computing, and Information Processing

Full text

Natural Deduction and Normalization Proofs for the Intersection Type Discipline

Federico Aschieri

Institut für Logic and Computation

Technische Universität Wien Funded by FWF START project Y544–N23 and FWF P 32080–N31

Abstract

Refining and extending previous work by Retoré [8], we develop a systematic approach to intersection types via natural deduction. We show how a step of beta reduction can be seen as performing, at the level of typing derivations, Prawitz reductions in parallel. Then we derive as immediate consequences of Subject Reduction the main theorems about normalization for intersection types: for system ${\mathsf{D}}$ , strong normalization, for system ${\mathsf{D\Omega}}$ , the leftmost reduction termination for terms typable without $\Omega$ .

1 Introduction

One of the most remarkable properties of the intersection type systems ${\mathsf{D\Omega}}$ and ${\mathsf{D}}$ [3] is that they characterize the normalizable and strongly normalizable terms of $\lambda$ -calculus. In turn, this characterization allows to prove in a logically grounded and elegant way several fundamental theorems about $\lambda$ -calculus, like the uniqueness of normal forms and the termination of the leftmost redex reduction for normalizable terms [6]. Unfortunately, since they exploit normalization for ${\mathsf{D\Omega}}$ , the first intersection-types-based proofs of these results employed the Tait reducibility technique [6], very well known for not conveying any combinatorial information and for its logical complexity. Using reducibility to prove elementary theorems about $\lambda$ -calculus is definitely an overkill and the resulting proofs are so indirect that are barely comprehensible. For these reasons, we are interested here in giving an elementary, direct, conceptually elegant proof of normalization for ${\mathsf{D\Omega}}$ , which may be used in elementary introductions to typed and untyped $\lambda$ -calculus. With our approach, it will turn out, the most important elementary results of $\lambda$ -calculus can be proved as corollaries of the normalization theorem for simply typed $\lambda$ -calculus.

The first elementary, arithmetical proof of strong normalization for system ${\mathsf{D}}$ was provided by Retoré [8]; then several others followed (e.g. [2, 10, 4, 1]). The beauty of Retoré’s approach is that one sees that actually…there is nothing to prove. If one moves to a Prawitz-style natural deduction presentation of intersection types, instead of sticking to Gentzen-style natural deduction, as it is traditionally done [6], then strong normalization becomes just consequence of Subject Reduction and normalization for natural deduction. The reason is that Gentzen-style natural deduction is based on sequents and, as a typing system, uses explicit contexts. As a result, the proof reductions are quite cumbersome to write and nowhere near the elegance achievable using Prawitz natural deduction trees. In fact, the usual proofs of Subject Reduction [6] provide no direct transformation of the typing derivation of a term into the typing derivations of the reducts. Writing the transformation explicitly, indeed, would be ugly. But without doing that, one misses the logical perspective on intersection types.

Retoré treated directly only strict intersection types, that is, types not allowing conjunction on the right of implications. This limitation is not present in [7], but the approach is not as direct and simple as Retoré’s. Indeed, strong normalization for ${\mathsf{D}}$ is deduced from strong normalization of a more complex logical system, where judgements are sequences of sequents, like in hypersequent calculi. Since each proof of this system can be translated as a sequence of parallel natural deductions, its strong normalization can be derived.

The goal of this paper is to address these limitations and extend the natural deduction approach to the typing system ${\mathsf{D\Omega}}$ , while refining Retoré’s treatment of system ${\mathsf{D}}$ and removing the restriction to strict types. As corollaries, we shall obtain strong normalization for ${\mathsf{D}}$ and normalization for ${\mathsf{D\Omega}}$ . A similar program was outlined in [5], but never carried out in detail. Moreover, the suggested normalization argument for ${\mathsf{D\Omega}}$ is presented as standard cut-elimination technique, where one reduces at each step natural-deduction redexes of maximal complexity. This argument, however, is not suitable for proving termination of the leftmost reduction strategy for $\lambda$ -calculus. Achieving that requires subtle adjustments and carefully formulated inductive statements, and indeed none of the aforementioned natural-deduction-based works straightforwardly generalizes to ${\mathsf{D\Omega}}$ so that it can accomplish our goals.

2 Natural Deduction for Intersection Types

In this section we define a natural deduction presentation of Coppo-Dezani intersection type systems ${\mathsf{D}}$ and ${\mathsf{D\Omega}}$ . These systems were invented with the aim of providing a logical characterization of strongly normalizable and normalizable $\lambda$ -terms. Namely, the terms typable in ${\mathsf{D}}$ are exactly the strongly normalizable ones, while the terms typable in ${\mathsf{D\Omega}}$ are precisely the normalizable ones.

We shall start by presenting the type inference rules, then we define a reduction relation on typing derivations, which consists in applying Prawitz reductions in parallel to the corresponding natural deduction.

2.1 Typing Derivations

A typing tree is a tree whose nodes are expressions of the form $t:A$ , where $t$ is a $\lambda$ -term and $A$ is a type built from type variables and $\top$ , using the connectives $\rightarrow,\land$ . A typing tree $\mathcal{D}$ with root $t:A$ will be denoted as

$\mathcal{D}$

$t:A$

. With

$x:A$

$\mathcal{D}$

, we denote a typing tree such that for all leaves $x:A$ and $x:B$ , we have $A=B$ .

A typing derivation in system ${\mathsf{D\Omega}}$ is a typing tree obtained by means of the following inference rules.

[TABLE]

$t:A$ $t:B$

$t:A\land B$

[TABLE]

We observe that the only inference rule that requires a condition to be applied is the $\rightarrow$ -introduction rule. One can only conclude $\lambda x\,u:A\rightarrow B$ when there is a typing derivation $\mathcal{D}$ of $u:B$ such that all the occurrences of $x$ are declared of the same type $A$ . In general we allow variables to be declared of multiple types in the leaves of typing derivations, as polymorphism is the essence of intersection types. There is no special technical reason: we could very well have restricted variables to have unique types, but since there is no gain in doing this, we avoid the restriction.

By construction, if $x_{1}:A_{1},\dots,x_{n}:A_{n}$ , are all the leaves of a typing derivation $\mathcal{D}$ of $t:A$ such that $x_{1},\dots,x_{n}$ are free variables of $t$ , then $\mathcal{D}$ is isomorphic to a natural deduction of $A$ from assumptions $A_{1},\dots,A_{n}$ ; such a $\mathcal{D}$ will be called a typing derivation of $t:A$ from $x_{1}:A_{1},\dots,x_{n}:A_{n}$ . Not all natural deductions, of course, are isomorphic to typing derivations: the $\land$ -introduction can only be applied when the typing derivations of the premises type the same term.

As usual, ${\mathsf{D}}$ is the typing system obtained from ${\mathsf{D\Omega}}$ by dropping the rule

$t:\top$

. Moreover, we assume Barendregt’s convention: in any context, free variables are always different from bound variables, so that there is no risk of capturing free variables when substituting terms for variables, as in $\beta$ -reduction.

2.2 Reduction Relation on Typing Derivations

We now define the standard operation of derivation composition. With $\mathcal{D}[t/x]$ we shall denote the replacement of every occurrence of $x$ in $\mathcal{D}$ with the $\lambda$ -term $t$ . If

[TABLE]

are two typing trees, the tree

[TABLE]

denotes the typing tree obtained from $\mathcal{D}[t/x]$ by replacing each leaf

$t:A$

with the typing tree

$\mathcal{E}$

$t:A$

. Indeed, this operation is a correct composition of typing derivations.

Proposition 1 (Typing Derivation Composition).

Let

[TABLE]

be two typing derivations. Then

[TABLE]

is a typing derivation

Proof.

By straightforward induction on $\mathcal{D}$ . ∎

In Table 1, we axiomatically define a binary reduction relation $\rightsquigarrow$ on typing derivations. The lefthand-side derivations of the first two reductions are called respectively $\rightarrow$ -redexes and $\land$ -redexes. A typing derivation is $\land$ -normal if it does not contain $\land$ -redexes and it is normal if it is not in relation $\rightsquigarrow$ with any typing derivation.

From the logical point of view, the relation $\rightsquigarrow$ formalizes the operation of performing several Prawitz reduction steps in parallel on the natural deduction associated to the typing derivation. Namely, we interpret the $\land$ -introduction rule as a parallel composition of derivations. We remark that for the $\rightarrow$ -elimination rule we do not allow parallel reductions, but this is a minimalistic design choice, rather than a necessity. From the computational point of view, indeed, the relation $\rightsquigarrow$ is intended to formalize the exact amount of Prawitz reductions needed to type a single step of $\beta$ -reduction.

In the following we shall need the well-known notion of weak head reduction over $\lambda$ -terms.

Definition 1 (Weak Head Reduction).

For every $\lambda$ -term $t$ , we say that $t\mapsto t^{\prime}$ by weak head reduction if

[TABLE]

3 Subject Reduction

The goal of this section is to prove Subject Reduction for system ${\mathsf{D}}$ . We instead prove later a Subjection Reduction for system ${\mathsf{D\Omega}}$ , because in ${\mathsf{D\Omega}}$ we are only interested in the contraction of the leftmost redex.

Since the relation $\rightsquigarrow$ embodies a Prawitz-style transformation of natural deductions, it always terminates.

Proposition 2.

The reduction relation $\rightsquigarrow$ is strongly normalizing.

Proof.

It is straightforward to prove, by induction on $\mathcal{D}$ , that if $\mathcal{D}\rightsquigarrow\mathcal{D^{\prime}}$ , the natural deduction corresponding to $\mathcal{D}$ reduces in a certain number of steps to the natural deduction corresponding to $\mathcal{D}^{\prime}$ , using the standard Prawitz reductions for $\rightarrow$ and $\land$ . Therefore, the relation $\rightsquigarrow$ produces no infinite reduction path. ∎

Eliminating the useless $\land$ -redex from typing derivations restores an important property of the simply typed $\lambda$ -calculus: the only way to type a function with arrow type is by a $\rightarrow$ -introduction.

Proposition 3 (Introduce!).

Suppose $\mathcal{D}$ is a $\land$ -normal typing derivation of $\lambda x\,u:T\neq\top$ whose last rule is not an $\land$ -introduction. Then

[TABLE]

with $T=A\rightarrow B$ .

Proof.

We proceed by induction on $\mathcal{D}$ and by cases according to the last rule of $\mathcal{D}$ . We observe that the last rule cannot be a leaf nor an $\rightarrow$ elimination, because the conclusion of $\mathcal{D}$ is not a variable nor an application and $T\neq\top$ . Therefore, only two rules can be applied:

•

The last rule of $\mathcal{D}$ is a $\rightarrow$ -introduction. This is the thesis.

•

$\mathcal{D}=\ignorespaces\ignorespaces\ignorespaces\ignorespaces\leavevmode\lower 48.26999pt\hbox{\vbox{\vbox{\hbox{\hskip 25.56497pt\hbox{\hskip 4.0pt\hbox{$ \mathcal{E} $}\hskip 4.0pt}}\vskip 2.0pt\nointerlineskip\hbox{\hskip 0.0pt\lower-0.5pt\hbox{}\hbox{\vbox{\vskip 1.0pt}}\lower-0.5pt\hbox{}}\vskip 2.0pt\nointerlineskip\hbox{\hbox{\hskip 4.0pt\hbox{$ \lambda x,u:B_{1}\land B_{2} $}\hskip 4.0pt}}}\vskip 2.0pt\nointerlineskip\hbox{\hskip 0.0pt\lower-0.2pt\hbox{}\hbox to65.93552pt{\xleaders\hrule\hfill}\lower-0.2pt\hbox{}}\vskip 2.0pt\nointerlineskip\hbox{\hskip 10.3232pt\hbox{\hbox{\hskip 4.0pt\hbox{$ \lambda x,u:B_{i} $}\hskip 4.0pt}}}}}\ignorespaces$ , with $T=B_{i}$ . We show that this case is impossibile. Since $\mathcal{D}$ is $\land$ -normal, the last rule of $\mathcal{E}$ is not an $\land$ -introduction. But by induction hypothesis the last rule of $\mathcal{E}$ must be an $\rightarrow$ -introduction, which is a contradiction.

∎

We can now prove Subject Reduction in the usual way. The proof makes explicit the transformations that are implicit in the usual presentations of intersection types.

Theorem 1 (Subject Reduction for ${\mathsf{D}}$ ).

Suppose $\mathcal{D}$ is a typing derivation of $t:A$ in ${\mathsf{D}}$ . Then

[TABLE]

Proof.

By straightforward induction on $\mathcal{D}$ . ∎

4 Strong Normalization

As corollary of Subject Reduction we obtain strong normalization for system ${\mathsf{D}}$ .

Theorem 2 (Strong Normalization).

Suppose that $\mathcal{D}$ is a typing derivation of $t:A$ in ${\mathsf{D}}$ . Then $t$ is strongly normalizable.

Proof.

We proceed by induction on the longest reduction of $\mathcal{D}$ . If $t\mapsto t^{\prime}$ , then by Theorem 1 we obtain $\ignorespaces\ignorespaces\ignorespaces\leavevmode\lower 24.41666pt\hbox{\vbox{\hbox{\hskip 5.90273pt\hbox{\hskip 4.0pt\hbox{$ \mathcal{D} $}\hskip 4.0pt}}\vskip 2.0pt\nointerlineskip\hbox{\hskip 0.0pt\lower-0.5pt\hbox{}\hbox{\vbox{\vskip 1.0pt}}\lower-0.5pt\hbox{}}\vskip 2.0pt\nointerlineskip\hbox{\hbox{\hskip 4.0pt\hbox{$ t:A $}\hskip 4.0pt}}}}\ignorespaces\rightsquigarrow\ignorespaces\ignorespaces\ignorespaces\leavevmode\lower 24.85316pt\hbox{\vbox{\hbox{\hskip 4.51385pt\hbox{\hskip 4.0pt\hbox{$ \mathcal{D}^{\prime} $}\hskip 4.0pt}}\vskip 2.0pt\nointerlineskip\hbox{\hskip 0.0pt\lower-0.5pt\hbox{}\hbox{\vbox{\vskip 1.0pt}}\lower-0.5pt\hbox{}}\vskip 2.0pt\nointerlineskip\hbox{\hbox{\hskip 4.0pt\hbox{$ t^{\prime}:A $}\hskip 4.0pt}}}}\ignorespaces$ By induction hypothesis, $t$ is strongly normalizable. Since $t$ reduces only to strongly normalizable terms, it is strongly normalizable. ∎

5 Normalization by Leftmost Redex Reduction

Before proving normalization for system ${\mathsf{D\Omega}}$ , we need a standard fact about intersection types.

Proposition 4.

Suppose that $\mathcal{D}$ is an $\land$ -normal typing derivation of $x\,t_{1}\dots t_{n}:A\neq\top$ in ${\mathsf{D\Omega}}$ from $x_{1}:A_{1},\dots,x_{m}:A_{m}$ and the last rule of $\mathcal{D}$ is not an $\land$ -introduction. Then $A$ is a subformula of one among $A_{1},\dots,A_{m}$ .

Proof.

By induction on $\mathcal{D}$ and by cases according to the last rule of $\mathcal{D}$ . We must consider only the following cases.

•

$n=0$ and $\mathcal{D}=\ignorespaces\ignorespaces\leavevmode\lower 25.33998pt\hbox{\vbox{\hbox{\hskip 11.73888pt\hbox{\hskip 4.0pt\hbox{}\hskip 4.0pt}}\vskip 2.0pt\nointerlineskip\hbox{\hskip 0.0pt\lower-0.2pt\hbox{}\hbox to31.47777pt{\xleaders\hrule\hfill}\lower-0.2pt\hbox{}}\vskip 2.0pt\nointerlineskip\hbox{\hbox{\hskip 4.0pt\hbox{$ x:A_{i} $}\hskip 4.0pt}}}}\ignorespaces$ , with $x=x_{i}$ and $A=A_{i}$ . Then thesis is verified.

•

$\mathcal{D}=\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\leavevmode\lower 48.57222pt\hbox{\vbox{\hbox{\vbox{\hbox{\hskip 28.91214pt\hbox{\hskip 4.0pt\hbox{$ \mathcal{E} $}\hskip 4.0pt}}\vskip 2.0pt\nointerlineskip\hbox{\hskip 0.0pt\lower-0.5pt\hbox{}\hbox{\vbox{\vskip 1.0pt}}\lower-0.5pt\hbox{}}\vskip 2.0pt\nointerlineskip\hbox{\hbox{\hskip 4.0pt\hbox{$ x,t_{1}\dots t_{n-1}:B\rightarrow A $}\hskip 4.0pt}}}\hbox{\hskip 14.45377pt}\vbox{\hbox{\hskip 7.04346pt\hbox{\hskip 4.0pt\hbox{$ \mathcal{F} $}\hskip 4.0pt}}\vskip 2.0pt\nointerlineskip\hbox{\hskip 0.0pt\lower-0.5pt\hbox{}\hbox{\vbox{\vskip 1.0pt}}\lower-0.5pt\hbox{}}\vskip 2.0pt\nointerlineskip\hbox{\hbox{\hskip 4.0pt\hbox{$ t_{n}:B $}\hskip 4.0pt}}}}\vskip 2.0pt\nointerlineskip\hbox{\hskip 0.0pt\lower-0.2pt\hbox{}\hbox to115.69836pt{\xleaders\hrule\hfill}\lower-0.2pt\hbox{}}\vskip 2.0pt\nointerlineskip\hbox{\hskip 26.53584pt\hbox{\hbox{\hskip 4.0pt\hbox{$ x,t_{1}\dots t_{n-1},t_{n}:A $}\hskip 4.0pt}}}}}\ignorespaces$ . The last rule of $\mathcal{E}$ is not an $\land$ -introduction, therefore by induction hypothesis $B\rightarrow A$ must be a subformula of one among $A_{1},\dots,A_{m}$ , thus $A$ satisfies the thesis.

•

$\mathcal{D}=\ignorespaces\ignorespaces\ignorespaces\ignorespaces\leavevmode\lower 48.5pt\hbox{\vbox{\vbox{\hbox{\hskip 28.83891pt\hbox{\hskip 4.0pt\hbox{$ \mathcal{E} $}\hskip 4.0pt}}\vskip 2.0pt\nointerlineskip\hbox{\hskip 0.0pt\lower-0.5pt\hbox{}\hbox{\vbox{\vskip 1.0pt}}\lower-0.5pt\hbox{}}\vskip 2.0pt\nointerlineskip\hbox{\hbox{\hskip 4.0pt\hbox{$ x,t_{1}\dots t_{n}:B_{1}\land B_{2} $}\hskip 4.0pt}}}\vskip 2.0pt\nointerlineskip\hbox{\hskip 0.0pt\lower-0.2pt\hbox{}\hbox to72.48341pt{\xleaders\hrule\hfill}\lower-0.2pt\hbox{}}\vskip 2.0pt\nointerlineskip\hbox{\hskip 10.3232pt\hbox{\hbox{\hskip 4.0pt\hbox{$ x,t_{1}\dots t_{n}:B_{i} $}\hskip 4.0pt}}}}}\ignorespaces$ , with $A=B_{i}$ . Since $\mathcal{D}$ is $\land$ -normal, the last rule of $\mathcal{E}$ is not an $\land$ -introduction, therefore by induction hypothesis $B_{1}\land B_{2}$ must be a subformula of one among $A_{1},\dots,A_{m}$ , thus $B_{i}$ satisfies the thesis.

∎

We now prove the version of the Subject Reduction that we need for system ${\mathsf{D\Omega}}$ : by contracting the leftmost redex of a typable $\lambda$ -term $t$ , we induce a reduction of its typing derivation, provided $t$ is typable without $\top$ . Intuitively, the leftmost redex cannot be inside a subterm of $t$ having type $\top$ , the only case in which we would not have any transformation of the natural deduction associated to the typing derivation.

Lemma 3 (On the Left!).

Suppose that $\mathcal{D}$ is a $\land$ -normal typing derivation of $t:A\neq\top$ in ${\mathsf{D\Omega}}$ from $x_{1}:A_{1},\dots,x_{n}:A_{n}$ . Then:

If the last rule of $\mathcal{D}$ is not a $\land$ -introduction and $t\mapsto t^{\prime}$ by weak head reduction, then

[TABLE] 2. 2.

If $A_{1},\ldots,A_{n},A$ do not contain $\top$ and $t\mapsto t^{\prime}$ by leftmost redex reduction, then

[TABLE]

Proof.

We prove 1. and 2. simultaneously by induction on the size of $\mathcal{D}$ and by cases according to the last rule of $\mathcal{D}$ .

•

$\mathcal{D}=\ignorespaces\ignorespaces\leavevmode\lower 24.41666pt\hbox{\vbox{\hbox{\hskip 10.77425pt\hbox{\hskip 4.0pt\hbox{}\hskip 4.0pt}}\vskip 2.0pt\nointerlineskip\hbox{\hskip 0.0pt\lower-0.2pt\hbox{}\hbox to29.5485pt{\xleaders\hrule\hfill}\lower-0.2pt\hbox{}}\vskip 2.0pt\nointerlineskip\hbox{\hbox{\hskip 4.0pt\hbox{$ x:A $}\hskip 4.0pt}}}}\ignorespaces$ . This case is not possible, since $x$ does not reduce to any term.

•

$\mathcal{D}=\ignorespaces\ignorespaces\leavevmode\lower 24.47221pt\hbox{\vbox{\hbox{\hskip 8.4722pt\hbox{\hskip 4.0pt\hbox{}\hskip 4.0pt}}\vskip 2.0pt\nointerlineskip\hbox{\hskip 0.0pt\lower-0.2pt\hbox{}\hbox to24.94441pt{\xleaders\hrule\hfill}\lower-0.2pt\hbox{}}\vskip 2.0pt\nointerlineskip\hbox{\hbox{\hskip 4.0pt\hbox{$ t:\top $}\hskip 4.0pt}}}}\ignorespaces$ , with $A=\top$ . This case is not possible, since $A\neq\top$ by hypothesis.

•

$\mathcal{D}=\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\leavevmode\lower 69.1833pt\hbox{\vbox{\hbox{\hskip 15.82124pt\vbox{\vbox{\hbox{\hskip 4.0pt\hbox{$ x:B $}\hskip 4.0pt}\vskip 2.0pt\nointerlineskip\hbox{\hskip 0.0pt\lower-0.5pt\hbox{}\hbox{\vbox{\vskip 1.0pt}}\lower-0.5pt\hbox{}}\vskip 2.0pt\nointerlineskip\hbox{\hskip 6.4782pt\hbox{\hbox{\hskip 4.0pt\hbox{$ \mathcal{D}^{\prime} $}\hskip 4.0pt}}}}\vskip 2.0pt\nointerlineskip\hbox{\hskip 0.10751pt\lower-0.5pt\hbox{}\hbox{\vbox{\vskip 1.0pt}}\lower-0.5pt\hbox{}}\vskip 2.0pt\nointerlineskip\hbox{\hskip 0.10751pt\hbox{\hbox{\hskip 4.0pt\hbox{$ u:C $}\hskip 4.0pt}}}}}\vskip 2.0pt\nointerlineskip\hbox{\hskip 0.0pt\lower-0.2pt\hbox{}\hbox to61.77777pt{\xleaders\hrule\hfill}\lower-0.2pt\hbox{}}\vskip 2.0pt\nointerlineskip\hbox{\hbox{\hskip 4.0pt\hbox{$ \lambda x,u:B\rightarrow C $}\hskip 4.0pt}}}}\ignorespaces$ with $t=\lambda x\,u$ , $t^{\prime}=\lambda x\,u^{\prime}$ , $u\mapsto u^{\prime}$ and $A=B\rightarrow C$ . We observe that 1. is trivially true, since $t$ reduces to nothing by weak head reduction. Moving on to 2., we can apply the induction hypothesis to

$\mathcal{D}^{\prime}$

$u:C$

, since $B$ does not contain $\top$ according to the hypotheses. We thus obtain

[TABLE]

Therefore,

[TABLE]

•

$\mathcal{D}=\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\leavevmode\lower 46.48888pt\hbox{\vbox{\hbox{\vbox{\hbox{\hskip 16.69724pt\hbox{\hskip 4.0pt\hbox{$ \mathcal{E} $}\hskip 4.0pt}}\vskip 2.0pt\nointerlineskip\hbox{\hskip 0.0pt\lower-0.5pt\hbox{}\hbox{\vbox{\vskip 1.0pt}}\lower-0.5pt\hbox{}}\vskip 2.0pt\nointerlineskip\hbox{\hbox{\hskip 4.0pt\hbox{$ u:B\rightarrow A $}\hskip 4.0pt}}}\hbox{\hskip 14.45377pt}\vbox{\hbox{\hskip 7.5491pt\hbox{\hskip 4.0pt\hbox{$ \mathcal{F} $}\hskip 4.0pt}}\vskip 2.0pt\nointerlineskip\hbox{\hskip 0.0pt\lower-0.5pt\hbox{}\hbox{\vbox{\vskip 1.0pt}}\lower-0.5pt\hbox{}}\vskip 2.0pt\nointerlineskip\hbox{\hbox{\hskip 4.0pt\hbox{$ v:B $}\hskip 4.0pt}}}}\vskip 2.0pt\nointerlineskip\hbox{\hskip 0.0pt\lower-0.2pt\hbox{}\hbox to92.27983pt{\xleaders\hrule\hfill}\lower-0.2pt\hbox{}}\vskip 2.0pt\nointerlineskip\hbox{\hskip 27.9247pt\hbox{\hbox{\hskip 4.0pt\hbox{$ u,v:A $}\hskip 4.0pt}}}}}\ignorespaces$ , with $t=u\,v$ .

If $t\mapsto t^{\prime}$ by weak head reduction, either $u\mapsto u^{\prime}$ by weak head reduction and $t^{\prime}=u^{\prime}\,v$ , or $u=\lambda x\,w$ and $t^{\prime}=w[v/x]$ . In the first case, the last rule of $\mathcal{E}$ cannot be an $\land$ -introduction, so by induction hypothesis 1. we obtain

[TABLE]

therefore,

[TABLE]

which proves 1. and 2. In the second case, since $\mathcal{E}$ is by hypothesis $\land$ -normal, by Proposition 3,

[TABLE]

Therefore,

[TABLE]

which proves 1. and 2.

We can now assume that $t\mapsto t^{\prime}$ not by weak head reduction, thus we are left to prove 2. Since, $t$ has no head redex, $t=x\,t_{1}\dots t_{m}$ , with $u=x\,t_{1}\dots t_{m-1}$ and $v=t_{m}$ . By Proposition 4, $B\rightarrow A$ must be a subformula of some $A_{i}$ . Therefore $B\rightarrow A$ and $B$ do not contain $\top$ . Since $t^{\prime}=u^{\prime}\,v$ , with $u\mapsto u^{\prime}$ , or $t^{\prime}=u\,v^{\prime}$ , with $v\mapsto v^{\prime}$ , by induction hypothesis respectively

[TABLE]

or

[TABLE]

Therefore,

[TABLE]

or

[TABLE]

which is the thesis.

•

$\mathcal{D}=\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\leavevmode\lower 46.33331pt\hbox{\vbox{\hbox{\vbox{\hbox{\hskip 6.50061pt\hbox{\hskip 4.0pt\hbox{$ \mathcal{E} $}\hskip 4.0pt}}\vskip 2.0pt\nointerlineskip\hbox{\hskip 0.0pt\lower-0.5pt\hbox{}\hbox{\vbox{\vskip 1.0pt}}\lower-0.5pt\hbox{}}\vskip 2.0pt\nointerlineskip\hbox{\hbox{\hskip 4.0pt\hbox{$ t:C $}\hskip 4.0pt}}}\hbox{\hskip 14.45377pt}\vbox{\hbox{\hskip 6.75166pt\hbox{\hskip 4.0pt\hbox{$ \mathcal{F} $}\hskip 4.0pt}}\vskip 2.0pt\nointerlineskip\hbox{\hskip 0.0pt\lower-0.5pt\hbox{}\hbox{\vbox{\vskip 1.0pt}}\lower-0.5pt\hbox{}}\vskip 2.0pt\nointerlineskip\hbox{\hbox{\hskip 4.0pt\hbox{$ t:B $}\hskip 4.0pt}}}}\vskip 2.0pt\nointerlineskip\hbox{\hskip 0.0pt\lower-0.2pt\hbox{}\hbox to70.2917pt{\xleaders\hrule\hfill}\lower-0.2pt\hbox{}}\vskip 2.0pt\nointerlineskip\hbox{\hskip 11.64352pt\hbox{\hbox{\hskip 4.0pt\hbox{$ t:C\land B $}\hskip 4.0pt}}}}}\ignorespaces$ , with $A=C\land B$ . By hypothesis on $\mathcal{D}$ , 1. is trivially true, we thus prove 2. Since $C\land B$ does not contain $\top$ , also $C$ and $B$ do not contain $\top$ . Therefore by induction hypothesis 2., we get

[TABLE]

thus

[TABLE]

which proves 2.

•

$\mathcal{D}=\ignorespaces\ignorespaces\ignorespaces\ignorespaces\leavevmode\lower 48.15886pt\hbox{\vbox{\vbox{\hbox{\hskip 17.9006pt\hbox{\hskip 4.0pt\hbox{$ \mathcal{E} $}\hskip 4.0pt}}\vskip 2.0pt\nointerlineskip\hbox{\hskip 0.0pt\lower-0.5pt\hbox{}\hbox{\vbox{\vskip 1.0pt}}\lower-0.5pt\hbox{}}\vskip 2.0pt\nointerlineskip\hbox{\hbox{\hskip 4.0pt\hbox{$ t:B_{1}\land B_{2} $}\hskip 4.0pt}}}\vskip 2.0pt\nointerlineskip\hbox{\hskip 0.0pt\lower-0.2pt\hbox{}\hbox to50.6068pt{\xleaders\hrule\hfill}\lower-0.2pt\hbox{}}\vskip 2.0pt\nointerlineskip\hbox{\hskip 10.3232pt\hbox{\hbox{\hskip 4.0pt\hbox{$ t:B_{i} $}\hskip 4.0pt}}}}}\ignorespaces$ , with $A=B_{i}$ . We first observe that $t$ cannot start with $\lambda$ , otherwise, since $\mathcal{D}$ is $\land$ -normal and thus the last rule of $\mathcal{E}$ cannot be an $\land$ -introduction, by Proposition 3 we would obtain that the last rule of $\mathcal{E}$ is a $\rightarrow$ -introduction.

Now, if $t\mapsto t^{\prime}$ by weak head reduction, then by induction hypothesis 1., we get

[TABLE]

thus

[TABLE]

which proves 1. and 2. Therefore, we can assume that $t\mapsto t^{\prime}$ not by weak head reduction and we are left to prove 2. Since $t$ does not start with $\lambda$ , it has no head redex, thus $t=x\,t_{1}\dots t_{m}$ . By Proposition 4, applied to $\mathcal{E}$ , we obtain that $B_{1}\land B_{2}$ is a subformula of some among $A_{1},\dots,A_{n}$ , hence $B_{1}\land B_{2}$ cannot contain $\top$ . By induction hypothesis,

[TABLE]

and we obtain the thesis.

∎

We now prove that every term typable in ${\mathsf{D\Omega}}$ without $\top$ is normalizable by leftmost redex reduction. The natural deduction proof sheds new light on this fundamental result. Every reduction step contracting the leftmost redex is actually a combination of reduction steps at the level of the natural deduction corresponding to the typing derivation. When this natural deduction reaches normal form, the term is in normal form. We also remark that the subformula property must hold. Since the term is typable without $\top$ , the normal derivation is actually a derivation in system ${\mathsf{D}}$ ! This means that the subterms having type $\top$ are systematically erased.

Theorem 4 (Normalization by Leftmost Redex Reduction).

Suppose that $\mathcal{D}$ is a typing derivation of $t:A$ in ${\mathsf{D\Omega}}$ from $x_{1}:A_{1},\dots,x_{n}:A_{n}$ such that $A_{1},\ldots,A_{n},A$ do not contain $\top$ . Then the leftmost redex reduction of $t$ terminates.

Proof.

We proceed by induction on the longest reduction of $\mathcal{D}$ . We have that $\ignorespaces\ignorespaces\ignorespaces\leavevmode\lower 24.41666pt\hbox{\vbox{\hbox{\hskip 5.90273pt\hbox{\hskip 4.0pt\hbox{$ \mathcal{D} $}\hskip 4.0pt}}\vskip 2.0pt\nointerlineskip\hbox{\hskip 0.0pt\lower-0.5pt\hbox{}\hbox{\vbox{\vskip 1.0pt}}\lower-0.5pt\hbox{}}\vskip 2.0pt\nointerlineskip\hbox{\hbox{\hskip 4.0pt\hbox{$ t:A $}\hskip 4.0pt}}}}\ignorespaces\rightsquigarrow^{*}\ignorespaces\ignorespaces\ignorespaces\leavevmode\lower 24.41666pt\hbox{\vbox{\hbox{\hskip 5.13272pt\hbox{\hskip 4.0pt\hbox{$ \mathcal{D}^{\prime} $}\hskip 4.0pt}}\vskip 2.0pt\nointerlineskip\hbox{\hskip 0.0pt\lower-0.5pt\hbox{}\hbox{\vbox{\vskip 1.0pt}}\lower-0.5pt\hbox{}}\vskip 2.0pt\nointerlineskip\hbox{\hbox{\hskip 4.0pt\hbox{$ t:A $}\hskip 4.0pt}}}}\ignorespaces$ , where $\mathcal{D}^{\prime}$ is $\land$ -normal. If $t$ is normal we are done. If $t\mapsto t^{\prime}$ by leftmost redex reduction, by Lemma 3 we obtain $\ignorespaces\ignorespaces\ignorespaces\leavevmode\lower 24.41666pt\hbox{\vbox{\hbox{\hskip 5.13272pt\hbox{\hskip 4.0pt\hbox{$ \mathcal{D}^{\prime} $}\hskip 4.0pt}}\vskip 2.0pt\nointerlineskip\hbox{\hskip 0.0pt\lower-0.5pt\hbox{}\hbox{\vbox{\vskip 1.0pt}}\lower-0.5pt\hbox{}}\vskip 2.0pt\nointerlineskip\hbox{\hbox{\hskip 4.0pt\hbox{$ t:A $}\hskip 4.0pt}}}}\ignorespaces\rightsquigarrow^{+}\ignorespaces\ignorespaces\ignorespaces\leavevmode\lower 24.85316pt\hbox{\vbox{\hbox{\hskip 3.74387pt\hbox{\hskip 4.0pt\hbox{$ \mathcal{D}^{\prime\prime} $}\hskip 4.0pt}}\vskip 2.0pt\nointerlineskip\hbox{\hskip 0.0pt\lower-0.5pt\hbox{}\hbox{\vbox{\vskip 1.0pt}}\lower-0.5pt\hbox{}}\vskip 2.0pt\nointerlineskip\hbox{\hbox{\hskip 4.0pt\hbox{$ t^{\prime}:A $}\hskip 4.0pt}}}}\ignorespaces$ By induction hypothesis, the leftmost redex reduction of $t$ terminates, which yields the thesis. ∎

Bibliography10

The reference list from the paper itself. Each links out to its DOI / PubMed record.

1[1] F. Aschieri, Una caratterizzazione dei lambda termini non fortemente normalizzabili , Master Thesis, Università di Verona, 2007.
2[2] A. Bucciarelli, S. De Lorenzis, A. Piperno, I. Salvo, Some Computational Properties of Intersection Types , 14th Annual IEEE Symposium on Logic in Computer Science, Trento, pp. 109–118, 1999. 10.1109/LICS.1999.782598 . · doi ↗
3[3] M. Coppo, M. Dezani, A new type assignment for λ 𝜆 \lambda -terms , Arch. Math. Log., vol. 19, n. 1, pp. 139–156, 1978. 10.1007/BF 02011875 · doi ↗
4[4] R. David, Normalization without reducibility , Ann. Pure Appl. Logic, vol. 107, n. 1-3, pp. 121–130, 2001. 10.1016/S 0168-0072(00)00030-0 . · doi ↗
5[5] M. Dezani-Ciancaglini, E. Giovannetti, U. de’Liguoro, Intersection Types, λ 𝜆 \lambda -models, and Böhm Trees . Theories of Types and Proofs, 45–97, The Mathematical Society of Japan, Tokyo, Japan, 1998. 10.2969/msjmemoirs/00201 C 020 . · doi ↗
6[6] J.-L. Krivine, Lambda-calculus, types and models , Studies in Logic and Foundations of Mathematics, pp. 1–176, Masson, Paris, 1990.
7[7] E. Pimentel, S. Ronchi Della Rocca and L. Roversi, Intersection Types from a Proof-theoretic Perspective , Fundamenta Informaticae, vol. 121, n. 1–4, pp. 253–274, 2012. 10.3233/FI-2012-778 . · doi ↗
8[8] C. Retoré, A Note on Intersection Types , Rapport de Recherche, RR-2431, INRIA, 1994.

TL;DR

Contribution

Findings

Abstract

Peer Reviews

Videos

Taxonomy

Natural Deduction and Normalization Proofs for the Intersection Type Discipline

Abstract

1 Introduction

2 Natural Deduction for Intersection Types

2.1 Typing Derivations

2.2 Reduction Relation on Typing Derivations

Proposition 1** (Typing Derivation Composition).**

Proof.

Definition 1** (Weak Head Reduction).**

3 Subject Reduction

Proposition 2**.**

Proof.

Proposition 3** (Introduce!).**

Proof.

Theorem 1** (Subject Reduction for D{\mathsf{D}}D).**

Proof.

4 Strong Normalization

Theorem 2** (Strong Normalization).**

Proof.

5 Normalization by Leftmost Redex Reduction

Proposition 4**.**

Proof.

Lemma 3** (On the Left!).**

Proof.

Theorem 4** (Normalization by Leftmost Redex Reduction).**

Proof.

Proposition 1 (Typing Derivation Composition).

Definition 1 (Weak Head Reduction).

Proposition 2.

Proposition 3 (Introduce!).

Theorem 1 (Subject Reduction for ${\mathsf{D}}$ ).

Theorem 2 (Strong Normalization).

Proposition 4.

Lemma 3 (On the Left!).

Theorem 4 (Normalization by Leftmost Redex Reduction).