proofs-algo.tex 63.7 KB
Newer Older
Giuseppe Castagna's avatar
Giuseppe Castagna committed
1
2
We  give in this section a typing algorithm that uses types schemes and is more general than the one presented in the main
body of the paper (that is, one whose completeness is not limited to
Giuseppe Castagna's avatar
Giuseppe Castagna committed
3
positive expressions). We start by defining how to compute the ``$\worra{}{}$'' operator and then we define type schemes and the algorithm. We prove that this algorithm (as well as the
Giuseppe Castagna's avatar
Giuseppe Castagna committed
4
5
6
one in the main body of the paper) is sound w.r.t.\ to the declarative type system
and that, under certain restrictions it is also complete.

Giuseppe Castagna's avatar
Giuseppe Castagna committed
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142



            \subsection{Operator $\worra {} {}$}\label{app:worra}

            In this section, we will use the algorithmic definition of $\worra {} {}$ and show that it is equivalent to its
            descriptive definition.

            \begin{eqnarray*}
                &t \simeq \bigvee_{i\in I}\left(\bigwedge_{p\in P_i}(s_p\to t_p)\bigwedge_{n\in N_i}\neg(s_n'\to t_n')\right)\\
                &\worra t s = \dom t \wedge\bigvee_{i\in I}\left(\bigwedge_{\{P \subseteq P_i\alt s \leq \bigvee_{p \in P} \neg t_p\}} \left(\bigvee_{p \in P} \neg s_p \right)\right)
            \end{eqnarray*}

            \begin{lemma}[Correctness of $\worra {} {}$]
                $\forall t, s.\ \apply t {(\dom t \setminus (\worra t s))} \leq \neg s$
            \end{lemma}

            \begin{proof}
            Let $t$ an arrow type. $t \simeq \bigvee_{i\in I}\left(\bigwedge_{p\in P_i}(s_p\to t_p)\bigwedge_{n\in N_i}\neg(s_n'\to t_n')\right)$\\
            Let $s$ be any type.

            Let's prove that $\apply t {(\dom t \setminus (\worra t s))} \leq \neg s$ (with the algorithmic definition for $\worra {} {}$).\\
            Equivalently, we want $(\apply t {(\dom t \setminus (\worra t s))}) \land s \simeq \Empty$.\\

            Let $u$ be a type such that $u \leq \dom t$ and $(\apply t u) \land s \not\simeq \Empty$ (if such a type does not exist, we are done).\\
            Let's show that $u \land (\worra t s) \not\simeq \Empty$ (we can easily deduce the wanted property from that, by the absurd).\\
            For that, we should prove the following:\\

            \[
                \exists i \in I.\
                u \land \bigwedge_{\{P \subseteq P_i\alt s \leq \bigvee_{p \in P} \neg t_p\}} \left(\bigvee_{p \in P} \neg s_p \right) \not\simeq \Empty
            \]

          From $(\apply t u) \land s \not\simeq \Empty$, we can take (using the algorithmic definition of $\circ$) $i \in I$ and $Q \subsetneq P_i$ such that:\\
          \[ u \not\leq\bigvee_{q\in Q}s_q \text{\ \ \ and\ \ \ } (\bigwedge_{p\in P_i\setminus Q}t_p) \land s \not\simeq \Empty \]

            For any $P \subseteq P_i$ such that $s \leq \bigvee_{p \in P} \neg t_p$ (equivalently, $s \land \bigwedge_{p \in P} t_p \simeq \Empty$),\\
            we have $P \cap Q \neq \varnothing$ (by the absurd, because $(\bigwedge_{p\in P_i\setminus Q}t_p) \land s \not\simeq \Empty$).\\
            Consequently, we have:
            \[ \forall P \subseteq P_i.\ s \leq \bigvee_{p \in P} \neg t_p \Rightarrow \bigwedge_{p \in P} s_p \leq \bigvee_{q \in Q}s_q \]
            We can deduce that:
            \[ \bigvee_{\{P \subseteq P_i\alt s \leq \bigvee_{p \in P} \neg t_p\}} \left(\bigwedge_{p \in P} s_p\right) \leq \bigvee_{q \in Q}s_q \]
            Moreover, as $u \not\leq \bigvee_{q\in Q}s_q$, we have $u \not\leq \bigvee_{\{P \subseteq P_i\alt s \leq \bigvee_{p \in P} \neg t_p\}} \left(\bigwedge_{p \in P} s_p\right)$.\\
            This is equivalent to the wanted result.
            \end{proof}

            \begin{lemma}[$\worra {} {}$ alternative definition]
                The following algorithmic definition for $\worra {} {}$ is equivalent to the previous one:

                \[\forall t, s.\ \worra t s \simeq \bigvee_{i \in I} \left( \bigvee_{\{P \subseteq P_i\alt s \not\leq \bigvee_{p \in P} \neg t_p \} }\left(
                    \dom t \land \bigwedge_{p\in P_i} s_p \land \bigwedge_{n \in P_i \setminus P} \neg s_n \right)\right)\]
            \end{lemma}

            \begin{proof}
            \begingroup
            \allowdisplaybreaks
            \begin{align*}
                \worra t s & = \dom t \wedge\bigvee_{i\in I}\left(
                    \bigwedge_{\{P \subseteq P_i\alt s \leq \bigvee_{p \in P} \neg t_p\}} \left(\bigvee_{p \in P} \neg s_p \right)\right)\\
                & \simeq \bigvee_{i\in I} \left(\dom t \wedge
                    \bigwedge_{\{P \subseteq P_i\alt s \leq \bigvee_{p \in P} \neg t_p\}} \left(\bigvee_{p \in P} \neg s_p \right)\right)\\
                & \simeq \bigvee_{i\in I} \left(\left( \dom t \wedge \bigvee_{p \in P_i} s_p \right) \wedge
                    \bigwedge_{\{P \subseteq P_i\alt s \leq \bigvee_{p \in P} \neg t_p\}} \left(\bigvee_{p \in P} \neg s_p \right)\right)\\
                & \simeq \bigvee_{i\in I} \left(\left( \dom t \wedge \bigvee_{p \in P_i} \left(s_p \land \bigvee_{P \subseteq P_i \setminus \{p\}}
                    \left(\bigwedge_{p \in P} s_p \land \bigwedge_{n \in (P_i \setminus \{p\}) \setminus P} \neg s_n \right) \right) \right) \wedge
                    \bigwedge_{\{P \subseteq P_i\alt s \leq \bigvee_{p \in P} \neg t_p\}} \left(\bigvee_{p \in P} \neg s_p \right)\right)\\
                & \simeq \bigvee_{i\in I} \left(\left( \dom t \wedge \bigvee_{p \in P_i} \left(\bigvee_{P \subseteq P_i \setminus \{p\}} \left( s_p \land
                    \bigwedge_{p \in P} s_p \land \bigwedge_{n \in (P_i \setminus \{p\}) \setminus P} \neg s_n \right) \right) \right) \wedge
                    \bigwedge_{\{P \subseteq P_i\alt s \leq \bigvee_{p \in P} \neg t_p\}} \left(\bigvee_{p \in P} \neg s_p \right)\right)\\
                & \simeq \bigvee_{i\in I} \left(\left( \dom t \wedge \bigvee_{\substack{P \subseteq P_i\\P \neq \varnothing}}
                    \left(\bigwedge_{p \in P} s_p \land \bigwedge_{n \in P_i \setminus P} \neg s_n \right) \right) \wedge
                    \bigwedge_{\{P \subseteq P_i\alt s \leq \bigvee_{p \in P} \neg t_p\}} \left(\bigvee_{p \in P} \neg s_p \right)\right)\\
                & \simeq \bigvee_{i\in I} \left( \dom t \wedge \bigvee_{\substack{P \subseteq P_i\\P \neq \varnothing}}
                    \left(\bigwedge_{p \in P} s_p \land \bigwedge_{n \in P_i \setminus P} \neg s_n \right) \setminus
                    \bigvee_{\{P \subseteq P_i\alt s \leq \bigvee_{p \in P} \neg t_p\}} \left(\bigwedge_{p \in P} s_p \right)\right)\\
                & \simeq \bigvee_{i\in I} \left( \dom t \wedge \bigvee_{\substack{P \subseteq P_i\\P \neq \varnothing}}
                    \left(\bigwedge_{p \in P} s_p \land \bigwedge_{n \in P_i \setminus P} \neg s_n \right) \setminus
                    \bigvee_{\{P \subseteq P_i\alt s \leq \bigvee_{p \in P} \neg t_p\}}
                    \left(\bigwedge_{p \in P} s_p \land \bigwedge_{n \in P_i \setminus P} \neg s_n \right)\right)\\
                & \simeq \bigvee_{i \in I} \left( \dom t \land \bigvee_{\{P \subseteq P_i\alt s \not\leq \bigvee_{p \in P} \neg t_p \} }\left(
                    \bigwedge_{p\in P_i} s_p \land \bigwedge_{n \in P_i \setminus P} \neg s_n \right)\right)\\
                & \simeq \bigvee_{i \in I} \left( \bigvee_{\{P \subseteq P_i\alt s \not\leq \bigvee_{p \in P} \neg t_p \} }\left(
                    \dom t \land \bigwedge_{p\in P_i} s_p \land \bigwedge_{n \in P_i \setminus P} \neg s_n \right)\right)
            \end{align*}
            \endgroup
            \end{proof}

            \begin{lemma}[Optimality of $\worra {} {}$]
                Let $t$, $s$, two types.
                For any $u$ such that $\apply t {(\dom t \setminus u)} \leq \neg s$, we have $\worra t s \leq u$.
            \end{lemma}

            \begin{proof}
            Let $t$ an arrow type. $t \simeq \bigvee_{i\in I}\left(\bigwedge_{p\in P_i}(s_p\to t_p)\bigwedge_{n\in N_i}\neg(s_n'\to t_n')\right)$\\
            Let $s$ be any type.

            Let $u$ be such that $\apply t {(\dom t \setminus u)} \leq \neg s$. We want to prove that $\worra t s \leq u$.

            We have:
            \[\worra t s = \bigvee_{i \in I} \left(\bigvee_{\{P \subseteq P_i\alt s \not\leq \bigvee_{p \in P} \neg t_p \} } a_{i,P}\right) \]
            With:
            \[a_{i,P}=\dom t \land \bigwedge_{p\in P_i} s_p \land \bigwedge_{n \in P_i \setminus P} \neg s_n\]

            Let $i \in I$ and $P \subseteq P_i$ such that $s \not\leq \bigvee_{p \in P} \neg t_p$ (equivalently, $s \land \bigwedge_{p \in P} t_p \not\simeq \Empty$) and such that $a_{i,P} \not\simeq \Empty$.\\
            For convenience, let $a = a_{i,P}$. We just have to show that $a \leq u$.

            By the absurd, let's suppose that $a \setminus u \not\simeq \Empty$ and show that $(\apply t {(\dom t \setminus u)}) \land s \not\simeq \Empty$.\\

            Let's recall the algorithmic definition of $\circ$:
            \[\apply t {(\dom t \setminus u)} = \bigvee_{i\in I}\left(\bigvee_{\{Q\subsetneq P_i\alt \dom t \setminus u \not\leq\bigvee_{q\in Q}s_q\}}\left(\bigwedge_{p\in P_i\setminus Q}t_p\right)\right)\]

            Let's take $Q = P_i \setminus P$. We just have to prove that:
            \[ \dom t \setminus u \not\leq\bigvee_{q\in Q}s_q \text{\ \ \ and\ \ \ } s \land \bigwedge_{p\in P_i\setminus Q}t_p \not\simeq \Empty \]

            As $P_i \setminus Q = P$, we immediatly have $s \land \bigwedge_{p\in P_i\setminus Q}t_p \not\simeq \Empty$.

            Moreover, we know that $a \leq \bigwedge_{q \in Q} \neg s_q$ (definition of $a_{i,P}$), so we have:
            \[a \land \bigwedge_{q\in Q} \neg s_q \simeq a\]
            Thus: \[(a \setminus u) \land \bigwedge_{q\in Q} \neg s_q \simeq (a \land \bigwedge_{q\in Q} \neg s_q) \setminus u \simeq a \setminus u \not\simeq \Empty\]
            And so: \[ a \setminus u \not\leq \bigvee_{q\in Q}s_q \]

            As $ \dom t \setminus u \geq a \setminus u$, we can immediatly obtain the remaining inequality.
            \end{proof}

            \begin{theorem}[Characterization of $\worra {} {}$]
                $\forall t, s.\ \worra t s = \min \{ u \alt \apply t {(\dom t \setminus u)} \leq \neg s \}$.
            \end{theorem}

            \begin{proof}
            Immediate consequence of the previous results.
            \end{proof}





