Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Giuseppe Castagna
occurrence-typing
Commits
26b72929
Commit
26b72929
authored
Feb 28, 2020
by
Mickael Laurent
Browse files
add underscore notation for parallel reductions
parent
d0481fea
Changes
2
Hide whitespace changes
Inline
Side-by-side
proofs.tex
View file @
26b72929
...
...
@@ -183,6 +183,8 @@
{}
\end{mathpar}
We denote by
$
e
\uleadsto
e'
$
a step of reduction of the parallel semantic, regardless of the value on the top of the arrow.
\[
\valsemantic
t
=
\{
v
\alt
\vvdash
v : t
\}
\]
\begin{mathpar}
...
...
@@ -584,7 +586,7 @@
\begin{theorem}
[Subject reduction]
Let
$
\Gamma
$
an ordinary environment,
$
e
$
and
$
e'
$
two expressions and
$
t
$
a type.
If
$
\Gamma\vdash
e:t
$
and
$
e
\leadsto
e'
$
, then
$
\Gamma\vdash
e':t
$
.
If
$
\Gamma\vdash
e:t
$
and
$
e
\
u
leadsto
e'
$
, then
$
\Gamma\vdash
e':t
$
.
\end{theorem}
\begin{proof}
...
...
@@ -605,9 +607,9 @@
\item
[\Rule{Const}]
Impossible case (no reduction possible).
\item
[\Rule{App}]
In this case,
$
e
\equiv
e
_
1
e
_
2
$
. There are three possible cases:
\begin{itemize}
\item
$
e
_
2
$
is not a value. In this case, we must have
$
e
_
2
\leadsto
e
_
2
'
$
\item
$
e
_
2
$
is not a value. In this case, we must have
$
e
_
2
\
u
leadsto
e
_
2
'
$
and
$
e'
\equiv
e
_
1
e
_
2
'
$
. We can easily conclude using the induction hypothesis.
\item
$
e
_
2
$
is a value and
$
e
_
1
$
is not. In this case, we must have
$
e
_
1
\leadsto
e
_
1
'
$
\item
$
e
_
2
$
is a value and
$
e
_
1
$
is not. In this case, we must have
$
e
_
1
\
u
leadsto
e
_
1
'
$
and
$
e'
\equiv
e
_
1
' e
_
2
$
. We can easily conclude using the induction hypothesis.
\item
Both
$
e
_
1
$
and
$
e
_
2
$
are values. This is the difficult case.
We have
$
e
_
1
\equiv
\lambda
^{
\bigwedge
_{
i
\in
I
}
\arrow
{
s
_
i
}{
t
_
i
}}
x.e
_
x
$
...
...
@@ -642,11 +644,11 @@
\item
[\Rule{Abs-}]
Impossible case (no reduction possible).
\item
[\Rule{Proj}]
In this case,
$
e
\equiv
\pi
_
i e
_
0
$
. There are two possible cases:
\begin{itemize}
\item
$
e
_
0
$
is not a value. In this case, we must have
$
e
_
0
\leadsto
e
_
0
'
$
\item
$
e
_
0
$
is not a value. In this case, we must have
$
e
_
0
\
u
leadsto
e
_
0
'
$
and
$
e'
\equiv
\pi
_
i e
_
0
'
$
. We can easily conclude using the induction hypothesis.
\item
$
e
_
0
$
is a value.
Given that
$
e
_
0
\leq
\pair
\Any
\Any
$
, we have
$
e
_
0
=
(
v
_
1
,v
_
2
)
$
with
$
v
_
1
$
and
$
v
_
2
$
two values.
We also have
$
e
\leadsto
v
_
i
$
.
We also have
$
e
\
id
leadsto
v
_
i
$
.
The derivation of
$
\Gamma
\vdash
(
v
_
1
,v
_
2
)
:
\pair
{
t
_
1
}
{
t
_
2
}$
must contain a rule
\Rule
{
Pair
}
which guarantees
$
\Gamma
\vdash
v
_
i: t
_
i
$
(recall that
$
\Gamma
\neq
\bot
$
and
$
\Gamma
$
is ordinary so there is no pair in
$
\dom\Gamma
$
).
...
...
@@ -654,9 +656,9 @@
\end{itemize}
\item
[\Rule{Pair}]
In this case,
$
e
\equiv
(
e
_
1
,e
_
2
)
$
. There are two possible cases:
\begin{itemize}
\item
$
e
_
2
$
is not a value. In this case, we must have
$
e
_
2
\leadsto
e
_
2
'
$
\item
$
e
_
2
$
is not a value. In this case, we must have
$
e
_
2
\
u
leadsto
e
_
2
'
$
and
$
e'
\equiv
(
e
_
1
, e
_
2
'
)
$
. We can easily conclude using the induction hypothesis.
\item
$
e
_
2
$
is a value and
$
e
_
1
$
is not. In this case, we must have
$
e
_
1
\leadsto
e
_
1
'
$
\item
$
e
_
2
$
is a value and
$
e
_
1
$
is not. In this case, we must have
$
e
_
1
\
u
leadsto
e
_
1
'
$
and
$
e'
\equiv
(
e
_
1
', e
_
2
)
$
. We can easily conclude using the induction hypothesis.
\end{itemize}
\item
[\Rule{Case}]
In this case,
$
e
\equiv
\ite
{
e
_
0
}
{
t
_{
if
}}
{
e
_
1
}
{
e
_
2
}$
. There are three possible cases:
...
...
@@ -680,8 +682,8 @@
\end{itemize}
It can be easily proved by induction on the derivation of the reduction step.
Secondly, as
$
e
_
a
\leadsto
e
_
b
$
and as the derivation of this reduction is a strict subderivation of that of
$
e
\leadsto
e'
$
,
we can use the induction hypothesis on
$
e
_
a
\leadsto
e
_
b
$
and we obtain
$
\forall
t'.
\ \Gamma
\vdash
e
_
a : t'
\Rightarrow
\Gamma\rho
\vdash
e
_
b:t'
$
.
Secondly, as
$
e
_
a
\
u
leadsto
e
_
b
$
and as the derivation of this reduction is a strict subderivation of that of
$
e
\
u
leadsto
e'
$
,
we can use the induction hypothesis on
$
e
_
a
\
u
leadsto
e
_
b
$
and we obtain
$
\forall
t'.
\ \Gamma
\vdash
e
_
a : t'
\Rightarrow
\Gamma\rho
\vdash
e
_
b:t'
$
.
Thus, we can conclude directly by using the substitution lemma on
$
e
$
and
$
\rho
$
.
\end{itemize}
...
...
@@ -703,7 +705,7 @@
\end{proof}
\begin{theorem}
[Progress]
If
$
\varnothing
\vdash
e:t
$
, then either
$
e
$
is a value or there exists
$
e'
$
such that
$
e
\leadsto
e'
$
.
If
$
\varnothing
\vdash
e:t
$
, then either
$
e
$
is a value or there exists
$
e'
$
such that
$
e
\
u
leadsto
e'
$
.
\end{theorem}
\begin{proof}
...
...
setup.sty
View file @
26b72929
...
...
@@ -154,6 +154,7 @@
\newcommand
{
\reduces
}{
\leadsto
}
\newcommand
{
\xleadsto
}
[1]
{
\overset
{
#1
}{
\leadsto
}}
\newcommand
{
\idleadsto
}
[0]
{
\xleadsto
{
Id
}}
\newcommand
{
\uleadsto
}
[0]
{
\xleadsto
{
\large
{
\textbf
{
\_
}}}}
\newcommand
{
\values
}
[0]
{
\mathcal
{
V
}}
\newcommand
{
\valsemantic
}
[1]
{{
\llbracket
#1
\rrbracket
}_{
\values
}}
\newcommand
{
\vvdash
}
[0]
{
\vdash
_
\values
}
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment