1
% Specification of agdaLight
2
% Author: Thierry Coquand
4
%\documentclass[12pt,a4paper]{amsart}
5
\documentclass[11pt]{article}
7
\newcommand{\mkbox}[1]{\ensuremath{#1}}
9
\newcommand{\pair}[1]{{\langle #1 \rangle}}
12
\newtheorem{theorem}{Theorem}[section]
13
\newtheorem{lemma}[theorem]{Lemma}
14
\newtheorem{corollary}[theorem]{Corollary}
15
\newtheorem{definition}[theorem]{Definition}
20
%\usepackage{isolatin1}
29
\newcommand{\evObj}[2]{\mkbox{#1{\downarrow}#2}}
30
\newcommand{\evTyp}[2]{\mkbox{#1{\uparrow}#2}}
31
\newcommand{\evPr}[2]{\mkbox{#1{\updownarrow}#2}}
33
%\documentstyle{article}
35
\setlength{\oddsidemargin}{0in} % so, left margin is 1in
36
\setlength{\textwidth}{6.27in} % so, right margin is 1in
37
\setlength{\topmargin}{0in} % so, top margin is 1in
38
\setlength{\headheight}{0in}
39
\setlength{\headsep}{0in}
40
\setlength{\textheight}{9.19in} % so, foot margin is 1.5in
41
\setlength{\footskip}{.8in}
43
% Definition of \placetitle
44
% Want to do an alternative which takes arguments
45
% for the names, authors etc.
47
\def\fin{\enspace\vbox{\hrule\hbox{\vrule\kern4pt
48
\vbox{\kern4pt\kern4pt}\kern4pt\vrule}\hrule}}
53
\def\FUN{\hbox{\sf Fun}}
56
\def\fun{\hbox{\sf fun}}
57
\def\SET{\hbox{\sf Set}}
58
\def\BSET{\hbox{\sf Bset}}
59
\def\EL{\hbox{\sf El}}
60
\def\PROOF{\hbox{\sf Prf}}
61
\def\NAT{\hbox{\sf Nat}}
62
\def\INTRO{\hbox{\sf intro}}
63
\def\ELIM{\hbox{\sf elim}}
64
\def\NATREC{\hbox{\sf natrec}}
65
\def\BOOLREC{\hbox{\sf boolrec}}
66
\def\LISTREC{\hbox{\sf listrec}}
67
\def\LIST{\hbox{\sf List}}
68
\def\ZERO{\hbox{\sf O}}
69
\def\SUCC{\hbox{\sf succ}}
70
\def\NIL{\hbox{\sf nil}}
71
\def\CONS{\hbox{\sf cons}}
72
\def\BOOL{\hbox{\sf Bool}}
73
\def\TRUE{\hbox{\sf true}}
74
\def\FALSE{\hbox{\sf false}}
75
\def\correct{\hbox{\sf correct}}
76
\def\fits{~\hbox{\sf fits}~}
77
\def\subtype{\sqsubseteq}
78
\def\fills{~\hbox{\sf fills}~}
80
\newcommand\object[1]{{<}#1{>}}
81
\newcommand\env[1]{(#1)}
82
\def\spec{\sqsubseteq}
84
\def\Undef{{\sf undef}}
85
\def\cont{\hbox {\sf cont}}
86
\newcommand\coerce[2]{#1/#2}
87
\def\implies{\Longrightarrow}
88
\def\tel{\hbox {\sf tel}}
89
\def\case{\hbox {\sf case}}
90
\def\data{\hbox {\sf data}}
91
\def\rec{\hbox {\sf rec}}
92
\def\val{\hbox {\sf val}}
94
\def\hd{\hbox{\sf hd}}
95
\def\tl{\hbox{\sf tl}}
96
\def\Pos{\hbox{\sf Pos}}
98
\def\nat{\hbox{\sf nat}}
99
\def\add{\hbox{\sf add}}
100
\def\Pt{\hbox{\sf Pt}}
102
\newcommand{\EnvDfn}[3]{\mkbox{#1+#2{=}#3}}
103
\newcommand{\EnvDcl}[4]{\mkbox{#1+#2{:}#3{=}#4}}
104
\newcommand{\EnvMty}{\mkbox{[]}}
107
\newcommand{\teq}[3]{\mkbox{#1=#2:#3}}
108
\newcommand{\subtyp}[2]{\mkbox{#1\sesubseteq #2}}
109
%\newcommand{\proj}[2]{\mkbox{\msf{proj}_{#1}#2}}
110
%\newcommand{\sig}[3]{\mkbox{<\!\!#1:#2\!\!>#3}}
111
\newcommand{\product}[3]{\{#1:#2\}#3}
112
\newcommand{\Adh}[1]{\bar{#1}}
113
\newcommand{\entails}{\vdash}
115
\newcommand{\covers}{\lhd}
116
\newcommand{\Cov}{\hbox{\sf Cov}}
117
\newcommand{\cover}{\lhd}
118
\def\cov{\hbox{\sf Cov}}
120
\newcommand{\arrow}{\mbox {$\rightarrow$}}
121
\newcommand{\inv}[1]{#1^{-1}}
122
\newcommand{\OO}{\hbox{\cal O}}
123
\newcommand{\MM}{\hbox{\cal M}}
124
\newcommand{\R}{\hbox{\bf R}}
125
\newcommand{\RR}{\hbox{\bf R}}
126
\newcommand{\LL}{\hbox{\bf L}}
127
\newcommand{\Type}{\hbox{\bf Type}}
128
\newcommand{\kind}{\hbox{\bf kind}}
129
\newcommand{\Sig}{\hbox{\bf Sig}}
130
\newcommand{\type}{\hbox{\bf type}}
131
\newcommand{\sig}{\hbox{\bf sig}}
132
\newcommand{\RType}{\hbox{\bf RType}}
133
\newcommand{\Kind}{\hbox{\bf Kind}}
135
%\newcommand{\nil}{\mbox{$<\!>$}}
136
%\newcommand{\abs}[1]{\mbox{$<\!#1\!>$}}
138
\newcommand{\nil}{\mbox{$\{\}$}}
139
\newcommand{\abs}[1]{\mbox{$\{#1\}$}}
140
\newcommand{\abst}[1]{\mbox{$\{\!|#1|\!\}$}}
141
%\newcommand{\lbr}{\lbrack\!\lbrack}
142
\newcommand{\lbr}{\mathopen{\lbrack\!\lbrack}}
143
%\newcommand{\rbr}{\rbrack\!\rbrack}
144
\newcommand{\rbr}{\mathopen{\rbrack\!\rbrack}}
145
%\newcommand{\sem}[1]{\mbox{$\lbr #1 \rbr$}}
146
%\newcommand{\sem}[1]{{\lbr #1 \rbr}}
147
%\newcommand{\typ}[1]{{(\!| #1 |\!)}}
148
\newcommand{\sem}[1]{#1}
149
\newcommand{\hypEl}[3]{#2{:}#3~[#1]}
150
\newcommand{\hypFa}[3]{#2{:}#3~[#1]}
151
\newcommand{\hypEq}[4]{#2=#3{:}#4~[#1]}
152
\newcommand{\hypSu}[3]{#2\subseteq #3~[#1]}
153
\newcommand{\hypTy}[2]{#2~\type~[#1]}
154
\newcommand{\hypKi}[2]{#2~\kind~[#1]}
155
\newcommand{\hypSi}[2]{#2~\sig~[#1]}
156
\newcommand{\typ}[1]{#1|}
157
\newcommand{\proj}[2]{\eta ~{#1}~{#2}}
158
\newcommand{\Fun}[2]{{\sf Fun}~{#1}~{#2}}
159
\newcommand{\Sum}[2]{{\sf Sum}~{#1}~{#2}}
160
\newcommand{\Elem}[1]{{\sf El}~{#1}}
161
\newcommand{\STAR}{*}
166
\title{Presentation of core agda}
168
\author{Thierry Coquand and Makoto Takeyama}
173
\section*{Introduction}
175
We present the typing system of core agda.
177
The syntax of the core version is the one of pure lambda-calculus with constants
178
$$ M ~::=~ n~|~M~M~|~\lambda x.M~~~~~~~~~~n~::=~x~|~f~|~c$$
180
There are two kind of constants: {\em primitive} $c$ or {\em defined} $f$. The definition
181
of $f$ may be {\em explicit}, of the form $f=M$, or {\em implicit}. It is then defined recursively
182
using pattern-matching equations.
184
We can define a priori $\beta,\iota$ conversion on terms.
186
The typing rules are essentially the one of Martin-L\"of Logical Framework.
187
The difference with his presentation is that substitution is taken as granted on
190
\section{The language}
192
Defined constants $f$ are defined by equations (computation rules) of the form
193
$$f~x_1~\dots~x_n~(c~y_1~\dots~y_k)\rightarrow M$$
195
$$f~{\bf x}~(c~{\bf y})\rightarrow M$$
197
Each constant has an arity $ar(f) = n+1,ar(c)=k$. We write $h,h',\dots$ for a constant $f$ or $c$
199
We define {\em conversion} to be the equality generated by the usual $\beta$ rules and
200
the computation rules for constants, called $\iota$ rules. It is standard that $\beta,\iota$
201
reduction is confluent. We write $M = N$ to say that $M$ and $N$ are convertible.
203
We assume given constants $\FUN,\SET,\EL$. We write $(x{:}A)\rightarrow B$ instead of
204
$\FUN~A~(\lambda x.B)$, and we write $A\rightarrow B$ for $\FUN~A~(\lambda x.B)$ if $x$
205
is not free in $B$. %Similarly we write $\lambda x{:}A.B$ for $\fun~A~(\lambda x.M)$.
206
We write $N(x=M)$ the result of substituting the free occurences of $x$ by $M$ in $N$
207
and may write it $N[M]$ if $x$ is clear from the context.
208
We consider terms up to $\alpha$-conversion.
210
\section{Typing rules}
212
We have three syntactical categories, for {\em types} $A,B,\dots$, for
213
{\em terms} $M,N,\dots$ and for {\em contexts} $\Gamma,\Delta,\dots$ We have
214
a special type $\SET$ of (data) types, i.e. primitive types given with
215
constructors. The syntax is
216
$$\begin{array}{lclr}
217
A & ::= & \SET~|~El~M~|~(x{:}A)\rightarrow A & types \\
218
M & ::= & x~|~M~M~|~\lambda x.M & terms \\
219
\Gamma & ::= & ()~|~\Gamma,x{:}A & contexts
222
There are five kinds of judgement $\Delta\vdash,~\Delta\vdash A,~\Delta\vdash M:A,~\Delta\vdash A_1=A_2$
223
and $\Delta\vdash M_1=M_2:A$.
224
The first $\Delta\vdash$ expresses that $\Delta$ is a correct context.
226
The typing rules are as follows:
229
{\em rules for contexts}
233
\frac{\Gamma\vdash~~~~~\Gamma\vdash A}{\Gamma,x{:}A\vdash}
236
{\em rules for types}
239
\frac{\Gamma\vdash}{\Gamma\vdash \SET}~~~~
240
\frac{\Gamma\vdash M:\SET}{\Gamma\vdash \EL~M}~~~~~~
241
\frac{\Gamma,x{:}A\vdash B}{\Gamma\vdash (x{:}A)\rightarrow B}
244
{\em rules for terms}
247
\frac{\Gamma\vdash~~~~~(x{:}A)~\in~\Gamma}{\Gamma\vdash x{:}A}~~~~~~~~~
248
\frac{\Gamma,x{:}A\vdash M:B}{\Gamma\vdash \lambda x.M:(x{:}A)\rightarrow B}~~~~~~
249
\frac{\Gamma\vdash M:(x{:}A)\rightarrow B~~~~\Gamma\vdash N:A}{\Gamma\vdash M~N:B(x=N)}
252
{\em conversion rule}
255
\frac{\Gamma\vdash M:A~~~~\Gamma\vdash A=B}{\Gamma\vdash M:B}
262
The general conversion rules are
265
\frac{\Gamma\vdash A}{\Gamma\vdash A=A}~~~~~~
266
\frac{\Gamma\vdash A=B}{\Gamma\vdash B=A}~~~~~~
267
\frac{\Gamma\vdash A=B~~~\Gamma\vdash B=C}{\Gamma\vdash A=C}
271
\frac{\Gamma\vdash M:A}{\Gamma\vdash M=M:A}~~~~~
272
\frac{\Gamma\vdash M=N:A}{\Gamma\vdash N=M:A}~~~~
273
\frac{\Gamma\vdash M=N:A~~~~\Gamma\vdash N=P:A}{\Gamma\vdash M=P:A}
277
\frac{\Gamma\vdash M=N:A~~~~~\Gamma\vdash A = B}
282
\frac{\Gamma,x{:}A\vdash B~~~~~\Gamma\vdash M_1=M_2:A}
283
{\Gamma\vdash B(x=M_1) = B(x=M_2)}
288
The last rule expresses
289
that a family of types depends in an extensional way of its argument.
290
It may be admissible, but it simplifies the metatheory to take
291
it as primitive. One could think
292
of including the substitution rule as well, for instance
293
the fact that $\Gamma\vdash B_1(x=M)=B_2(x=M)$
294
follows from $\Gamma\vdash M:A$ and $\Gamma,x{:}A\vdash B_1=B_2$.
296
below, the substitution rule is directly admissible. Furthermore, to include the substitution as a
297
rule may complicate some arguments, especially for proving {\em inversion} lemmas. It is
298
direct now that $\Gamma\vdash (x{:}A)\rightarrow B$ implies $\Gamma\vdash A$ and
299
$\Gamma,x{:}A\vdash B$. This would be a little more complicated to prove in presence of
302
The conversion rules for type theory are
305
\frac{}{\Gamma\vdash\SET=\SET}~~~~
306
\frac{\Gamma\vdash M_1=M_2:\SET}{\Gamma\vdash\EL~M_1=\EL~M_2}~~~~~~
307
\frac{\Gamma\vdash A_1=A_2~~~~~\Gamma,x{:}A_1\vdash B_1=B_2}{\Gamma\vdash (x{:}A_1)\rightarrow B_1 = (x{:}A_2)\rightarrow B_2}
311
\frac{\Gamma,x{:}A\vdash M_1=M_2:B}{\Gamma\vdash \lambda x.M_1=\lambda x.M_2:(x{:}A)\rightarrow B}
315
\frac{\Gamma,x{:}A\vdash B~~~~\Gamma\vdash N_1=N_2:(x{:}A)\rightarrow B~~~~\Gamma\vdash M_1=M_2:A}
316
{\Gamma\vdash N_1~M_1 = N_2~M_2:B(x=M_1)}
320
\frac{\Gamma,x{:}A\vdash N:B~~~~~\Gamma\vdash M:A}
321
{\Gamma\vdash (\lambda x.N)~M = N(x=M): B(x=M)}~~~~~~~
322
\frac{\Gamma\vdash A~~~~\Gamma\vdash M:(x{:}A)\rightarrow B}
323
{\Gamma\vdash M = \lambda x.M~x : (x{:}A)\rightarrow B}
326
In this presentation of rules, we consider $\lambda$ terms up to $\alpha$-conversion.
328
This system is quite close to the substitution calculus of P. Martin-L\"of. We note
329
however that the following judgement is derivable
331
A{:}\SET,P{:}A\rightarrow\SET\vdash \lambda x.\lambda x.x:(x{:}A)\rightarrow P~x\rightarrow P~x
333
while it is not in the substitution calculus (as noticed by R. Pollack).
337
If $\Gamma\vdash J$ then $\Gamma$ and all free variables of $J$ are declared in $\Gamma$.
340
In particular, if $\vdash A$ then $A$ is closed and if $\vdash M:A$ then both $M$ and
344
Notice that, because of the conversion rule, the strengthening property, stating that
345
$\Gamma\vdash J$ follows from $\Gamma,x{:}A\vdash J$ if $x$ is not free in $J$, is not
346
clear {\em a priori}. It will be a consequence of the normalisation property.
349
If $\sigma$ is a substitution we define $\Delta\vdash\sigma:\Gamma$ to mean that $\Delta\vdash x\sigma:A\sigma$ for
350
all $x{:}A$ in $\Gamma$
353
If $\Gamma\vdash J$ and $\Delta\vdash\sigma:\Gamma$ then $\Delta\vdash J\sigma$
357
We first prove the lemma in the case where $\sigma$ is a renaming by induction on
358
the proof of $\Gamma\vdash J$.
359
This contains {\em weakening}: if $\Gamma'\vdash$ and $x{:}A$ is in $\Gamma'$ whenever it is in
360
$\Gamma$ and if $\Gamma\vdash J$ then $\Gamma'\vdash J$. After weakening is proved, it is
361
direct to prove the lemma in the general case by induction on
362
the proof of $\Gamma\vdash J$.
367
If $\Gamma,x{:}A\vdash J$ and $\Gamma\vdash M:A$
368
then $\Gamma\vdash J(x=M)$.
374
If $\Gamma\vdash A=B$ then $\Gamma\vdash A$ and $\Gamma\vdash B$. If $\Gamma\vdash M_1=M_2:A$ then
375
$\Gamma\vdash M_1:A$ and $\Gamma\vdash M_2:A$. If $\Gamma\vdash M:A$
376
then $\Gamma\vdash A$. If
377
$\Gamma\vdash M=N:A$ then $\Gamma\vdash A$.
380
As a remark we can notice that the extensionality property for terms is derivable.
383
If $\Gamma,x{:}A\vdash N:B$ and $\Gamma\vdash M_1=M_2:A$ then
384
$\Gamma\vdash N(x=M_1) = N(x=M_2)\in B(x=M_1)$.
388
If $\Gamma\vdash (x{:}A_1)\rightarrow B_1=(x{:}A_2)\rightarrow B_2$ then $\Gamma\vdash A_1=A_2$
389
and $\Gamma,x{:}A_1\vdash B_1=B_2$.
392
We write $M\rightarrow M'$ if we get $M'$ from $M$ by one step of $\beta,\iota$ reduction.
394
\begin{corollary}\label{red}
395
If $\Gamma\vdash M:A$ and $M\rightarrow M'$ then $\Gamma\vdash M':A$
398
\begin{corollary}\label{conv}
399
If $\Gamma\vdash M:A$ and $\Gamma\vdash M':A$ and $M=M'$ then
400
$\Gamma\vdash M=M':A$
404
This is direct from Corollary \ref{red} and the Church-Rosser property of
405
$\beta,\iota$ reduction.
408
We have also a notion of signature $\Sigma$ which is a list of type declaration
409
$f:A$ or $c:A$. If $h:A$ is in the signature we should add the rule
411
\frac{}{\Gamma\vdash h:A}
414
Any type is of the form $(x_1{:}A_1)\rightarrow\dots\rightarrow (x_n{:}A_n)\rightarrow \SET$
415
or $(x_1{:}A_1)\rightarrow\dots\rightarrow (x_n{:}A_n)\rightarrow \EL~M$. We write it
416
$\Delta\rightarrow\SET$ or $\Delta\rightarrow\EL~M$ where $\Delta$ is the context
417
$x_1{:}A_1,\dots,x_n{:}A_n$. Similarly we may write $\lambda\Delta.M$ instead of
418
$\lambda x_1.\dots.\lambda x_n.M$.
420
We have an alternative presentation for typing terms and infering the types with rules
423
\frac{(x{:}A)~\in~\Gamma}{\Gamma\vdash x\downarrow A}~~~~~~~~~
424
\frac{\Gamma\vdash M\downarrow (x{:}A)\rightarrow B~~~~\Gamma\vdash N\uparrow A}
425
{\Gamma\vdash M~N\downarrow B(x=N)}
429
\frac{\Gamma,x{:}A\vdash M\uparrow B}{\Gamma\vdash \lambda x.M\uparrow (x{:}A)\rightarrow B}~~~~
430
\frac{\Gamma\vdash M\downarrow A~~~~\Gamma\vdash A = B}{\Gamma\vdash M\uparrow B}
433
The rules for types can then be replaced by
435
\frac{}{\Gamma\vdash \SET\downarrow}~~~~
436
\frac{\Gamma\vdash M\downarrow\SET}{\Gamma\vdash \EL~M\downarrow}~~~~~~
437
\frac{\Gamma\vdash A\downarrow~~~~~\Gamma,x{:}A\vdash B\downarrow}{\Gamma\vdash (x{:}A)\rightarrow B\downarrow}
439
%and the rules for checking contexts are
441
%\frac{\Gamma\downarrow~~~~\Gamma\vdash A\downarrow}{\Gamma,x{:}A\downarrow}
444
If $M$ is in $\beta$-normal form and $\Gamma\vdash M{:}A$ then $\Gamma\vdash M\uparrow A$.
450
We assume given a model $\DD$ with a subset $E\subseteq \DD$ of {\em existing} elements.
451
We may write $\Ex~u$ for $u\in E$.
452
We have an interpretation
453
$M\rho\in\DD$ for each environment $\rho:V\rightarrow\DD$.
454
If ${\bf u}$ is a sequence of elements
455
$u_1,\dots,u_k$ we write $\Ex~{\bf u}$ for $u_1\in E\wedge\dots\wedge u_k\in E$. If ${\bf u}$
456
and ${\bf v}$ are sequences of the same length $u_1,\dots,u_k$ and $v_1,\dots,v_k$
457
we write ${\bf u} = {\bf v}$ for $u_1=v_1,\dots,u_k=v_k$.
458
We assume that we have an interpretation $h\in\DD$ for each constant $h$ in the signature.
463
$f~{\bf u}~(c~{\bf v}) = M({\bf x} = {\bf u},{\bf y}={\bf v})$ if $\Ex~{\bf u}$ and $\Ex~{\bf v}$
464
and $f~{\bf x}~(c~{\bf y}) = M$
468
$(\lambda x.M)\rho~u = M(\rho,x=u)$ if $\Ex~u$
472
$\Ex~(c~{\bf u})$ if $\Ex~{\bf u}$
480
$(M~N)\rho = M\rho~(N\rho)$
484
$M(x=N)\rho = M(\rho,x=N\rho)$
488
$M\rho = M\nu$ if $\rho(x) = \nu(x)$ for all free variables $x$ of $M$
492
We assume also that we have a special element $\TOP\in\DD$ such that
500
$\TOP~u = \TOP$ if $\Ex~u$
504
$f~{\bf u}~\TOP = \TOP$ whenever $\Ex~{\bf u}$.
511
%If $\Ex~(M\rho)$ and $M\rightarrow M'$ then $M\rho = M'\rho$ in $\DD$.
512
%If $M=N$ and $\Ex~(M\rho)$ and $\Ex~(N\rho)$ then $M\rho = N\rho$ in $\DD$.
515
A {\em totality} on $\DD$
516
is a PER, partial equivalence relation, on $\DD$, that is a subset $X\subseteq \DD$ with
517
an equivalence relation $=_X$, such that $\Ex~u$ if $u\in X$ and $\nabla\in X$. We write
518
$u_1=u_2\in X$ instead of $u_1=_X u_2$.
519
We let $\TOT$ be the collection of all totality.
522
If $X\in\TOT$ is a totality and $F:X\rightarrow\TOT$ such that
523
$F(u_1)=F(u_2)$ if $u_1= u_2\in X$ we define $\Pi(X,F)$ to be the set
524
$ \{v\in\DD~|~u_1= u_2\in X\Rightarrow v~u_1 = v~u_2\in {F(u_1)}\}$
525
with the equivalence relation $v_1{=}v_2\in {\Pi(X,F)}$ iff $v_1~u{=}~ v_2~u\in {F(u)}$ for
526
all $u\in X.$ Then $\Pi(X,F)$ is a totality.
530
We have $\nabla\in X$. If $v\in\Pi(X,F)$ then $v~\nabla\in F(\nabla)$ and so $\Ex~(v~\nabla)$ and
531
$\Ex~v$ holds. If $u\in X$ then $\Ex~u$ so that $\nabla~u =\nabla\in F(u)$. This shows $\nabla\in \Pi(X,F)$.
534
We assume give a totality $S\in\TOT$ together with a function $Y:S\rightarrow\TOT$ which
535
is {\em extensional}, that is such that $Y(s_1) = Y(s_2)$ if $s_1= s_2\in S$
538
We define now $T\in\TOT$ and an extensional function $X{:}T\rightarrow\TOT$.
542
(1) $\SET=\SET\in T$ and $X(\SET) = S$
546
(2) $\FUN~U_1~F_1 = \FUN~U_2~F_2\in T$ if $U_1=U_2\in T$ and $F_1~u_1=F_2~u_2\in T$ whenever $u_1=u_2\in X(U_1)$. We
547
define then $X(\FUN~U_1~F_1)=X(\FUN~U_2~F_2)$ to be $\Pi(X(U_1),\lambda u.X(F_1~u))$
551
(3) $\EL~u_1=\EL~u_2\in T$ if $u_1=u_2\in S$ and $X(\EL~u_1) = X(\EL~u_2) = Y(u_1)$
555
If $\Delta$ is a context $x_1{:}A_1,\dots,x_k{:}A_k$ we write $\rho\Vdash\Delta$ to
556
express that $A_i\rho\in\TOT$ and $\rho(x_i)\in X(A_i\rho)$ for $i=1,\dots,k$ and
557
we write $\rho_1=\rho_2\Vdash\Delta$ to express that $A_i\rho_1=A_i\rho_2$ and
558
$x_i\rho_1 = x_i\rho_2\in A_i\rho_1$ for $i=1,\dots,k$.
560
For the next theorem, we assume $A\rho\in T$ and $h\in X(A\rho)$ for all
561
constant $h{:}A$ in the given signature $\Sigma$.
564
If $x$ is not declared in $\Delta$ and all the free variables of $A$ are declared
565
in $\Delta$ and $\rho\Vdash\Delta$ and $A\rho\in T$ and $u\in X(A\rho)$ then
566
$(\rho,x=u)\Vdash \Delta,x{:}A$.
569
The next result states the soundness of PER semantics for the type system.
571
\begin{theorem}\label{sem}
572
Assume $\rho_1=\rho_2\Vdash\Delta$. If $\Delta\vdash A$ then $A\rho_1=A\rho_2\in T$. If
573
$\Delta\vdash M{:}A$ then $A\rho_1=A\rho_2\in T$ and $M\rho_1=M\rho_2\in X(A\rho_1)$.
577
If $\vdash A$ then $\Ex~A()$. If $\vdash M:A$ then $\Ex~M()$.
581
\section{Strong normalisation and decidability of equality}
583
If we specialise Corollary \ref{sem} to the strict filter domain, we get
586
If $\vdash A$ then $A$ is strongly normalisable. If $\vdash M:A$ then $M$
587
is strongly normalisable.
590
In order to get decidability of conversion, we first define the $\eta$-expansion
591
$\eta~A~M$ in a syntactical way.
594
\eta~(\EL~M')~M = M~~~~
595
\eta~(\FUN~A~F)~M = \lambda x.\eta~(F~(\eta~A~x))~(M~(\eta~A~x))
598
\begin{lemma}\label{exp}
599
If $\Gamma\vdash M:A$ then $\Gamma\vdash M = \eta~A~M:A$
603
This is clear if $A$ is $\SET$ or of the form $\EL~M'$ because in this case
604
$\eta~A~M = M$ and $\Gamma\vdash M:A$ implies $\Gamma\vdash M = M :A$.
606
If $A$ is $(x{:}B)\rightarrow C$ then we have
607
$\eta~A~M = \lambda x.\eta~(C[\eta~B~x])~(M~(\eta~B~x))$. We have $\Gamma,x:B\vdash M~x:C$.
608
By induction on $A$ we have furthermore
609
$\Gamma,x:B\vdash x = \eta~B~x:B$ and so $\Gamma,x:B\vdash C = C[\eta~B~x]$ and
610
hence $\Gamma\vdash A = (x:B)\rightarrow C[\eta~B~x]$ and
611
$\Gamma,x:B\vdash M~x = M~(\eta~B~x):C[\eta~B~x].$ By induction on $A$
613
$$\Gamma,x:B\vdash M~x = \eta~(C[\eta~B~x])~(M~(\eta~B~x)):C[\eta~B~x]$$
615
$$\Gamma\vdash \lambda x.M~x = \lambda x.\eta~(C[\eta~B~x])~(M~(\eta~B~x)):(x:B)\rightarrow C[\eta~B~x]$$
616
Since $\Gamma\vdash A = (x:B)\rightarrow C[\eta~B~x]$ we deduce
617
$$\Gamma\vdash \lambda x.M~x = \lambda x.\eta~(C[\eta~B~x])~(M~(\eta~B~x)):A$$
618
and since $\Gamma\vdash M = \lambda x.M~x:A$ we have finally
619
$\Gamma\vdash M = \eta~A~M:A$ \end{proof}
621
We recall that $M_1=M_2$ means that $M_1$ and $M_2$ are $\beta,\iota$ convertible.
622
The intuition between the next statement is clear: if we work with the $\eta$ expansion
623
of the terms, we don't need the $\eta$ rule. For a precise proof, we rely on
624
the soundness of a particular PER model for our type system.
626
\begin{lemma}\label{betaiota}
627
If $\vdash M_1=M_2:A$ then $\eta~A~M_1 = \eta~A~M_2$
631
For the proof we use the following PER model. The domain $D$ is the set of all terms, with
632
$\beta,\iota$-conversion as equality. The PER $\SET$ is interpreted by the conversion: we
633
have $M_1=M_2:\SET$ iff $M_1=M_2$, and for any $M$ the PER $\EL~M$ is also the conversion.
634
We can then define $A_1=A_2$ and if it is the case when we have $M_1=M_2\in A_1$.
635
This is the case if $A_1=A_2=\SET$ or $A_1=A_2=\EL~M$ for some $M$ or
636
if $A_1=(x:B_1)\rightarrow C_1,~A_2=(x:B_2)\rightarrow C_2$ and $B_1 = B_2$
637
and $M_1=M_2\in B_1$ implies $C_1[M_1] = C_2[M_2]$.
638
For instance all terms are in $\SET\rightarrow\SET$ but we have
639
$f=\lambda x.f~x\in\SET\rightarrow\SET$, and not all terms are
640
in $(\SET\rightarrow\SET)\rightarrow\SET$.
642
$N_1=N_2\in (x:B_1)\rightarrow C_1$ iff $M_1=M_2\in B_1$ implies
643
$N_1~M_1=N_2~M_2\in C_1[M_1]$.
644
We then show by induction that if $A$ is a type that
648
$\eta~A~M$ is of type $A$ for any $M$
652
$M_1=M_2\in A$ iff $\eta~A~M_1=\eta~A~M_2$
656
By interpretation in this model we have that if $\vdash M_1=M_2:A$ then $A$
657
is a type and $M_1=M_2\in A$. This is equivalent to $\eta~A~M_1=\eta~A~M_2$.
661
In presence of constant, we interpret $h$ by $\eta~A~h$ if $h$ is declared of type
662
$A$. If $h=f$ is a defined constant, we need then to check that $\eta~A~f$ satisfies
663
the same equality as $f$. For instance, we have
664
(to simplify the notations, we write simply $X$ instead of $\EL~X$ if $X:\SET$)
666
\NATREC:(C{:}\NAT\rightarrow\SET)\rightarrow C~\ZERO\rightarrow ((n{:}\NAT)\rightarrow C~n~\rightarrow C~(\SUCC~n))
667
\rightarrow (n{:}\NAT)\rightarrow C~n
671
\NATREC~C~a~b~(\SUCC~n) = b~n~(\NATREC~C~a~b)
673
The $\eta$-expanded form of $\NATREC$ is
674
$$\NATREC^*=\lambda C.\lambda a.\lambda b.\lambda n.\NATREC~(\lambda x.C~x)~a~(\lambda x.\lambda y.b~x~y)~n$$
675
and we can check that we have
678
\NATREC^*~C~a~b~(\SUCC~n) & = & \NATREC~(\lambda x.C~x)~a~(\lambda x.\lambda y.b~x~y)~(\SUCC~n) \\
679
& = & b~n~(\NATREC~(\lambda x.C~x)~a~(\lambda x.\lambda y.b~x~y)~n) \\
680
& = & b~n~(\NATREC^*~C~a~b~n)
687
If $\vdash M_1:A$ and $\vdash M_2:A$ then $\vdash M_1=M_2:A$ iff
688
$\eta~A~M_1=\eta~A~M_2$
692
This follows from Lemmas \ref{exp} and \ref{betaiota} and Corollary \ref{conv}.
696
Assume $\Delta\vdash M_1:A$ and $\Delta\vdash M_2:A$. We have $\Delta\vdash M_1=M_2:A$ iff
697
$\eta~(\Delta\rightarrow A)~(\lambda\Delta.M_1)=\eta~(\Delta\rightarrow A)~(\lambda\Delta.M_2)$
701
We have $\Delta\vdash M_1=M_2:A$ iff $\vdash \lambda\Delta.M_1 = \lambda\Delta.M_2:\Delta\rightarrow A$.
705
If $A$ is in $\beta$-normal form then $\vdash A$ is decidable. If $\vdash A$ and $M$ is
706
in $\beta$-normal form then $\vdash M:A$ is decidable.
709
\section{Representation of type theory}
711
We add the primitive constants
713
\BOOL:\SET,~~~~\NAT:\SET,~~~~\LIST:\SET\rightarrow\SET,~~~~\TRUE:\BOOL,~~~~\FALSE:\BOOL,~~~
714
\ZERO:\NAT,~~~~\SUCC:\NAT\rightarrow\NAT
716
It is convenient to give the typing rules
718
\frac{\Gamma\vdash A:\SET}{\Gamma\vdash \NIL:\EL~(\LIST~A)}~~~~~~~
719
\frac{\Gamma\vdash A:\SET}{\Gamma\vdash \CONS:\EL~A\rightarrow \EL~(\LIST~A)\rightarrow \EL~(\LIST~A)}
721
We add also $\BOOLREC,\NATREC,\LISTREC$ with computation rules
724
\BOOLREC~C~a~b~\TRUE = a & & \BOOLREC~C~a~b~\FALSE = b \\
725
\NATREC~C~a~b~\ZERO = a & & \NATREC~C~a~b~(\SUCC~n) = b~n~(\NATREC~C~a~b~n) \\
726
\LISTREC~A~C~a~b~\NIL = a & & \LISTREC~A~C~a~b~(\CONS~x~xs) = b~x~xs~(\LISTREC~A~C~a~b~xs)
732
\BOOLREC:& & (C{:}\BOOL\rightarrow\SET)\rightarrow C~\TRUE\rightarrow C~\FALSE
733
\rightarrow (b{:}\BOOL)\rightarrow C~b \\
734
\NATREC:& & (C{:}\NAT\rightarrow\SET)\rightarrow C~\ZERO\rightarrow ((n{:}\NAT)\rightarrow C~n~\rightarrow C~(\SUCC~n))
735
\rightarrow (n{:}\NAT)\rightarrow C~n \\
736
\LISTREC:& & (A:\SET)\rightarrow (C{:}\LIST~A\rightarrow\SET)\rightarrow \\
737
& & C~\NIL\rightarrow ((x{:}A)\rightarrow (xs:\LIST~A)\rightarrow C~xs~\rightarrow C~(\CONS~x~xs)) \rightarrow \\
738
& & (xs{:}\LIST~A)\rightarrow C~xs
744
In this system, we show that the constants $\BOOLREC,\NATREC,\LISTREC$ are total.
747
If $A$ is in $\beta$-normal form then $\vdash A$ is decidable. If $\vdash A$ and $M$ is
748
in $\beta$-normal form then $\vdash M:A$ is decidable.
751
\section{A simple module system}
753
As a simple module system, we can take contexts as interface. We have the typing rules
755
\frac{\Gamma,x:A\vdash\Delta}{\Gamma\vdash x:A,\Delta}
758
\frac{\Gamma\vdash M:A~~~~~~\Gamma\vdash {\bf M}:\Delta(x=M)}
759
{\Gamma\vdash M,{\bf M}:(x:A,\Delta)}
762
If we have $\Gamma\vdash {\bf M}:\Delta$ we can extend the context $\Gamma$ to
763
$\Gamma,\Delta$. Intuitively, we hide the definitions of the variables declared
764
in $\Delta$, but we still have access to their types.
766
This a simple, but robust, notion of modular construction of terms.
768
\section{Defined constants}
770
A {\em small} type is a type which does not contain $\SET$. If $\Delta\vdash A$
771
and $A$ is a small type, we can always introduce a new primitive constant
772
$c:\Delta\rightarrow\SET$ such that $c~{\bf M}$ is ``equivalent'' to $A[{\bf M}]$ if
773
${\bf M}$ is an instance of $\Delta$. We introduce also two constants
775
\frac{\Gamma\vdash {\bf M}:\Delta~~~~~\Gamma\vdash N:A[{\bf M}]}{\Gamma\vdash \INTRO~N:c~{\bf M}}~~~~
776
\frac{\Gamma\vdash {\bf M}:\Delta~~~~~\Gamma\vdash P:c~{\bf M}}{\Gamma\vdash \ELIM~P:A[{\bf M}]}
778
with the computation rule $\ELIM~(\INTRO~N) = N$.
780
This is an example of a uniform extension of the Logical Framework in a way that
781
preserves strong normalisation. A special case is the addition of a $\Pi$ operation
783
is the context $X:\SET,Y:\EL~A\rightarrow\SET$ and $A$ is $(x{:}\EL~X)\rightarrow\EL~(Y~x)$.
785
\section{Sigma types}
787
We can extend the Logical Framework with sigma types. The proofs of strong normalisation
788
and decidability of type-checking extend without problems.
790
The new typing rules are
792
\frac{\Gamma,x{:}A\vdash B}{\Gamma\vdash (x{:}A)\times B}~~~~~~~
793
\frac{\Gamma\vdash M:A~~~~~\Gamma\vdash N:B(x=M)}{\Gamma\vdash M,N:(x{:}A)\times B}~~~
794
\frac{\Gamma\vdash P:(x{:}A)\times B}{\Gamma\vdash P.1:A}~~~
795
\frac{\Gamma\vdash P:(x{:}A)\times B}{\Gamma\vdash P.2:B(x=P.1)}
797
and the new conversion rules are
799
\frac{\Gamma\vdash A_1=A_2~~~~~\Gamma,x{:}A_1\vdash B_1=B_2}
800
{\Gamma\vdash (x{:}A_1)\times B_1 = (x{:}A_2)\times B_2}
803
\frac{\Gamma,x:A\vdash B~~~\Gamma\vdash M_1=M_2:A~~~~~\Gamma\vdash N_1=N_2:B(x=M_1)}
804
{\Gamma\vdash (M_1,N_1) = (M_2,N_2):(x:A)\times B}$$
806
\frac{\Gamma\vdash M:A~~~~~\Gamma\vdash N:B(x=M)}
807
{\Gamma\vdash (M,N).1 = M:A}$$
809
\frac{\Gamma,x:A\vdash B~~~~\Gamma\vdash M:A~~~~~\Gamma\vdash N:B(x=M)}
810
{\Gamma\vdash (M,N).2 = N:B(x=M)}$$
812
\frac{\Gamma\vdash P:(x{:}A)\times B}{\Gamma\vdash P = (P.1,P.2):(x{:}A)\times B}
815
The types are interfaces and can be thought of as (generalised) context. We need a system
816
of pattern notations, so that we can write
817
$\lambda (x,y).M:((x:A)\times B)\rightarrow C$ if $x{:}A,y{:}B\vdash M:C$.
818
When we instanciate a given interface $x_1{:}A_1,\dots,x_k{:}A_k$ by elements
819
$M_1,\dots,M_k$ the typing rules are that $M_i:A_i[M_1,\dots,M_{i-1}]$. Intuitively,
820
during the instantiation we have access to the values of $x_1,\dots,x_k$. But
821
these values are hidden outside the module.
825
In order to represent the collection of all ``Bishop'' sets (sets with an equivalence
826
relation), we can introduce a new type $\SET_1$, with a new type forming operation
827
$$\frac{\Gamma\vdash M:\SET_1}{\Gamma\vdash \EL_1~M}$$
828
In combination with sigma types, and defined constants, one can then represent
829
for instance the collection of all Bishop sets as a constant
830
$\BSET:\SET_1$ with rules
832
\frac{\Gamma\vdash A:\SET~~~~\Gamma\vdash R:A\rightarrow A\rightarrow\SET~~~~
833
\Gamma\vdash M:equiv~A~R}
834
{\Gamma\vdash \INTRO~(A,R,M):\BSET}
837
\frac{\Gamma\vdash P:\BSET}
838
{\Gamma\vdash \ELIM~P:(A{:}\SET)\times (R{:}A\rightarrow A\rightarrow\SET)\times equiv~A~R}
841
In this way, we keep the structure of the types close to simple type
842
theory. The new atomic types are of the form $\SET_1$ or $\EL_1~M$.
844
\section{Extension with bar recursion}
846
Using the filter domain model for strong normalisation, it can be shown, using
847
impredicative means, that the constant for bar recursion, or for modified
848
bar recursion are totals.
850
We write $a:l$ for $\CONS~a~l$
851
We define $\lambda l.|l|:\LIST~A\rightarrow \NAT$, and $\hat{l}:\NAT\rightarrow A$ if $l:\LIST~A$
853
$|\NIL| = \ZERO~~~~~~|a:l| = \SUCC~|l|$
855
$\NIL:x = x:\NIL~~~~~~~(a:l):x = a:(l:x)$
857
$\widehat{\NIL}~n = \ZERO~~~~~~~\widehat{a:l}~\ZERO = a~~~~~\widehat{a:l}~(\SUCC~n) = \widehat{l}~n$
859
We introduce then $\Phi,\Psi$ with the equations
861
$\Phi~y~g~h~s = \Psi~y~g~h~s~(y~|s|<\hat{s})$
863
$\Psi~y~g~h~s~\TRUE = g~s$
865
$\Psi~y~g~h~s~\FALSE = h~s~(\lambda x.\Phi~y~g~h~(s:x))$
869
$y:(\NAT\rightarrow A)\rightarrow\NAT$
871
$h:\LIST~ A\rightarrow (A\rightarrow B)\rightarrow B$
873
$g:\LIST~A\rightarrow B$
875
It can then be shown that $\Phi,\Psi$ are total.
877
\section{Proof irrelevance}
879
We add two new constants $\PROOF$ and $\ZERO$ with the rules
882
\frac{\Gamma\vdash A:\SET}{\Gamma\vdash \PROOF~A}~~~~~~
883
\frac{\Gamma\vdash M:\PROOF~A}{\Gamma\vdash \ZERO: \PROOF~A}~~~~~
884
\frac{\Gamma\vdash A_1=A_2:\SET}{\Gamma\vdash \PROOF~A_1 = \PROOF~A_2}
888
\frac{\Gamma\vdash M_1:\PROOF~A~~~~~\Gamma\vdash M_2:\PROOF~A}{\Gamma\vdash M_1=M_2:\PROOF~A}
891
Conversion is still decidable and type-checking for terms in $\beta$-normal
892
form which do not contain $\ZERO.$
894
Another reading of $\Gamma\vdash \ZERO:\PROOF~A$ is $\Gamma\vdash A~\TRUE$. We know
895
that $A$ has a proof but the proof has been hidden.
900
Notice that the strengthening property does not hold for this system.
902
The PER model extends directly to this system by interpreting $\ZERO$
903
by $\nabla$ and letting $\PROOF~u$ be the set $\EL~u$ with the universal
904
equivalence relation. So strong normalisation still holds for this system.
906
This is also a semantics for the following rule.
908
\frac{\Gamma\vdash M:\EL~A}{\Gamma\vdash M:\PROOF~A}
911
For proving the decidability of convertibility, we update the
912
definition of $\eta~A~M$ by taking $\eta~(\PROOF~M')~M = \ZERO$. It is then still
913
the case that $\vdash M_1=M_2:A$ iff $\eta~A~M_1=\eta~A~M_2$ if
914
$\vdash M_1:A$ and $\vdash M_2:A$.
917
If $A$ is in $\beta$-normal form and does not contain $\ZERO$
918
then $\vdash A$ is decidable. If $\vdash A$ and $M$ is
919
in $\beta$-normal form and does not contain $\ZERO$ then $\vdash M:A$ is decidable.
924
\begin{thebibliography}{9}
927
B. Nordstr\"om, K. Petersson, J. Smith.
928
\newblock{{\em Programming in Martin-L\"of's Type Theory.}}
929
\newblock{Oxford Science Publications, 1990.}
933
\end{thebibliography}
added
removed
notes/typechecking/core.tex