Giuseppe Castagna's avatar
Giuseppe Castagna committed
143
\subsection{Type Schemes}
Giuseppe Castagna's avatar
Giuseppe Castagna committed
144
145
146
147
148
149
150
151



We introduce for the proofs the notion of \emph{type schemes}
and we define a more powerful algorithmic type system that uses them.
It allows us to have a stronger (but still partial) completeness theorem.

The proofs for the algorithmic type system presented in \ref{sec:algorules} can be derived
Giuseppe Castagna's avatar
Giuseppe Castagna committed
152
from the proofs of this section (see Section \ref{sec:proofs_algorithmic_without_ts}).
Giuseppe Castagna's avatar
Giuseppe Castagna committed
153
154
155
156
157
158
159
160
161
162
163

\subsubsection{Type schemes}\label{app:typeschemes}

We introduce the new syntactic category of \emph{type schemes} which are the terms~$\ts$ inductively produced by the following grammar.
\[
\begin{array}{lrcl}
  \textbf{Type schemes} & \ts & ::= & t \alt \tsfun {\arrow t t ; \cdots ; \arrow t t} \alt \ts \tstimes \ts \alt \ts \tsor \ts \alt \tsempty
\end{array}
\]
Type schemes denote sets of types, as formally stated by the following definition:
\begin{definition}[Interpretation of type schemes]
Kim Nguyễn's avatar
Kim Nguyễn committed
164
  We define the function $\tsint {\_}$ that maps type schemes into sets of types.\svvspace{-2.5mm}
Giuseppe Castagna's avatar
Giuseppe Castagna committed
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
  \begin{align*}
    \begin{array}{lcl}
    \tsint t &=& \{s\alt t \leq s\}\\
    \tsint {\tsfunone {t_i} {s_i}_{i=1..n}} &=& \{s\alt
    \exists s_0 = \bigwedge_{i=1..n} \arrow {t_i} {s_i}
    \land \bigwedge_{j=1..m} \neg (\arrow {t_j'} {s_j'}).\
    \Empty \not\simeq s_0 \leq s \}\\
    \tsint {\ts_1 \tstimes \ts_2} &=& \{s\alt \exists t_1 \in \tsint {\ts_1}\
    \exists t_2 \in \tsint {\ts_2}.\ \pair {t_1} {t_2} \leq s\}\\
    \tsint {\ts_1 \tsor \ts_2} &=& \{s\alt \exists t_1 \in \tsint {\ts_1}\
    \exists t_2 \in \tsint {\ts_2}.\ {t_1} \vee {t_2} \leq s\}\\
    \tsint \tsempty &=& \varnothing
    \end{array}
  \end{align*}
\end{definition}
Note that $\tsint \ts$ is closed under subsumption and intersection
 and that $\tsempty$, which denotes the
empty set of types is different from $\Empty$ whose interpretation is
the set of all types.

\begin{lemma}[\cite{Frisch2008}]
  Let $\ts$ be a type scheme and $t$ a type. It is possible to decide the assertion $t \in \tsint \ts$,
  which we also write $\ts \leq t$.
\end{lemma}

We can now formally define the relation $v\in t$ used in
Section~\ref{sec:opsem} to define the dynamic semantics of
the language. First, we associate each (possibly, not well-typed)
value to a type scheme representing the best type information about
the value. By induction on the definition of values: $\tyof c {} =
\basic c$, $\tyof {\lambda^{\wedge_{i\in I}s_i\to t_i} x.e}{}=
\tsfun{s_i\to t_i}_{i\in I}$, $\tyof {(v_1,v_2)}{} = \tyof
      {v_1}{}\tstimes\tyof {v_1}{}$. Then we have $v\in t\iffdef \tyof
      v{}\leq t$.

We also need to perform intersections of type schemes so as to intersect the static type of an expression (i.e., the one deduced by conventional rules) with the one deduced by occurrence typing (i.e., the one derived by $\vdashp$). For our algorithmic system (see \Rule{Env$_{\scriptscriptstyle\mathcal{A}}$} in Section~\ref{sec:algorules}) all we need to define is the intersection of a type scheme with a type:
\begin{lemma}[\cite{Frisch2008}]
  Let $\ts$ be a type scheme and $t$ a type. We can compute a type scheme, written $t \tsand \ts$, such that
  \(\tsint {t \tsand \ts} = \{s \alt \exists t' \in \tsint \ts.\ t \land t' \leq s \}\)
\end{lemma}
Finally, given a type scheme $\ts$ it is straightforward to choose in its interpretation a type $\tsrep\ts$ which serves as the canonical representative of the set (i.e., $\tsrep \ts \in \tsint \ts$):
\begin{definition}[Representative]
Kim Nguyễn's avatar
Kim Nguyễn committed
207
  We define a function $\tsrep {\_}$ that maps every non-empty type scheme into a type, \textit{representative} of the set of types denoted by the scheme.\svvspace{-2mm}
Giuseppe Castagna's avatar
Giuseppe Castagna committed
208
209
210
211
212
  \begin{align*}
    \begin{array}{lcllcl}
    \tsrep t &=& t  &  \tsrep {\ts_1 \tstimes \ts_2} &=& \pair {\tsrep {\ts_1}} {\tsrep {\ts_2}}\\
    \tsrep {\tsfunone {t_i} {s_i}_{i\in I}} &=& \bigwedge_{i\in I} \arrow {t_i} {s_i} \qquad&    \tsrep {\ts_1 \tsor \ts_2} &=& \tsrep {\ts_1} \vee \tsrep {\ts_2}\\
    \tsrep \tsempty && \textit{undefined}
Kim Nguyễn's avatar
Kim Nguyễn committed
213
    \end{array}\svvspace{-4mm}
Giuseppe Castagna's avatar
Giuseppe Castagna committed
214
215
216
217
218
219
220
  \end{align*}
\end{definition}

Type schemes are already present in the theory of semantic subtyping presented in~\cite[Section
6.11]{Frisch2008}. In particular, it explains how the operators such as $\circ$, $\bpl t$ and $\bpr t$
can be extended to type schemes (see also~\citep[\S4.4]{Cas15} for a detailed description).

Giuseppe Castagna's avatar
Giuseppe Castagna committed
221
\subsection{Algorithmic type system with type schemes}
Giuseppe Castagna's avatar
Giuseppe Castagna committed
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519

We present here a refinement of the algorithmic type system presented in \ref{sec:algorules}
that associates to an expression a type scheme instead of a regular type.
This allows to type expressions more precisely and thus to have a more powerful
(but still partial) completeness theorem in regards to the declarative type system.

