Commit 674c6ec0 authored by Kim Nguyễn's avatar Kim Nguyễn
Browse files

Fix appendix and references to the appendix.

parent 0b36acea
......@@ -29,7 +29,7 @@ need to define some operators on types, which are given in
Section~\ref{sec:typeops}. The second origin is the rule \Rule{Abs-}
by which it is possible to deduce for every well-typed lambda
abstraction infinitely many types, that is the annotation of the
function intersected with as many negations of arrow types as
function intersected with as many negations of arrow types as
possible without making the type empty. We do not handle this
multiplicity directly in the algorithmic system but only in the proof
of its soundness by using and adapting the technique of \emph{type
......@@ -38,11 +38,11 @@ representations of the infinite sets of types of
$\lambda$-abstractions which can be used to define an algorithmic
system that can be easily proved to be sound. The simpler algorithm
that we propose in this section implies (i.e., it is less precise than) the one with type schemes (cf.\
Theorem~\ref{????}) and it is thus sound, too. The algorithm of this
section is not only simpler but, as we discuss in Section~\ref{???},
Lemma~\ref{soundness_simple_ts}) and it is thus sound, too. The algorithm of this
section is not only simpler but, as we discuss in Section~\ref{???}\kim{Where?},
is also the one that should be used in practice. This is why we preferred to
present it here and relegate the presentation of type schemes to
$(ii)$. For what concerns the use of the auxiliary derivation for the $\Gamma \evdash e t \Gamma' $ and $\pvdash \Gamma e t \varpi:t'$
judgments, we present in Section~\ref{sec:typenv} an algorithm that is sound and satisfies a limited form of
......@@ -79,7 +79,7 @@ the function has a functional type is easy since it corresponds to
checking that it has a type subtype of $\Empty{\to}\Any$. Determining
its domain and the type of the application is more complicated and needs the operators $\dom{}$ and $\circ$ we informally described in Section~\ref{sec:ideas} where we also introduced the operator $\worra{}{}$. These three operators are used by our algorithm and formally defined as:\vspace{-2mm}
\dom t & = & \max \{ u \alt t\leq u\to \Any\}
\dom t & = & \max \{ u \alt t\leq u\to \Any\}
\apply t s & = &\,\min \{ u \alt t\leq s\to u\}
......@@ -118,7 +118,7 @@ $i$ in $I$. For such a $t$ and any type $s$ then we have:\vspace{-1.7mm}
The formula considers only the positive arrows of each summand that
forms $t$ and states that, for each summand, whenever you take a subset
$P$ of its positive arrows that cannot yield results in
$P$ of its positive arrows that cannot yield results in
$s$ (since $s$ does not overlap the intersection of the codomains of these arrows), then
the success of the test cannot depend on these arrows and therefore
the intersection of the domains of these arrows---i.e., the values that would precisely select that set of arrows---can be removed from $\dom t$. The proof
......@@ -134,7 +134,7 @@ deduction of $\Gamma \evdash e t \Gamma'$, that is an algorithm that
takes as input $\Gamma$, $e$, and $t$, and returns an environment that
extends $\Gamma$ with hypotheses on the occurrences of $e$ that are
the most general that can be deduced by assuming that $e\,{\in}\,t$ succeeds. For that we need the notation $\tyof{e}{\Gamma}$ which denotes the type deduced for $e$ under the type environment $\Gamma$ in the algorithmic type system of Section~\ref{sec:algorules}.
That is, $\tyof{e}{\Gamma}=t$ if and only if $\Gamma\vdashA e:t$ is provable.
That is, $\tyof{e}{\Gamma}=t$ if and only if $\Gamma\vdashA e:t$ is provable.
We start by defining the algorithm for each single occurrence, that is for the deduction of $\pvdash \Gamma e t \varpi:t'$. This is obtained by defining two mutually recursive functions $\constrf$ and $\env{}{}$:\vspace{-1.3mm}
......@@ -160,7 +160,11 @@ in the definition are defined).\footnote{Note that the definition is
$\Gamma$ the type of every occurrence of $e$.)\vspace{-3mm}}
Each case of the definition of the $\constrf$ function corresponds to the
application of a logical rule (\emph{cf.} Footnote~\ref{fo:rules}) in
application of a logical rule
(\emph{cf.} Footnote~\ref{fo:rules})
the deduction system for $\vdashp$: case \eqref{uno} corresponds
to the application of \Rule{PEps}; case \eqref{due} implements \Rule{Pappl}
straightforwardly; the implementation of rule \Rule{PAppR} is subtler:
......@@ -236,7 +240,7 @@ $\dom{\Refine{e,t}\Gamma} = \dom{\RefineStep {e,t}(\Gamma)} = \dom{\Gamma} \cup
In other terms, we try to find a fixpoint of $\RefineStep{e,t}$ but we
bound our search to $n_o$ iterations. Since $\RefineStep {e,t}$ is
monotone (w.r.t.\ the subtyping pre-order extended to type environments pointwise), then
every iteration yields a better solution.
every iteration yields a better solution.
While this is unsatisfactory from a formal point of view, in practice
the problem is a very mild one. Divergence may happen only when
......@@ -358,14 +362,14 @@ The algorithmic system above is sound with respect to the deductive one of Secti
For every $\Gamma$, $e$, $t$, $n_o$, if $\Gamma\vdashA e: t$, then $\Gamma \vdash e:t$.
The proof of this theorem (see Appendix~\ref{}) is obtained by
The proof of this theorem (see Appendix~\ref{sec:proofs_algorithmic_without_ts}) is obtained by
defining an algorithmic system $\vdashAts$ that uses type schemes,
that is, which associates each typable term $e$ with a possibly
infinite set of types $\ts$ (in particular a $\lambda$-expression
$\lambda^{\wedge_{i\in I}\arrow {s_i} {t_i}}x.e$ will
be associated to a set of types of the form $\{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'}).\
\land \bigwedge_{j=1..m} \neg (\arrow {t_j'} {s_j'}).\
\Empty \not\simeq s_0 \leq s \}$) and proving that, if
$\Gamma\vdashA e: t$ then $\Gamma\vdashAts e: \ts$ with
$t\in\ts$: the soundness of $\vdashA$ follows from the soundness
......@@ -424,7 +428,7 @@ left-hand side of negated arrows.\vspace{-.7mm}
\begin{definition}[Rank-0 negation]
A derivation of $\Gamma \vdash e:t$ is \emph{rank-0 negated} if
\Rule{Abs--} never occurs in the derivation of a left premise of a
\Rule{PAppL} rule.\vspace{-.7mm}
\Rule{PAppL} rule.\vspace{-.7mm}
\noindent The use of this terminology is borrowed from the ranking of higher-order
types, since, intuitively, it corresponds to typing a language in
......@@ -312,3 +312,25 @@ series = {POPL ’12}
@article{levy2017, title={Redexes are stable in the $\lambda$-calculus},
volume={27}, DOI={10.1017/S0960129515000353},
number={5}, journal={Mathematical Structures in
Computer Science}, publisher={Cambridge University
Press}, author={LÉVY, JEAN-JACQUES}, year={2017},
title = "Parallel reductions in $\lambda$-calculus",
journal = "Journal of Symbolic Computation",
volume = "7",
number = "2",
pages = "113 - 123",
year = "1989",
issn = "0747-7171",
doi = "",
url = "",
author = "Masako Takahashi",
abstract = "The notion of parallel reduction is extracted from the Tait-Martin-Löf proof of the Church-Rosser theorem (for β-reduction). We define parallel β-, η- and βη-reduction by induction, and use them to give simple proofs of some fundamental theorems in λ-calculus; the normal reduction theorem for β-reduction, that for βη-reduction, the postponement theorem of η-reduction (in βη-reduction), and some others."
\ No newline at end of file
This diff is collapsed.
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment