Skip to content
Projects
Groups
Snippets
Help
Loading...
Help
Support
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
H
hor2019
Project overview
Project overview
Details
Activity
Releases
Repository
Repository
Files
Commits
Branches
Tags
Contributors
Graph
Compare
Issues
0
Issues
0
List
Boards
Labels
Milestones
Merge Requests
0
Merge Requests
0
CI / CD
CI / CD
Pipelines
Jobs
Schedules
Analytics
Analytics
CI / CD
Repository
Value Stream
Wiki
Wiki
Snippets
Snippets
Members
Members
Collapse sidebar
Close sidebar
Activity
Graph
Create a new issue
Jobs
Commits
Issue Boards
Open sidebar
Guillaume GENESTIER
hor2019
Commits
23c38922
Commit
23c38922
authored
Jun 20, 2019
by
Guillaume GENESTIER
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Corrections Olivier
parent
e10c88ff
Changes
1
Hide whitespace changes
Inline
Side-by-side
Showing
1 changed file
with
29 additions
and
29 deletions
+29
-29
Slides/SlidesFSCD.tex
Slides/SlidesFSCD.tex
+29
-29
No files found.
Slides/SlidesFSCD.tex
View file @
23c38922
...
...
@@ -102,7 +102,7 @@
\definecolor
{
bleufonce
}{
RGB
}{
0,0,130
}
\definecolor
{
blue-violet
}{
rgb
}{
0.54, 0.17, 0.89
}
\newcommand
{
\bto
}{
{
\color
{
blue
}
\to
}
}
\newcommand
{
\bto
}{
~
{
\color
{
blue
}
\to
}
~
}
\newcommand
{
\interp
}
[1]
{
\left\llbracket
#1
\right\rrbracket
}
...
...
@@ -112,12 +112,6 @@
\lstset
{
escapeinside=
{
@
}{
@
}}
\AtBeginSection
[]
{
\begin{frame}
\frametitle
{
Contents
}
\tableofcontents
[currentsection,hideothersubsections]
\end{frame}
}
\begin{document}
...
...
@@ -130,6 +124,12 @@
\section
{
Context:
\Dedukti
{}}
\AtBeginSection
[]
{
\begin{frame}
\frametitle
{
Contents
}
\tableofcontents
[currentsection,hideothersubsections]
\end{frame}
}
\begin{frame}
[fragile]
\frametitle
{
\emph
{
Dedukti
}}
\emph
{
Dedukti
}
is a type-checker for the
$
\lambda\Pi
$
-calculus modulo rewriting.
...
...
@@ -187,7 +187,7 @@ def sum : (n: Nat) -> F n
\end{frame}
\begin{frame}
{
Non-restrictive Rewriting
}
\begin{frame}
\frametitle
{
Non-restrictive Rewriting
}
\begin{itemize}
\itemsep
=6mm
\item
overlapping:
\hfill
$
x
+
0
\bto
x
$
,
$
0
+
x
\bto
x
$
...
...
@@ -196,13 +196,13 @@ def sum : (n: Nat) -> F n
\item
higher-order:
\hfill
$
lam
\,
(
\lambda
x.app
\,
F
\,
x
)
\bto
F
$
\item
matching modulo
$
\beta
$
:
\hfill
$
\partial\,
(
\lambda
x. ln
\,
(
F
\,
x
))
\bto\lambda
x.
(
\partial\,
F
\,
x
)
/
(
F
\,
x
)
$
\item
rules can be
both at the object and type levels
\item
there can be rules
both at the object and type levels
\end{itemize}
\end{frame}
\begin{frame}
\frametitle
{
Expected
properties of r
ewriting
}
\frametitle
{
Expected
Properties of R
ewriting
}
\begin{itemize}
\item
Termination: There is no infinite sequence of reduction starting from a well-typed term;
...
...
@@ -240,7 +240,7 @@ def sum : (n: Nat) -> F n
\end{itemize}
\end{frame}
\begin{frame}
{
Termination: d
ifficulties
}
\begin{frame}
\frametitle
{
Termination: D
ifficulties
}
\begin{itemize}
\itemsep
=5mm
\item
The set of terms
$
\lambda\Pi
/
\mathcal
{
R
}$
depends on rewriting rules
$
\mathcal
{
R
}$
;
...
...
@@ -248,8 +248,8 @@ def sum : (n: Nat) -> F n
independently of
$
\beta
$
-reduction;
\item
Type-level rewriting forbids the use of erasing tricks
reducing termination to simply-typed
$
\lambda
$
-calculus;
\item
Type-level rewriting allows to encode any functional
pure t
ype
system (e.g. system F or the calculus of c
onstructions).
\item
Type-level rewriting allows to encode any functional
Pure T
ype
System (e.g. System F or the Calculus of C
onstructions).
\end{itemize}
\end{frame}
...
...
@@ -265,7 +265,7 @@ def sum : (n: Nat) -> F n
\newcommand
{
\paren
}
[1]
{
\left
(#1
\right
)
}
\newcommand
{
\crochet
}
[1]
{
\left
[#1\right]
}
\begin{frame}
\frametitle
{
Typing
r
ules
}
\begin{frame}
\frametitle
{
Typing
R
ules
}
Abstraction:
\begin{prooftree}
\AxiomC
{$
\Gamma\vdash
\rA
:
\bType
$}
...
...
@@ -303,7 +303,7 @@ def sum : (n: Nat) -> F n
\subsection
{
Logical relation
}
\begin{frame}
\frametitle
{
Logical
relation
}
\begin{frame}
\frametitle
{
Logical
Relations
}
\begin{block}
{
Goal
}
Define
$
\interp
{
T
}$
such :
\begin{itemize}
...
...
@@ -312,7 +312,7 @@ def sum : (n: Nat) -> F n
\end{itemize}
\end{block}
\begin{block}
{
Reducibility
c
onditions
}
\begin{block}
{
Reducibility
C
onditions
}
\begin{itemize}
\item
$
\interp
{
T
}
\subseteq\mathrm
{
SN
}$
,
\item
If
$
t
\in\interp
{
T
}$
and
$
t
\to
_{
\beta\mathcal
{
R
}}
u
$
, then
$
u
\in\interp
{
T
}$
,
...
...
@@ -328,7 +328,7 @@ def sum : (n: Nat) -> F n
\end{block}
\end{frame}
\begin{frame}
\frametitle
{
Our
i
nterpretation
}
\begin{frame}
\frametitle
{
Our
I
nterpretation
}
We define
$
\interp
{
.
}$
as the fixpoint of a monotonic function.
...
...
@@ -358,7 +358,7 @@ A rule $f\,\bar l \to r$ gives rise to the \emph{dependency pairs} $f\,\bar l >
\end{itemize}
\end{definition}
\begin{theorem}
[Arts
et
Giesl]
\begin{theorem}
[Arts
and
Giesl]
First order:
$
\to
_{
\mathcal
{
R
}}$
terminates iff there is no
$
f
\,\bar
t>g
\,\bar
u
\to
_{
arg
}^
*
g
\,\bar
u'>
\dots
$
...
...
@@ -392,7 +392,7 @@ $\color{red}{(3)}$ append _ (cons x p l) q m $\color{red}{>}$ p + q
\end{frame}
\begin{frame}
[fragile]
\frametitle
{
Call-graph:
e
xample
}
\begin{frame}
[fragile]
\frametitle
{
Call-graph:
E
xample
}
\begin{lstlisting}
[mathescape=true]
def plus : Nat -> Nat -> Nat.
set infix "+" := plus.
...
...
@@ -436,20 +436,20 @@ def append: (p: Nat) -> List p ->
\end{definition}
\begin{definition}
[Plain Function Passing]
$
f
\,\bar
l
\to
r
$
is
\emph
{
PFP
}
if every functional type variable occurring in
$
r
$
are
equal to one of the
$
l
_
i
$
.
$
f
\,\bar
l
\to
r
$
is
\emph
{
PFP
}
if every functional type variable occurring in
$
r
$
is
equal to one of the
$
l
_
i
$
.
\end{definition}
\end{frame}
\subsection
{
Main
t
heorem
}
\subsection
{
Main
T
heorem
}
\begin{frame}
\frametitle
{
Main
r
esult
}
\begin{frame}
\frametitle
{
Main
R
esult
}
\begin{block}
{
Reminder
}
If for all
$
f
$
,
$
f
\in\interp
{
\Theta
_
f
}$
and
$
\Gamma\vdash
t:T
$
, then
$
t
\in\interp
{
T
}$
.
\end{block}
\begin{lemma}
Every
$
f
$
is in the interpretation of
$
\Theta
_
f
$
if:
Every
$
f
\in\interp
{
\Theta
_
f
}$
,
if:
\begin{itemize}
\item
$
\mathcal
{
R
}$
is
\emph
{
well-structured
}
,
\item
$
\mathcal
{
R
}$
is
\emph
{
PFP
}
,
...
...
@@ -458,7 +458,7 @@ def append: (p: Nat) -> List p ->
\end{lemma}
\end{frame}
\begin{frame}
\frametitle
{
Main
r
esult
}
\begin{frame}
\frametitle
{
Main
R
esult
}
\begin{theorem}
$
\to
_{
\beta\mathcal
{
R
}}$
terminates on every typable term in
$
\lambda\Pi
/
\mathcal
{
R
}$
if:
\begin{itemize}
...
...
@@ -473,7 +473,7 @@ def append: (p: Nat) -> List p ->
\subsection
{
Size-Change Termination
}
\begin{frame}
[fragile]
\frametitle
{
Call-graph:
e
xample
}
\begin{frame}
[fragile]
\frametitle
{
Call-graph:
E
xample
}
\begin{lstlisting}
[mathescape=true]
def plus : Nat -> Nat -> Nat.
set infix "+" := plus.
...
...
@@ -502,7 +502,7 @@ def append: (p: Nat) -> List p ->
\end{center}
\end{frame}
\begin{frame}
{
Size-Change Termination
}
\begin{frame}
\frametitle
{
Size-Change Termination
}
\begin{block}
{
Principle
}
Exclude cycles occurring in the call-graph.
...
...
@@ -525,7 +525,7 @@ def append: (p: Nat) -> List p ->
\definecolor
{
darkgreen
}{
RGB
}{
30,160,30
}
\begin{frame}
[fragile]
\frametitle
{
Size-Change Termination :
e
xample
}
\begin{frame}
[fragile]
\frametitle
{
Size-Change Termination :
E
xample
}
Evolution of the sizes of the arguments:
\vspace
{
1em
}
\begin{tabular}
{
|l|c|
}
...
...
@@ -630,7 +630,7 @@ $\color{red}{(3)}$ append _ (cons x p l) q m
\end{tikzpicture}
}
\end{frame}
\begin{frame}
\frametitle
{
Comparisons with
other t
ools
}
\begin{frame}
\frametitle
{
Comparisons with
Other T
ools
}
\begin{block}
{
Simply-typed
}
\begin{itemize}
\item
Annual competition, few participants (Wanda, SOL?),
...
...
@@ -647,7 +647,7 @@ $\color{red}{(3)}$ append _ (cons x p l) q m
\end{frame}
\begin{frame}
\frametitle
{
Future
w
ork
}
\begin{frame}
\frametitle
{
Future
W
ork
}
\begin{block}
{
Plain Function Passingness
}
Weaken this hypothesis to ``positivity'', requires to use structural ordering rather than subterm.
...
...
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