The results about this new type system will be used in \ref{sec:proofs_algorithmic_without_ts} in order to obtain a soundness and completeness
theorem for the algorithmic type system presented in \ref{sec:algorules}.

            \begin{mathpar}
              \Infer[Efq\Aats]
          { }
          { \Gamma, (e:\Empty) \vdashAts e': \Empty }
          { \begin{array}{c}\text{\tiny with priority over}\\[-1.8mm]\text{\tiny all the other rules}\end{array}}
          \qquad
          \Infer[Var\Aats]
              { }
              { \Gamma \vdashAts x: \Gamma(x) }
              { x\in\dom\Gamma}
          \\
          \Infer[Env\Aats]
              { \Gamma\setminus\{e\} \vdashAts e : \ts }
              { \Gamma \vdashAts e: \Gamma(e) \tsand \ts }
              { e\in\dom\Gamma \text{ and } e \text{ not a variable}}
          \qquad
          \Infer[Const\Aats]
              { }
              {\Gamma\vdashAts c:\basic{c}}
              {c\not\in\dom\Gamma}
           \\
              \Infer[Abs\Aats]
                  {\Gamma,x:s_i\vdashAts e:\ts_i'\\ \ts_i'\leq t_i}
                  {
                  \Gamma\vdashAts\lambda^{\wedge_{i\in I}\arrow {s_i} {t_i}}x.e:\textstyle\tsfun {\arrow {s_i} {t_i}}_{i\in I}
                  }
                  {\lambda^{\wedge_{i\in I}\arrow {s_i} {t_i}}x.e\not\in\dom\Gamma}
                  \\
              \Infer[App\Aats]
                  {
                    \Gamma \vdashAts e_1: \ts_1\\
                    \Gamma \vdashAts e_2: \ts_2\\
                    \ts_1 \leq \arrow \Empty \Any\\
                    \ts_2 \leq \dom {\ts_1}
                  }
                  { \Gamma \vdashAts {e_1}{e_2}: \ts_1 \circ \ts_2 }
                  { {e_1}{e_2}\not\in\dom\Gamma}
                  \\
              \Infer[Case\Aats]
                    {\Gamma\vdashAts e:\ts_0\\
                    \Refine {e,t} \Gamma \vdashAts e_1 : \ts_1\\
                    \Refine {e,\neg t} \Gamma \vdashAts e_2 : \ts_2}
                    {\Gamma\vdashAts \tcase {e} t {e_1}{e_2}: \ts_1\tsor \ts_2}
                    { \tcase {e} {t\!} {\!e_1\!}{\!e_2}\not\in\dom\Gamma}
              \\
              \Infer[Proj\Aats]
              {\Gamma \vdashAts e:\ts\and \ts\leq\pair\Any\Any}
              {\Gamma \vdashAts \pi_i e:\bpi_{\mathbf{i}}(\ts)}
              {\pi_i e\not\in\dom\Gamma}

              \Infer[Pair\Aats]
              {\Gamma \vdashAts e_1:\ts_1 \and \Gamma \vdashAts e_2:\ts_2}
              {\Gamma \vdashAts (e_1,e_2):{\ts_1}\tstimes{\ts_2}}
              {(e_1,e_2)\not\in\dom\Gamma}

            \end{mathpar}

            \begin{align*}
              \tyof e \Gamma =
              \left\{\begin{array}{ll}
                \ts & \text{if } \Gamma \vdashAts e:\ts \\
                \tsempty & \text{otherwise}
              \end{array}\right.
            \end{align*}

            \begin{eqnarray}
              \constr\epsilon{\Gamma,e,t} & = & t\\
              \constr{\varpi.0}{\Gamma,e,t} & = & \neg(\arrow{\env {\Gamma,e,t}{(\varpi.1)}}{\neg \env {\Gamma,e,t} (\varpi)})\\
              \constr{\varpi.1}{\Gamma,e,t} & = & \worra{\tsrep {\tyof{\occ e{\varpi.0}}\Gamma}}{\env {\Gamma,e,t} (\varpi)}\\
              \constr{\varpi.l}{\Gamma,e,t} & = & \bpl{\env {\Gamma,e,t} (\varpi)}\\
              \constr{\varpi.r}{\Gamma,e,t} & = & \bpr{\env {\Gamma,e,t} (\varpi)}\\
              \constr{\varpi.f}{\Gamma,e,t} & = & \pair{\env {\Gamma,e,t} (\varpi)}\Any\\
              \constr{\varpi.s}{\Gamma,e,t} & = & \pair\Any{\env {\Gamma,e,t} (\varpi)}\\
              \env {\Gamma,e,t} (\varpi) & = & \tsrep {\constr \varpi {\Gamma,e,t} \tsand \tyof {\occ e \varpi} \Gamma}
            \end{eqnarray}

            \begin{align*}
              &\RefineStep {e,t} (\Gamma) = \Gamma' \text{ with:}\\
              &\dom{\Gamma'}=\dom{\Gamma} \cup \{e' \alt \exists \varpi.\ \occ e \varpi \equiv e'\}\\
              &\Gamma'(e') =
                \left\{\begin{array}{ll}
                  \bigwedge_{\{\varpi \alt \occ e \varpi \equiv e'\}}
                  \env {\Gamma,e,t} (\varpi) & \text{if } \exists \varpi.\ \occ e \varpi \equiv e' \\
                  \Gamma(e') & \text{otherwise}
                \end{array}\right.\\&\\
              &\Refine {e,t} \Gamma={\RefineStep {e,t}}^{n_o}(\Gamma)\qquad\text{with $n$ a global parameter}
            \end{align*}


            \subsection{Proofs for the algorithmic type system with type schemes}

            This section is about the algorithmic type system with type schemes (soundness and some completeness properties).

            Note that, now that we have type schemes, use a different but more convenient definition for $\tyof e \Gamma$ that the one
            in Section~\ref{sec:typenv}:
            \begin{align*}
              \tyof e \Gamma =
              \left\{\begin{array}{ll}
                \ts & \text{if } \Gamma \vdashAts e:\ts \\
                \tsempty & \text{otherwise}
              \end{array}\right.
            \end{align*}

            In this way, $\tyof e \Gamma$ is always defined but is equal to $\tsempty$ when $e$ is not
            well-typed in $\Gamma$.

            We will reuse the definitions and notations introduced in the previous proofs.
            In particular, we only consider well-formed environments, as in the proofs of the declarative type system.

            \subsubsection{Soundness}

            \begin{theorem}[Soundness of the algorithm]\label{soundnessAts}
              For every $\Gamma$, $e$, $t$, $n_o$, if $\tyof e \Gamma \leq t$, then we can derive $\Gamma \vdash e:t$.

              More precisely:
              \begin{align*}
                &\forall \Gamma, e, t.\ \tyof e \Gamma \leq t \Rightarrow \Gamma \vdash e:t\\
                &\forall \Gamma, e, t, \varpi.\ \tyof e \Gamma \neq \tsempty \Rightarrow \pvdash \Gamma e t \varpi:\env {\Gamma,e,t} (\varpi)\\
                &\forall \Gamma, e, t.\ \tyof e \Gamma \neq \tsempty \Rightarrow \Gamma \evdash e t \Refine {e,t} \Gamma
              \end{align*}
            \end{theorem}

            \begin{proof}
            We proceed by induction over the structure of $e$
            and, for two identical $e$, on the domain of $\Gamma$ (with the inclusion order).

            Let's prove the first property.
            Let $t$ such that $\tsint{\tyof e \Gamma} \leq t$.

            If $\Gamma = \bot$, we trivially have $\Gamma \vdash e:t$ with the rule \Rule{Efq}.
            Let's assume $\Gamma \neq \bot$.

            If $e=x$ is a variable, then the last rule used is \Rule{Var\Aats}.
            We can derive $\Gamma \vdash x:t$ by using the rule \Rule{Env} and \Rule{Subs}.
            So let's assume that $e$ is not a variable.

            If $e\in\dom\Gamma$, then the last rule used is \Rule{Env\Aats}.
            Let $t'\in\tsint{\ts}$ such that $t'\land\Gamma(e)\leq t$.
            The induction hypothesis gives $\Gamma\setminus\{e\} \vdash e:t'$
            (the premise uses the same $e$ but the domain of $\Gamma$ is strictly smaller).
            Thus, we can build a derivation $\Gamma \vdash e:t$ by using the rules \Rule{Subs}, \Rule{Inter},
            \Rule{Env} and the derivation $\Gamma\setminus\{e\} \vdash e:t'$.

            Now, let's suppose that $e\not\in\dom\Gamma$.

            \begin{description}
              \item[$e=c$] The last rule is \Rule{Const\Aats}. We derive easily $\Gamma \vdash c:t$ with \Rule{Const} and \Rule{Subs}.
              \item[$e=x$] Already treated.
              \item[$e=\lambda^{\bigwedge_{i\in I} \arrow {t_i}{s_i}}x.e'$]
              The last rule is \Rule{Abs\Aats}.
              We have $\bigwedge_{i\in I} \arrow {t_i}{s_i} \leq t$.
              Using the definition of type schemes, let $t'=\bigwedge_{i\in I} \arrow {t_i}{s_i} \land \bigwedge_{j\in J} \neg \arrow {t'_j}{s'_j}$ such that $\Empty \neq t' \leq t$.
              The induction hypothesis gives, for all $i\in I$, $\Gamma,x:s_i\vdash e':t_i$.

              Thus, we can derive $\Gamma\vdash e:\bigwedge_{i\in I} \arrow {t_i}{s_i}$ using the rule \Rule{Abs+}, and with \Rule{Inter} and
              \Rule{Abs-} we can derive $\Gamma\vdash e:t'$. We can conclude by applying \Rule{Subs}.
              \item[$e=e_1 e_2$] The last rule is \Rule{App\Aats}.
              We have $\apply {\ts_1} {\ts_2} \leq t$. Thus, let $t_1$ and $t_2$ such that $\ts_1 \leq t_1$, $\ts_2 \leq t_2$ and $\apply {t_1} {t_2} \leq t$.
              We know, according to the descriptive definition of $\apply {} {}$, that there exists $s\leq t$ such that $t_1 \leq \arrow {t_2} s$.

              By using the induction hypothesis, we have $\Gamma\vdash e_1:t_1$ and $\Gamma\vdash e_2:t_2$. We can thus derive
              $\Gamma\vdash e_1:\arrow {t_2} s$ using \Rule{Subs}, and together with $\Gamma\vdash e_2:t_2$ it gives
              $\Gamma\vdash e_1\ e_2:s$ with \Rule{App}. We conclude with \Rule{Subs}.

              \item[$e=\pi_i e'$] The last rule is \Rule{Proj\Aats}. We have $\bpi_i \ts \leq t$. Thus, let $t'$ such that $\ts \leq t'$ and $\bpi_i t' \leq t$.
              We know, according to the descriptive definition of $\bpi_i$, that there exists $t_i\leq t$ such that $t' \leq \pair \Any {t_i}$ (for $i=2$) or $t' \leq \pair {t_i} \Any$ (for $i=1$).

              By using the induction hypothesis, we have $\Gamma\vdash e':t'$, and thus we easily conclude using \Rule{Subs} and \Rule{Proj}
              (for instance for the case $i=1$, we can derive $\Gamma\vdash e':\pair {t_i} \Any$ with \Rule{Subs} and then use \Rule{Proj}).

              \item[$e=(e_1,e_2)$] The last rule is \Rule{Pair\Aats}. We conclude easily with the induction hypothesis and the rules \Rule{Subs} and \Rule{Pair}.

              \item[$e=\ite {e_0} t {e_1} {e_2}$] The last rule is \Rule{Case\Aats}. We conclude easily with the induction hypothesis and the rules
              \Rule{Subs} and \Rule{Case} (for the application of \Rule{Case}, $t'$ must be taken equal to $t_1 \vee t_2$ with $t_1$ and $t_2$ such that $\ts_1\leq t_1$, $\ts_2\leq t_2$ and $t_1 \vee t_2 \leq t$).
            \end{description}\ \\

            Now, let's prove the second property.
            We perform a (nested) induction on $\varpi$.

            Recall that $\env {\Gamma,e,t} (\varpi) = \tsrep {\constr \varpi {\Gamma,e,t} \tsand \tyof {\occ e \varpi} \Gamma}$.

            For any $t'$ such that $\tyof {\occ e \varpi} \Gamma \leq t'$, we can easily derive $\pvdash \Gamma e t \varpi : t'$ by using the outer induction hypothesis
            (the first property that we have proved above) and the rule \Rule{PTypeof}.

            Now we have to derive $\pvdash \Gamma e t \varpi : \constr \varpi {\Gamma,e,t}$ (then it will be easy to conclude using the rule \Rule{PInter}).
            \begin{description}
              \item[$\varpi=\epsilon$] We use the rule \Rule{PEps}.
              \item[$\varpi=\varpi'.1$]
              Let's note $f=\tsrep {\tyof {\occ e {\varpi'.0}} \Gamma}$, $s=\env {\Gamma,e,t} (\varpi')$ and $t_{\text{res}} = \worra f s$.

              By using the outer and inner induction hypotheses, we can derive $\pvdash \Gamma e t \varpi'.0 : f$ and $\pvdash \Gamma e t \varpi' : s$.

              By using the descriptive definition of $\worra {} {}$, we have $t' = \apply f {(\dom f \setminus t_{\text{res}})} \leq \neg s$.

              Moreover, by using the descriptive definition of $\apply {} {}$ on $t'$, we have
              $f \leq \arrow {(\dom f \setminus t_{\text{res}})} {t'}$.

              As $t'\leq \neg s$, it gives $f \leq \arrow {(\dom f \setminus t_{\text{res}})} {\neg s}$.

              Let's note $t_1 = \dom f \setminus t_{\text{res}}$ and $t_2 = \neg s$. The above inequality can be rewritten $f \leq \arrow {t_1} {t_2}$.

              Thus, by using \Rule{PSubs} on the derivation $\pvdash \Gamma e t \varpi'.0 : f$, we can derive $\pvdash \Gamma e t \varpi'.0 : \arrow {t_1} {t_2}$.
              We have:
              \begin{itemize}
                \item $t_2 \land s \simeq \Empty$ (as $t_2 = \neg s$)
                \item $\neg t_1 = t_{\text{res}} \vee \neg \dom f = t_{\text{res}}$
              \end{itemize}

              In consequence, we can conclude by applying the rule \Rule{PAppR}
              with the premises $\pvdash \Gamma e t \varpi'.0 : \arrow {t_1} {t_2}$ and $\pvdash \Gamma e t \varpi' : s$.

              \item[$\varpi=\varpi'.0$] By using the inner induction hypothesis and the previous case we've just proved, we can derive
              $\pvdash \Gamma e t \varpi' : \env {\Gamma,e,t} (\varpi')$ and $\pvdash \Gamma e t \varpi'.1 : \env {\Gamma,e,t} (\varpi'.1)$.
              Hence we can apply \Rule{PAppL}.
              \item[$\varpi=\varpi'.l$] Let's note $t_1=\bpi_1 \env {\Gamma,e,t} (\varpi')$.
              According to the descriptive definition of $\bpi_1$, we have $\env {\Gamma,e,t} (\varpi') \leq \pair {t_1} {\Any}$.

              The inner induction hypothesis gives $\pvdash \Gamma e t \varpi' : \env {\Gamma,e,t} (\varpi')$, and thus using the rule \Rule{PSubs}
              we can derive $\pvdash \Gamma e t \varpi' : \pair {t_1} \Any$. We can conclude just by applying the rule \Rule{PPairL} to this premise.
              \item[$\varpi=\varpi'.r$] This case is similar to the previous.
              \item[$\varpi=\varpi'.f$] The inner induction hypothesis gives $\pvdash \Gamma e t \varpi' : \env {\Gamma,e,t} (\varpi')$,
              so we can conclude by applying \Rule{PFst}.
              \item[$\varpi=\varpi'.s$] The inner induction hypothesis gives $\pvdash \Gamma e t \varpi' : \env {\Gamma,e,t} (\varpi')$,
              so we can conclude by applying \Rule{PSnd}.
            \end{description}\ \\

            Finally, let's prove the third property.
            Let $\Gamma' = \Refine {e,t} \Gamma = {\RefineStep{e,t}}^{n_0}(\Gamma)$.
            We want to show that $\Gamma \evdash e t \Gamma'$ is derivable.

            First, let's note that $\evdash e t$ is transitive:
            if $\Gamma \evdash e t \Gamma'$ and $\Gamma' \evdash e t \Gamma''$, then $\Gamma \evdash e t \Gamma''$.
            The proof is quite easy: we can just start from the derivation of $\Gamma \evdash e t \Gamma'$, and we add
            at the end a slightly modified version of the derivation of $\Gamma' \evdash e t \Gamma''$ where:
            \begin{itemize}
              \item the initial \Rule{Base} rule has been removed in order to be able to do the junction,
              \item all the $\Gamma'$ at the left of $\evdash e t$ are replaced by $\Gamma$
              (the proof is still valid as this $\Gamma'$ at the left is never used in any rule)
            \end{itemize}

            Thanks to this property, we can suppose that $n_0 = 1$ (and so $\Gamma' = \RefineStep{e,t}(\Gamma)$).
            If it is not the case, we just have to proceed by induction on $n_0$ and use the transitivity property.

            Let's build a derivation for $\Gamma \evdash e t \Gamma'$.

            By using the proof of the second property on $e$ that we've done just before, we get:
            $\forall \varpi.\ \pvdash \Gamma e t \varpi: \env {\Gamma,e,t} (\varpi)$.

            Let's recall a monotonicity property: for any $\Gamma_1$ and $\Gamma_2$ such that $\Gamma_2 \leq \Gamma_1$, we have
            $\forall t'.\ \pvdash {\Gamma_1} e t \varpi:t' \Rightarrow \pvdash {\Gamma_2} e t \varpi:t'$.\\
            Moreover, when we also have $\occ e \varpi \in\dom{\Gamma_2}$, we can derive $\pvdash {\Gamma_2} e t \varpi:t'\land\Gamma_2(\occ e \varpi)$
            (just by adding a \Rule{PInter} rule with a \Rule{PTypeof} and a \Rule{Env}).

            Hence, we can apply successively a \Rule{Path} rule for all valid $\varpi$ in $e$,
            with the following premises ($\Gamma_\varpi$ being the previous environment, that trivially verifies $\Gamma_\varpi\leq\Gamma$):\\

            \begin{tabular}{lll}
              If $\occ e \varpi \in\dom{\Gamma_\varpi}$&$\pvdash {\Gamma_\varpi} e t \varpi: \env {\Gamma,e,t} (\varpi)\land\Gamma_\varpi(\occ e \varpi)$&$\Gamma\evdash e t {\Gamma_\varpi}$\\
              Otherwise&$\pvdash {\Gamma_\varpi} e t \varpi: \env {\Gamma,e,t} (\varpi)$&$\Gamma\evdash e t {\Gamma_\varpi}$
            \end{tabular}

            At the end, it gives the judgement $\Gamma \evdash e t \Gamma'$, so it concludes the proof.
            \end{proof}

            \subsubsection{Completeness}

            \begin{definition}[Bottom environment]
              Let $\Gamma$ an environment.\\
              $\Gamma$ is bottom (noted $\Gamma = \bot$) iff $\exists e\in\dom\Gamma.\ \Gamma(e)\simeq\Empty$.
            \end{definition}

            \begin{definition}[Algorithmic (pre)order on environments]
            Let $\Gamma$ and $\Gamma'$ two environments. We write $\Gamma' \leqA \Gamma$ iff:
            \begin{align*}
                &\Gamma'=\bot \text{ or } (\Gamma\neq\bot \text{ and } \forall e \in \dom \Gamma.\ \tyof e \Gamma \leq \Gamma(e))
            \end{align*}

            For an expression $e$, we write $\Gamma' \leqA^e \Gamma$ iff:
            \begin{align*}
              &\Gamma'=\bot \text{ or } (\Gamma\neq\bot \text{ and } \forall e' \in \dom \Gamma \text{ such that $e'$ is a subexpression of $e$}.\ \tyof {e'} \Gamma \leq \Gamma({e'}))
            \end{align*}

            Note that if $\Gamma' \leqA \Gamma$, then $\Gamma' \leqA^e \Gamma$ for any $e$.
            \end{definition}

            \begin{definition}[Order relation for type schemes]
              Let $\ts_1$ and $\ts_2$ two type schemes. We write $\ts_2 \leq \ts_1$ iff $\tsint {\ts_1} \subseteq \tsint{\ts_2}$.
            \end{definition}

520
          \begin{lemma} When well-defined, the following inequalities hold:
Giuseppe Castagna's avatar
Giuseppe Castagna committed
521
522
            \begin{align*}
              &\forall t,\ts.\ \tsrep{t\tsand\ts} \leq t \land \tsrep{\ts}\\
523
              &\forall t_1,t_2,\ts_1,\ts_2.\ t_1 \leq t_2 \text{ and } \ts_1\leq\ts_2 \text{ and } \tsrep{\ts_1}\leq\tsrep{\ts_2} \Rightarrow \tsrep{t_1\tsand\ts_1} \leq \tsrep{t_2\tsand\ts_2}\\
Giuseppe Castagna's avatar
Giuseppe Castagna committed
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
              &\forall \ts_1,\ts_2.\ \tsrep{\apply {\ts_1}{\ts_2}} \leq \apply {\tsrep {\ts_1}}{\tsrep {\ts_2}}
            \end{align*}
          \end{lemma}

          \begin{proof}
            Straightfoward, by induction on the structure of $\ts$.
          \end{proof}

          \begin{lemma}[Monotonicity of the algorithm] Let $\Gamma$, $\Gamma'$ and $e$ such that $\Gamma'\leqA^e \Gamma$ and $\tyof e \Gamma \neq \tsempty$. We have:
            \begin{align*}
              &\tyof e {\Gamma'} \leq \tyof e {\Gamma} \text{ and } \tsrep{\tyof e {\Gamma'}} \leq \tsrep{\tyof e {\Gamma}}\\
              &\forall t,\varpi.\ \env {\Gamma',e,t} (\varpi) \leq \env {\Gamma,e,t} (\varpi)\\
              &\forall t.\ \Refine {e,t} {\Gamma'} \leqA^e \Refine {e,t} \Gamma\\
            \end{align*}
          \end{lemma}

          \begin{proof}
          We proceed by induction over the structure of $e$
          and, for two identical $e$, on the domains of $\Gamma$ and $\Gamma'$ (with the lexicographical inclusion order).

          Let's prove the first property: $\tyof e {\Gamma'} \leq \tyof e {\Gamma} \text{ and } \tsrep{\tyof e {\Gamma'}} \leq \tsrep{\tyof e {\Gamma}}$.
          We will focus on showing $\tyof e {\Gamma'} \leq \tyof e {\Gamma}$.

          The property $\tsrep{\tyof e {\Gamma'}} \leq \tsrep{\tyof e {\Gamma}}$
          can be proved in a very similar way, by using the fact that operators on type schemes like $\tsand$ or $\apply {} {}$ are also monotone.
          (Note that the only rule that introduces the type scheme constructor $\tsfun {\_}$ is \Rule{Abs\Aats}.)

          If $\Gamma' = \bot$ we can conclude directly with the rule \Rule{Efq\Aats}.
          So let's assume $\Gamma' \neq \bot$ and $\Gamma \neq \bot$
          (as $\Gamma = \bot \Rightarrow \Gamma' = \bot$ by definition of $\leqA^e$).

          If $e=x$ is a variable, then the last rule used in $\tyof e \Gamma$ and $\tyof e {\Gamma'}$ is \Rule{Var\Aats}.
          As $\Gamma' \leqA^e \Gamma$, we have $\Gamma'(e) \leq \Gamma(e)$ and thus
          we can conclude with the rule \Rule{Var\Aats}.
          So let's assume that $e$ is not a variable.

          If $e\in\dom\Gamma$, then the last rule used in $\tyof e \Gamma$ is \Rule{Env\Aats}.
          As $\Gamma' \leqA^e \Gamma$, we have $\tyof e {\Gamma'} \leq \Gamma(e)$.
          Moreover, by applying the induction hypothesis, we get $\tyof e {\Gamma'\setminus \{e\}} \leq \tyof e {\Gamma\setminus \{e\}}$
          (we can easily verify that $\Gamma'\setminus\{e\} \leqA^e \Gamma\setminus\{e\}$).
          \begin{itemize}
            \item If we have $e\in\dom{\Gamma'}$, we have according to the rule \Rule{Env\Aats}
            $\tyof e {\Gamma'} \leq \tyof e {\Gamma'\setminus \{e\}} \leq \tyof e {\Gamma\setminus \{e\}}$.

            Together with $\tyof e {\Gamma'} \leq \Gamma(e)$,
            we deduce $\tyof e {\Gamma'} \leq \Gamma(e) \tsand \tyof e {\Gamma\setminus \{e\}} = \tyof e {\Gamma}$.
            \item  Otherwise, we have $e\not\in\dom{\Gamma'}$. Thus
            $\tyof e {\Gamma'} = \tyof e {\Gamma'\setminus \{e\}} \leq \Gamma(e) \tsand \tyof e {\Gamma\setminus \{e\}}=\tyof e {\Gamma}$.
          \end{itemize}

          If $e\not\in\dom\Gamma$ and $e\in\dom{\Gamma'}$, the last rule is \Rule{Env\Aats} for $\tyof e {\Gamma'}$.
          As $\Gamma'\setminus\{e\} \leqA^e \Gamma\setminus\{e\} = \Gamma$,
          we have $\tyof e {\Gamma'} \leq \tyof e {\Gamma'\setminus \{e\}} \leq \tyof e {\Gamma}$ by induction hypothesis.

          Thus, let's suppose that $e\not\in\dom\Gamma$ and $e\not\in\dom{\Gamma'}$.
          From now we know that the last rule in the derivation of $\tyof e {\Gamma}$ and $\tyof e {\Gamma'}$ (if any) is the same.

          \begin{description}
            \item[$e=c$] The last rule is \Rule{Const\Aats}. It does not depend on $\Gamma$ so this case is trivial.
            \item[$e=x$] Already treated.
            \item[$e=\lambda^{\bigwedge_{i\in I} \arrow {t_i}{s_i}}x.e'$]
            The last rule is \Rule{Abs\Aats}.
            We have $\forall i\in I.\ \Gamma', (x:s_i) \leqA^{e'} \Gamma, (x:s_i)$ (quite straightforward)
            so by applying the induction hypothesis we have $\forall i\in I.\ \tyof {e'} {\Gamma', (x:s_i)} \leq \tyof {e'} {\Gamma, (x:s_i)}$.

            \item[$e=e_1 e_2$] The last rule is \Rule{App\Aats}.
            We can conclude immediately by using the induction hypothesis and noticing that $\apply {} {}$ is monotonic for both of its arguments.

            \item[$e=\pi_i e'$] The last rule is \Rule{Proj\Aats}.
            We can conclude immediately by using the induction hypothesis and noticing that $\bpi_i$ is monotonic.

            \item[$e=(e_1,e_2)$] The last rule is \Rule{Pair\Aats}.
            We can conclude immediately by using the induction hypothesis.

            \item[$e=\ite {e_0} t {e_1} {e_2}$] The last rule is \Rule{Case\Aats}.
            By using the induction hypothesis we get $\Refine {e_0,t} {\Gamma'} \leqA^{e_0} \Refine {e_0,t} \Gamma$.
            We also have $\Gamma' \leqA^{e_1} \Gamma$ (as $e_1$ is a subexpression of $e$).

            From those two properties, let's show that we can deduce $\Refine {e_0,t} {\Gamma'} \leqA^{e_1} \Refine {e_0,t} \Gamma$:

            Let $e'\in\dom{\Refine {e_0,t} \Gamma}$ a subexpression of $e_1$.
            \begin{itemize}
              \item If $e'$ is also a subexpression of $e_0$, we can directly deduce\\
              $\tyof {e'} {\Refine {e_0,t} \Gamma'} \leq (\Refine {e_0,t} \Gamma) (e')$
              by using $\Refine {e_0,t} {\Gamma'} \leqA^{e_0} \Refine {e_0,t} \Gamma$.

              \item Otherwise, as $\Refine {e_0,t} {\_}$ is reductive,
              we have $\Refine {e_0,t} {\Gamma'} \leqA \Gamma'$ and thus by using the induction hypothesis
              $\tyof {e'} {\Refine {e_0,t} {\Gamma'}} \leq \tyof {e'} {\Gamma'}$.
              We also have $\tyof {e'} {\Gamma'} \leq \Gamma(e')$ by using $\Gamma' \leqA^{e_1} \Gamma$.
              We deduce $\tyof {e'} {\Refine {e_0,t} {\Gamma'}} \leq \Gamma(e') = (\Refine {e_0,t} \Gamma) (e')$.
            \end{itemize}

            So we have $\Refine {e_0,t} {\Gamma'} \leqA^{e_1} \Refine {e_0,t} \Gamma$.
            Consequently, we can apply the induction hypothesis again to get
            $\tyof {e_1} {\Refine {e_0,t} {\Gamma'}} \leq \tyof {e_1} {\Refine {e_0,t} {\Gamma}}$.

            We proceed the same way for the last premise.
          \end{description}\ \\

          Now, let's prove the second property.
          We perform a (nested) induction on $\varpi$.

627
          Recall that we have $\forall t_1,t_2,\ts_1,\ts_2.\ t_1 \leq t_2 \text{ and } \ts_1\leq\ts_2 \text{ and } \tsrep{\ts_1}\leq\tsrep{\ts_2} \Rightarrow \tsrep{t_1\tsand\ts_1} \leq \tsrep{t_2\tsand\ts_2}$ (lemma above).
Giuseppe Castagna's avatar
Giuseppe Castagna committed
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
1001
1002
1003
1004
1005
1006
1007
1008
1009
1010
1011
1012
1013
1014
1015
1016
1017
1018
1019
1020
1021
1022
1023
1024
1025
1026
1027
1028
1029
1030
1031
1032
1033
1034
1035
1036
1037

          Thus, in order to prove
          $\tsrep {\constr {\varpi} {\Gamma',e,t} \tsand \tyof {\occ e \varpi} {\Gamma'}} \leq \tsrep {\constr {\varpi} {\Gamma,e,t} \tsand \tyof {\occ e \varpi} {\Gamma}}$,
          we can prove the following:
          \begin{align*}
            &\constr {\varpi} {\Gamma',e,t} \leq \constr {\varpi} {\Gamma,e,t}\\
            &\tyof {\occ e \varpi} {\Gamma'} \leq \tyof {\occ e \varpi} {\Gamma}\\
            &\tsrep{\tyof {\occ e \varpi} {\Gamma'}} \leq \tsrep{\tyof {\occ e \varpi} {\Gamma}}
          \end{align*}

          The two last inequalities can be proved
          with the outer induction hypothesis (for $\varpi=\epsilon$ we use the proof of the first property above).

          Thus we just have to prove that $\constr {\varpi} {\Gamma',e,t} \leq \constr {\varpi} {\Gamma,e,t}$.
          The only case that is interesting is the case $\varpi=\varpi'.1$.

          First, we can notice that the $\worra {} {}$ operator is monotonic for its second argument
          (consequence of its declarative definition).

          Secondly, let's show that for any function types $t_1 \leq t_2$, and for any type $t'$,
          we have $(\worra {t_1} {t'}) \land \dom {t_2} \leq \worra {t_2} {t'}$. By the absurd, let's suppose it is not true.
          Let's note $t'' = (\worra {t_1} {t'}) \land \dom {t_2}$.
          Then we have $t'' \leq \dom {t_2} \leq \dom {t_1}$ and $t_2 \leq \arrow {t''} {t'}$ and
          $t_1 \not\leq \arrow {t''} {t'}$, which contradicts $t_1 \leq t_2$.

          Let's note $t_1 = \tsrep {\tyof{\occ e{\varpi'.0}}{\Gamma'}}$ and $t_2 = \tsrep {\tyof{\occ e{\varpi'.0}}\Gamma}$
          and $t'=\env {\Gamma,e,t} (\varpi')$.
          As $e$ is well-typed, and using the inner induction hypothesis, we have $\tsrep {\tyof {\occ e {\varpi'.1}} {\Gamma'}} \leq \tsrep {\tyof {\occ e {\varpi'.1}} {\Gamma}} \leq \dom {t_2}$.\\
          Thus, using this property, we get:\\
          \begin{align*}
          &(\worra {t_1} {t'}) \land \tsrep {\tyof {\occ e {\varpi'.1}} {\Gamma'}}\\
          \leq &(\worra {t_2} {t'}) \land \tsrep {\tyof {\occ e {\varpi'.1}} {\Gamma}}
          \end{align*}

          Then, using the monotonicity of the second argument of $\worra {}{}$ and the outer induction hypothesis:
          \begin{align*}
            &(\worra {t_1} {\env {\Gamma',e,t} (\varpi')}) \land \tsrep {\tyof {\occ e {\varpi'.1}} {\Gamma'}}\\
            \leq &(\worra {t_2} {\env {\Gamma,e,t} (\varpi')}) \land \tsrep {\tyof {\occ e {\varpi'.1}} {\Gamma}}
          \end{align*}
          \\

          \

          Finally, we must prove the third property.\\
          It is straightforward by using the previous result and the induction hypothesis:\\
          $\forall e'$ s.t. $\exists \varpi.\ \occ e \varpi \equiv e'$, we get
          $\bigwedge_{\{\varpi\alt \occ e \varpi \equiv e'\}} \env {\Gamma',e,t} (\varpi) \leq \bigwedge_{\{\varpi\alt \occ e \varpi \equiv e'\}} \env {\Gamma,e,t} (\varpi)$.

          The rest follows.
          \end{proof}

          \begin{definition}[Positive derivation]
            A derivation of the declarative type system is said positive iff it does not contain any rule \Rule{Abs-}.
          \end{definition}

          \begin{theorem}[Completeness for positive derivations]\label{completenessAtsPositive}
            For every $\Gamma$, $e$, $t$ such that we have a positive derivation of $\Gamma \vdash e:t$,
            there exists a global parameter $n_o$ with which $\tsrep{\tyof e \Gamma} \leq t$.

            More precisely:
            \begin{align*}
              &\forall \Gamma, e, t.\ \Gamma \vdash e:t \text{ has a positive derivation } \Rightarrow \tsrep{\tyof e \Gamma} \leq t\\
              &\forall \Gamma, \Gamma', e, t.\ \Gamma \evdash e t \Gamma' \text{ has a positive derivation } \Rightarrow \Refine {e,t} \Gamma \leqA \Gamma' \text{ (for $n_o$ large enough)}
            \end{align*}
          \end{theorem}

          \begin{proof}
          We proceed by induction on the derivation.

          Let's prove the first property. We have a positive derivation of $\Gamma \vdash e:t$.

          If $\Gamma = \bot$, we can conclude directly using \Rule{Efq\Aats}. Thus, let's suppose $\Gamma \neq \bot$.

          If $e=x$ is a variable, then the derivation only uses \Rule{Env}, \Rule{Inter} and \Rule{Subs}.
          We can easily conclude just be using \Rule{Var\Aats}. Thus, let's suppose $e$ is not a variable.

          If $e\in\dom\Gamma$, we can have the rule \Rule{Env} applied to $e$ in our derivation, but in this case
          there can only be \Rule{Inter} and \Rule{Subs} after it (not \Rule{Abs-} as we have a positive derivation).
          Thus, our derivation contains a derivation of $\Gamma \vdash e:t'$ that does not use the rule \Rule{Env} on $e$
          and such that $t'\land \Gamma(e) \leq t$ (actually, it is possible for our derivation to typecheck $e$ only using the rule \Rule{Env}:
          in this case we can take $t'=\Any$ and use the fact that $\Gamma$ is well-formed).
          Hence, we can build a positive derivation for $\Gamma\setminus\{e\} \vdash e:t'$.
          By using the induction hypothesis we deduce that $\tsrep{\tyof e {\Gamma\setminus\{e\}}} \leq t'$.
          Thus, by looking at the rule \Rule{Env\Aats},
          we deduce $\tsrep{\tyof e \Gamma} \leq \Gamma(e) \land \tsrep{\tyof e {\Gamma\setminus\{e\}}} \leq t$.
          It concludes this case, so let's assume $e\not\in\dom\Gamma$.

          Now we analyze the last rule of the derivation:

          \begin{description}
            \item[\Rule{Env}] Impossible case ($e\not\in\dom\Gamma$).
            \item[\Rule{Inter}] By using the induction hypothesis we get $\tsrep{\tyof e \Gamma} \leq t_1$ and $\tsrep{\tyof e \Gamma} \leq t_2$.
            Thus, we have $\tsrep{\tyof e \Gamma} \leq t_1 \land t_2$.
            \item[\Rule{Subs}] Trivial using the induction hypothesis.
            \item[\Rule{Const}] We know that the derivation of $\tyof e \Gamma$ (if any) ends with the rule \Rule{Const\Aats}.
            Thus this case is trivial.
            \item[\Rule{App}] We know that the derivation of $\tyof e \Gamma$ (if any) ends with the rule \Rule{App\Aats}.
            Let $\ts_1 = \tyof {e_1} \Gamma$ and $\ts_2 = \tyof {e_2} \Gamma$.
            With the induction hypothesis we have $\tsrep {\ts_1} \leq \arrow {t_1} {t_2}$ and $\tsrep {\ts_2} \leq t_1$, with $t_2=t$.
            According to the descriptive definition of $\apply{}{}$, we have
            $\apply{\tsrep {\ts_1}}{\tsrep {\ts_2}} \leq \apply{\arrow {t_1}{t_2}}{t_1} \leq t_2$.
            As we also have $\tsrep{\apply {\ts_1} {\ts_2}} \leq \apply{\tsrep {\ts_1}}{\tsrep {\ts_2}}$,
            we can conclude that $\tyof e \Gamma \leq t_2=t$.

            \item[\Rule{Abs+}] We know that the derivation of $\tyof e \Gamma$ (if any) ends with the rule \Rule{Abs\Aats}.
            This case is straightforward using the induction hypothesis.
            \item[\Rule{Abs-}] This case is impossible (the derivation is positive).
            \item[\Rule{Case}] We know that the derivation of $\tyof e \Gamma$ (if any) ends with the rule \Rule{Case\Aats}.
            By using the induction hypothesis and the monotonicity lemma, we get $\tsrep{\ts_1}\leq t$ and $\tsrep{\ts_2}\leq t$.
            So we have $\tsrep{\ts_1\tsor\ts_2}=\tsrep{\ts1}\vee\tsrep{\ts2}\leq t$.
            \item[\Rule{Proj}] Quite similar to the case \Rule{App}.
            \item[\Rule{Pair}] We know that the derivation of $\tyof e \Gamma$ (if any) ends with the rule \Rule{Pair\Aats}.
            We just use the induction hypothesis and the fact that $\tsrep{\ts_1\tstimes\ts_2}=\pair {\tsrep{\ts1}} {\tsrep{\ts2}}$.
          \end{description}

          \

          Now, let's prove the second property. We have a positive derivation of $\Gamma \evdash e t \Gamma'$.

          \begin{description}
            \item[\Rule{Base}] Any value of $n_o$ will give $\Refine {e,t} \Gamma \leqA \Gamma$, even $n_o = 0$.
            \item[\Rule{Path}] We have $\Gamma' = \Gamma_1,(\occ e \varpi:t')$.
            By applying the induction hypothesis on the premise $\Gamma \evdash e t \Gamma_1$, we have
            $\RefineStep {e,t}^n (\Gamma) = \Gamma_2$ with $\Gamma_2 \leqA \Gamma_1$ for a certain $n$.

            We now proceed by induction on the derivation $\pvdash {\Gamma_1} e t \varpi:t'$
            to show that we can obtain $\env {\Gamma'',e,t} (\varpi) \leq t'$ with $\Gamma'' = \RefineStep {e,t}^{n'} (\Gamma_2)$
            for a certain $n'$. It is then easy to conclude by taking $n_o = n+n'$.

            \begin{description}
              \item[\Rule{PSubs}] Trivial using the induction hypothesis.
              \item[\Rule{PInter}] By using the induction hypothesis we get:
              \begin{align*}
                &\env {\Gamma_1'',e,t} (\varpi) \leq t_1\\
                &\env {\Gamma_2'',e,t} (\varpi) \leq t_2\\
                &\RefineStep {e,t}^{n_1} (\Gamma_1) \leqA \Gamma_1''\\
                &\RefineStep {e,t}^{n_2} (\Gamma_2) \leqA \Gamma_2''
              \end{align*}

              By taking $n'=\max (n_1,n_2)$,
              we can have $\Gamma'' = \RefineStep {e,t}^{n'} (\Gamma_2)$ with $\Gamma'' \leqA \Gamma_1''$ and $\Gamma'' \leqA \Gamma_2''$.
              Thus, by using the monotonicity lemma, we can obtain $\env {\Gamma'',e,t} (\varpi) \leq t_1 \land t_2 = t'$.
              \item[\Rule{PTypeof}] By using the outer induction hypothesis we get
              $\tsrep{\tyof {\occ e \varpi} {\Gamma_2}} \leq t'$.
              Moreover we have $\env {\Gamma_2,e,t} (\varpi) \leq \tsrep{\tyof {\occ e \varpi} {\Gamma_2}}$
              (by definition of $\env {}$), thus we can conclude directly.
              \item[\Rule{PEps}] Trivial.
              \item[\Rule{PAppR}] By using the induction hypothesis we get:
              \begin{align*}
                &\env {\Gamma_1'',e,t} (\varpi.0) \leq \arrow {t_1} {t_2}\\
                &\env {\Gamma_2'',e,t} (\varpi) \leq t_2'\\
                & t_2\land t_2' \simeq \Empty\\
                &\RefineStep {e,t}^{n_1} (\Gamma_1) \leqA \Gamma_1''\\
                &\RefineStep {e,t}^{n_2} (\Gamma_2) \leqA \Gamma_2''
              \end{align*}

              By taking $n'=\max (n_1,n_2) + 1$,
              we can have $\Gamma'' = \RefineStep {e,t}^{n'} (\Gamma_2)$ with $\Gamma'' \leqA \RefineStep {e,t} (\Gamma_1'')$
              and $\Gamma'' \leqA \RefineStep {e,t} (\Gamma_2'')$.

              In consequence, we have $\tsrep{\tyof {\occ e {\varpi.0}} {\Gamma''}} \leq \env {\Gamma_1'',e,t} (\varpi.0) \leq \arrow {t_1} {t_2}$
              (by definition of $\RefineStep {e,t}$).
              We also have, by monotonicity, $\env {\Gamma'',e,t} (\varpi) \leq t_2'$.

              As $t_2\land t_2' \simeq \Empty$, we have:
              \begin{align*}
                &\apply {(\arrow {t_1} {t_2})} {(\dom{\arrow {t_1} {t_2}}\setminus(\neg t_1))}\\
                &\simeq \apply {(\arrow {t_1} {t_2})} {t_1} \simeq t_2 \leq \neg t_2'
              \end{align*}

              Thus, by using the declarative definition of $\worra {} {}$, we know that
              $\worra {(\arrow {t_1} {t_2})} {t_2'} \leq \neg t_1$.

              According to the properties on $\worra {} {}$ that we have proved in the proof of the monotonicity lemma,
              we can deduce:
              \begin{align*}
              &t_1 \land \worra {\tsrep{\tyof {\occ e {\varpi.0}} {\Gamma''}}} {\env {\Gamma'',e,t} (\varpi)}\\
              &\leq t_1 \land \worra {(\arrow {t_1} {t_2})} {t_2'} \leq t_1 \land \neg t_1 \simeq \Empty
              \end{align*}
              And thus $\worra {\tsrep{\tyof {\occ e {\varpi.0}} {\Gamma''}}} {\env {\Gamma'',e,t} (\varpi)} \leq \neg t_1$.

              It concludes this case.

              \item[\Rule{PAppL}] By using the induction hypothesis we get:
              \begin{align*}
                &\env {\Gamma_1'',e,t} (\varpi.1) \leq t_1\\
                &\env {\Gamma_2'',e,t} (\varpi) \leq t_2\\
                &\RefineStep {e,t}^{n_1} (\Gamma_1) \leqA \Gamma_1''\\
                &\RefineStep {e,t}^{n_2} (\Gamma_2) \leqA \Gamma_2''
              \end{align*}

              By taking $n'=\max (n_1,n_2)$,
              we can have $\Gamma'' = \RefineStep {e,t}^{n'} (\Gamma_2)$ with $\Gamma'' \leqA \Gamma_1''$ and $\Gamma'' \leqA \Gamma_2''$.
              Thus, by using the monotonicity lemma, we can obtain $\env {\Gamma'',e,t} (\varpi.0) \leq \neg (\arrow {t_1} {\neg t_2}) = t'$.

              \item[\Rule{PPairL}] Quite straightforward using the induction hypothesis and the descriptive definition of $\bpi_1$.
              \item[\Rule{PPairR}] Quite straightforward using the induction hypothesis and the descriptive definition of $\bpi_2$.
              \item[\Rule{PFst}] Trivial using the induction hypothesis.
              \item[\Rule{PSnd}] Trivial using the induction hypothesis.
            \end{description}
          \end{description}
          \end{proof}

          From this result, we will now prove a stronger but more complex completeness theorem.
          We were not able to prove full completeness, just a partial form of it. Indeed,
          the use of nested \Rule{PAppL} yields a precision that the algorithm loses by applying \tsrep{}
          in the definition of \constrf{}. Completeness is recovered by forbidding nested negated arrows on the
          left-hand side of negated arrows.

          \begin{definition}[Rank-0 negated derivation]
            A derivation of the declarative type system is said rank-0 negated iff any application of \Rule{PAppL}
            has a positive derivation as first premise ($\pvdash \Gamma e t \varpi.1:t_1$).
          \end{definition}

          \noindent The use of this terminology is borrowed from the ranking of higher-order
          types, since, intuitively, it corresponds to typing a language in
          which  in the types used in dynamic tests, a negated arrow never occurs  on the
          left-hand side of another negated arrow.

          \begin{lemma}
            If $e$ is an application, then $\tyof e \Gamma$ does not contain any constructor $\tsfun \cdots$.
            Consequently, we have $\tsrep{\tyof e \Gamma} \simeq \tyof e \Gamma$.
          \end{lemma}

          \begin{proof}
            By case analysis: neither \Rule{Efq\Aats}, \Rule{Env\Aats} nor \Rule{App\Aats} can produce a type
            containing a constructor $\tsfun \cdots$.
          \end{proof}

          \begin{theorem}[Completeness for rank-0 negated derivations]
            For every $\Gamma$, $e$, $t$ such that we have a rank-0 negated derivation of $\Gamma \vdash e:t$, there exists a global parameter $n_o$
            with which $\tyof e \Gamma \leq t$.

            More precisely:
            \begin{align*}
              &\forall \Gamma, e, t.\ \Gamma \vdash e:t \text{ has a rank-0 negated derivation } \Rightarrow \tyof e \Gamma \leq t\\
              &\forall \Gamma, \Gamma', e, t.\ \Gamma \evdash e t \Gamma' \text{ has a rank-0 negated derivation } \Rightarrow \Refine {e,t} \Gamma \leqA \Gamma' \text{ (for $n_o$ large enough)}
            \end{align*}
          \end{theorem}

          \begin{proof}
            This proof is done by induction. It is quite similar to that of the completeness for positive derivations.
            In consequence, we will only detail cases that are quite different from those of the previous proof.

            Let's begin with the first property. We have a rank-0 negated derivation of $\Gamma \vdash e:t$.
            We want to show $\tyof e \Gamma \leq t$ (note that this is weaker than showing $\tsrep {\tyof e \Gamma} \leq t$).

            As in the previous proof, we can suppose that $\Gamma \neq \bot$ and that $e$ is not a variable.

            The case $e\in\dom\Gamma$ is also very similar, but there is an additional case to consider:
            the rule \Rule{Abs-} could possibly be used after a rule \Rule{Env} applied on $e$.
            However, this case can easily be eliminated by changing the premise of this \Rule{Abs-} with another one
            that does not use the rule \Rule{Env} on $e$ (the type of the premise does not matter for the rule \Rule{Abs-},
            even $\Any$ suffices). Thus let's assume $e\not\in\dom\Gamma$.

            Now we analyze the last rule of the derivation (only the cases that are not similar are shown):
            \begin{description}
              \item[\Rule{Abs-}] We know that the derivation of $\tyof e \Gamma$ (if any) ends with the rule \Rule{Abs\Aats}.
              Moreover, by using the induction hypothesis on the premise, we know that $\tyof e \Gamma \neq \tsempty$.
              Thus we have $\tyof e \Gamma \leq \neg (\arrow {t_1} {t_2}) = t$ (because every type $\neg (\arrow {s'} {t'})$
              such that $\neg (\arrow {s'} {t'}) \land \bigwedge_{i\in I} \arrow {s_i} {t_i} \neq \Empty$ is in $\tsint{\tsfun{\arrow {s_i} {t_i}}}$).
            \end{description}

            \

            Now let's prove the second property. We have a rank-0 negated derivation of $\Gamma \evdash e t \Gamma'$.

            \begin{description}
              \item[\Rule{Base}] Any value of $n_o$ will give $\Refine {e,t} \Gamma \leqA \Gamma$, even $n_o = 0$.
              \item[\Rule{Path}] We have $\Gamma' = \Gamma_1,(\occ e \varpi:t')$.

              As in the previous proof of completeness,
              by applying the induction hypothesis on the premise $\Gamma \evdash e t \Gamma_1$, we have
              $\RefineStep {e,t}^n (\Gamma) = \Gamma_2$ with $\Gamma_2 \leqA \Gamma_1$ for a certain $n$.

              However, this time, we can't prove $\env {\Gamma'',e,t} (\varpi) \leq t'$ with $\Gamma'' = \RefineStep {e,t}^{n'} (\Gamma_2)$
              for a certain $n'$: the induction hypothesis is weaker than in the previous proof
              (we don't have $\tsrep {\tyof e \Gamma} \leq t$ but only $\tyof e \Gamma \leq t$).

              Instead, we will prove by induction on the derivation $\pvdash {\Gamma_1} e t \varpi:t'$ that
              $\env {\Gamma'',e,t} (\varpi) \tsand \tyof {\occ e \varpi} {\Gamma''} \leq t'$.
              It suffices to conclude in the same way as in the previous proof:
              by taking $n_o = n+n'$,
              it ensures that our final environment $\Gamma_{n_o}$ verifies $\tyof {\occ e \varpi} \Gamma_{n_o} \leq t'$
              and thus we have $\Gamma_{n_o} \leq \Gamma'$
              (given that $\tsrep{\Empty} = \Empty$, we also easily verify that if $\Gamma' = \bot \Rightarrow \Gamma_{n_o}=\bot$).

              \begin{description}
                \item[\Rule{PSubs}] Trivial using the induction hypothesis.
                \item[\Rule{PInter}] Quite similar to the previous proof (the induction hypothesis is weaker, but it works the same way).
                \item[\Rule{PTypeof}] By using the outer induction hypothesis we get $\tyof {\occ e \varpi} {\Gamma_2} \leq t'$ so it is trivial.
                \item[\Rule{PEps}] Trivial.
                \item[\Rule{PAppR}] By using the induction hypothesis, we get:
                \begin{align*}
                  &\env {\Gamma_1'',e,t} (\varpi.0) \tsand \tyof {\occ e {\varpi.0}} {\Gamma_1''} \leq \arrow {t_1} {t_2}\\
                  &\env {\Gamma_2'',e,t} (\varpi) \tsand \tyof {\occ e {\varpi}} {\Gamma_2''} \leq t_2'\\
                  &t_2 \land t_2' \simeq \Empty\\
                  &\RefineStep {e,t}^{n_1} (\Gamma_1) \leqA \Gamma_1''\\
                  &\RefineStep {e,t}^{n_2} (\Gamma_2) \leqA \Gamma_2''
                \end{align*}

                Moreover, as $\occ e {\varpi}$ is an application, we can use the lemma above to deduce
                $\env {\Gamma_2'',e,t} (\varpi) \tsand \tyof {\occ e {\varpi}} {\Gamma_2''} = \env {\Gamma_2'',e,t} (\varpi)$
                (see definition of $\env {}$).

                Thus we have $\env {\Gamma_2'',e,t} (\varpi) \leq t_2'$.\\
                We also have $\env {\Gamma_1'',e,t} (\varpi.0) \leq \tsrep{\env {\Gamma_1'',e,t} (\varpi.0) \tsand \tyof {\occ e {\varpi.0}} {\Gamma_1''}} \leq \arrow {t_1} {t_2}$.

                Now we can conclude exactly as in the previous proof (by taking $n'=\max (n_1,n_2)$).

                \item[\Rule{PAppL}] We know that the left premise is a positive derivation.
                Thus, using the previous completeness theorem, we get:
                \begin{align*}
                  &\env {\Gamma_1'',e,t} (\varpi.1) \leq t_1\\
                  &\RefineStep {e,t}^{n_1} (\Gamma_1) \leqA \Gamma_1''
                \end{align*}

                By using the induction hypothesis, we also get:
                \begin{align*}
                  &\env {\Gamma_2'',e,t} (\varpi) \tsand \tyof {\occ e {\varpi}} {\Gamma_2''} \leq t_2\\
                  &\RefineStep {e,t}^{n_2} (\Gamma_2) \leqA \Gamma_2''
                \end{align*}

                Moreover, as $\occ e {\varpi}$ is an application, we can use the lemma above to deduce
                $\env {\Gamma_2'',e,t} (\varpi) \tsand \tyof {\occ e {\varpi}} {\Gamma_2''} = \env {\Gamma_2'',e,t} (\varpi)$
                (see definition of $\env {}$).

                Thus we have $\env {\Gamma_2'',e,t} (\varpi) \leq t_2$.

                Now we can conclude exactly as in the previous proof (by taking $n'=\max (n_1,n_2)$).

                \item[\Rule{PPairL}] Quite straightforward using the induction hypothesis and the descriptive definition of $\bpi_1$.
                \item[\Rule{PPairR}] Quite straightforward using the induction hypothesis and the descriptive definition of $\bpi_2$.
                \item[\Rule{PFst}] Quite straightforward using the induction hypothesis.
                \item[\Rule{PSnd}] Quite straightforward using the induction hypothesis.
              \end{description}
            \end{description}
          \end{proof}

    \subsection{Proofs for the algorithmic type system without type
      schemes}
    \label{sec:proofs_algorithmic_without_ts}

    In this section, we consider the algorithmic type system without type schemes, as defined in \ref{sec:algorules}.

    \subsubsection{Soundness}

    \begin{lemma}
      \label{soundness_simple_ts}
    For every $\Gamma$, $e$, $t$, $n_o$, if $\Gamma\vdashA e: t$, then there exists $\ts \leq t$ such that $\Gamma \vdashAts e: \ts$.
    \end{lemma}

    \begin{proof}
      Straightforward induction over the structure of $e$.
    \end{proof}

    \begin{theorem}[Soundness of the algorithmic type system without type schemes]\label{soundnessA}
    For every $\Gamma$, $e$, $t$, $n_o$, if $\Gamma\vdashA e: t$, then $\Gamma \vdash e:t$.
    \end{theorem}

    \begin{proof}
      Trivial by using the theorem \ref{soundnessAts} and the previous lemma.
    \end{proof}

    \subsubsection{Completeness}

    \[
      \begin{array}{lrcl}
        \textbf{Simple type} & t_{s} & ::= & b \alt \pair {t_{s}} {t_{s}} \alt t_{s} \vee t_{s} \alt \neg t_{s} \alt \Empty \alt \arrow \Empty \Any\\
        \textbf{Positive type} & t_+ & ::= & t_{s} \alt t_+ \vee t_+ \alt t_+ \land t_+ \alt \arrow {t_+} {t_+} \alt \arrow {t_+} {\neg t_+}\\
        \textbf{Positive abstraction type} & t^\lambda_+ & ::= & \arrow {t_+} {t_+} \alt \arrow {t_+} {\neg t_+} \alt t^\lambda_+ \land t^\lambda_+\\
        \textbf{Positive expression} & e_+ & ::= & c\alt x\alt e_+ e_+\alt\lambda^{t^\lambda_+} x.e_+\alt \pi_j e_+\alt(e_+,e_+)\alt\tcase{e_+}{t_{s}}{e_+}{e_+}
      \end{array}
    \]

    \begin{lemma}
      If we restrict the language to positive expressions $e_+$,
      then we have the following property:

      $\forall \Gamma, e_+, \ts.\ \Gamma \vdashAts e_+:\ts \Rightarrow \Gamma \vdashA e_+:\tsrep{\ts}$
    \end{lemma}

    \begin{proof}
      We can prove it by induction over the structure of $e_+$.

      The main idea of this proof is that, as $e_+$ is a positive expression, the rule \Rule{Abs-} is not needed anymore
      because the negative part of functional types (i.e. the $N_i$ part of their DNF) becomes useless:

      \begin{itemize}
        \item When typing an application $e_1 e_2$, the negative part of the type of $e_1$
        is ignored by the operator $\apply {} {}$.
        \item Moreover, as there is no negated arrows in the domain of lambda-abstractions,
        the negative arrows of the type of $e_2$ can also be ignored.
        \item Similarly, negative arrows can be ignored when refining an application ($\worra {} {}$ also ignore the negative part
        of the type of $e_1$).
        \item Finally, as the only functional type that we can test is $\arrow \Empty \Any$, a functional type
        cannot be refined to $\Empty$ due to its negative part, and thus we can ignore its negative part
        (it makes no difference relatively to the rule \Rule{Efq\Aats}).
      \end{itemize}
    \end{proof}

    \begin{theorem}[Completeness of the algorithmic type system for positive expressions]\label{completenessA}
      For every type environment $\Gamma$ and positive expression $e_+$, if
      $\Gamma\vdash e_+: t$, then there exist $n_o$ and  $t'$ such that $\Gamma\vdashA
      e_+: t'$.
    \end{theorem}

    \begin{proof}
      Trivial by using the theorem \ref{completenessAtsPositive} and the previous lemma.
    \end{proof}