Commit ec4d67e4 authored by Guillaume GENESTIER's avatar Guillaume GENESTIER

To \mbb{U}

parent 57a438e4
......@@ -2,7 +2,7 @@
\section{Dependency pairs}
\begin{defi}[Dependency pairs]
Let $f\bar l>g\bar m$ if there are a rule $f\bar l\rul r\in\mcal{R}$,
Let $f\bar l>g\bar m$ if there is a rule $f\bar l\rul r\in\mcal{R}$,
such that $g\,\bar m$ occurs in $r$, $\valabs{\bar m}\<\arity(g)$
and if $\valabs{\bar m}<\arity(g)$ then $\bar m$ are all the arguments to which $g$ is applied (ie. $\bar m$ are the arguments to which $g$ is applied truncated to the arity of $g$).
\end{defi}
......@@ -13,23 +13,95 @@
and for all $k\<j$, $m_k\sg=u_k$.
\end{defi}
\begin{defi}[Symbol order]
Let $\sqsupseteq$ be the smallest pre-order on $\Func$ such that
\begin{itemize}
\item if $g$ occurs in $\tau(f)$, then $f\sqsupseteq g$,
\item if there are $\bar l$ and $\bar u$ such that $f\,\bar l>g\,\bar u$, then $f\sqsupseteq g$.
\end{itemize}
\end{defi}
\begin{defi}[Computability closure]
Given $f\bar l$, let $\vdash_{f\bar l}$ be the relation defined as $\vdash$,
except the rules (app) and (fun) replaced by
\begin{cond}{cond-symb-order-wf}
$\sqsubset$ is well-founded.
\todo{Note that it is free if $\Func$ is finite.}
\end{cond}
\todo{
Should we add function symbol occuring at accessible position in the lhs?
}
\begin{defi}[Ordered typing]
Let $f\in\Func$.
Let $\vdash_{\sqsubset f}$ be the relation defined as $\vdash$,
but where the rule (fun) is replaced by:
\begin{prooftree}
\AxiomC{$\Gamma\vdash_{f\bar l} t: \Pi(x:A). B$}
\AxiomC{$\Gamma\vdash_{f\bar l} u:A$}
\RightLabel{
\begin{tabular}{l}
$t$ not of the form $g\,\bar l$\\
with $g$ a symbol of the signature
\end{tabular}}
\BinaryInfC{$\Gamma\vdash_{f\bar l} t\,u:\subst{B}{x}{u}$}
\AxiomC{$\G\vdash_{\sqsubset f}\tau(g):s(g)$}
\AxiomC{$g\sqsubset f$}
\BinaryInfC{$\G\vdash_{\sqsubset f}g:\tau(g)$}
\end{prooftree}
Note that it introduces predicates well-formed${}_{\sqsubset f}$.
\begin{center}
\begin{tabular}{rcl}
\AxiomC{$\phantom{\Gamma\vdash A}$}
\UnaryInfC{$[]$ well-formed${}_{\sqsubset f}$}
\DisplayProof&&
\AxiomC{$\Gamma\vdash_{\sqsubset f} A:s$}
\RightLabel{$\sys{x\notin\support(\Gamma)}{s\in\Sort}$}
\UnaryInfC{$\Gamma,x:A$ well-formed${}_{\sqsubset f}$}
\DisplayProof
\end{tabular}
\end{center}
\end{defi}
\begin{defi}[Computability closure]
Let $f\,\bar l$ be the left-hand side of a rewrite rule.
Let $\vdash_{f\bar l}$ be the relation defined by:
\begin{center}
\begin{tabular}{rcl}
\AxiomC{$\Gamma$ well-formed${}_{\sqsubset f}$}
\UnaryInfC{$\Gamma\vdash_{f\bar l} \Type:\Kind$}
\DisplayProof&&
\AxiomC{$\Gamma$ well-formed${}_{\sqsubset f}$}
\RightLabel{$x:A\in\Gamma$}
\UnaryInfC{$\Gamma\vdash_{f\bar l} x:A$}
\DisplayProof
\end{tabular}
\end{center}
\begin{prooftree}
\AxiomC{$\Gamma\vdash_{f\bar l} A:\Type$}
\AxiomC{$\Gamma,x:A\vdash_{f\bar l} B:s$}
\RightLabel{$s\in\Sort$}
\BinaryInfC{$\Gamma\vdash_{f\bar l} \Pi(x:A).B:s$}
\end{prooftree}
\begin{prooftree}
\AxiomC{$\Gamma\vdash_{\sqsubset f}\Pi(x:A).B:s$}
\AxiomC{$\Gamma,x:A\vdash_{f\bar l} t:B$}
\RightLabel{$s\in\Sort$}
\BinaryInfC{$\Gamma\vdash_{f\bar l}\lambda(x:A).t: \Pi(x:A).B$}
\end{prooftree}
\begin{prooftree}
\AxiomC{$\Gamma\vdash_{f\bar l} t: \Pi(x:A).B$}
\AxiomC{$\Gamma\vdash_{f\bar l} u:A$}
\AxiomC{$\Gamma\vdash_{\sqsubset f}\Pi(x:A).B:s$}
\TrinaryInfC{$\Gamma\vdash_{f\bar l} t\,u:\subst{B}{x}{u}$}
\end{prooftree}
\begin{prooftree}
\AxiomC{$\Gamma\vdash_{f\bar l} t:A$}
\AxiomC{$\Gamma\vdash_{\sqsubset f} A:s$}
\AxiomC{$\Gamma\vdash_{\sqsubset f} B:s$}
\RightLabel{$\sys{A\downarrow B}{s\in\Sort}$}
\TrinaryInfC{$\Gamma\vdash_{f\bar l} t:B$}
\end{prooftree}
\begin{prooftree}
\def\defaultHypSeparation{\hskip 0em}
\AxiomC{$\vdash_{f\bar l} \tau(g):s(g)$}
\AxiomC{$\vdash_{\sqsubset f} \tau(g):s(g)$}
\AxiomC{$\overline{\G\vdash_{f\bar l} u:U\g}$}
\RightLabel{
$\left\{\begin{matrix}
......@@ -41,6 +113,13 @@
\end{prooftree}
\end{defi}
\begin{prooftree}
\AxiomC{$\G\vdash_{\sqsubset f}\tau(g):s(g)$}
\RightLabel{$g$ undefined}
\UnaryInfC{$\G\vdash_{f\bar l}g:\tau(g)$}
\end{prooftree}
\begin{defi}[Valid rule]
A rule $f\,\bar l\rul r$ with $\tau(f)=\Pi\overline{(x:T)}. U$, $\G=\overline{(x:T)}$ and $\pi=\crochet{\overline{\sur{l}{x}}}$ is \emph{valid} if
......@@ -60,12 +139,19 @@
\tau(f)\in\interp{s(f)},\\
\tau(f)=\Pi\overline{(x:T)}. T',\\
T'\text{ is not an arrow}\\
\valabs{\bar t}=\arity(f)\\
\crochet{\overline{\sur{t}{x}}}\vDash\overline{(x:T)}
\end{matrix}
}
\]
\end{defi}
\begin{defi}[$\rew_{arg}$]
Let $f\,\bar t\in\mbb{U}$.
$f\,\bar t\rew_{arg}u$ if $u=f\,\bar t'$, there is a $i$ such that $t_i\rew t'_i$
and for all $j\neq i$, $t_j=t'_j$.
\end{defi}
\begin{thm}
$\tau$ is valid if $\call$ terminates on $\mbb{U}$ and all rules in $\mcal{R}$ are valid.
......@@ -78,7 +164,7 @@
Let $\pi=\crochet{\overline{\sur{t}{x}}}$.
We want to prove that $f\in\interp{\Pi\overline{(x:T)}. T'}$ which by definition of the interpretation of a product is equivalent to show that $f\,\bar t\in\interp{T'\pi}$.
Since $\rew_{arg}$ and $\call$ terminate on $\mbb{U}$ and $\rew_{arg}\call \subseteq{\call}$,
Since $\rew_{arg}$ and $\call$ terminate on $\mbb{U}$ and $(\rew_{arg}\call) \subseteq{\call}$,
we have that $\rew_{arg}\cup{\call}$ terminates on $\mbb{U}$.
We now prove that, $f\,\bar t\in\interp{T'\pi}$ by induction on ${\rew_{arg}}\cup{\call}$.
......
......@@ -20,7 +20,7 @@
\begin{proof}
Let $\sg$ be such that $\sg\vDash\G$.
We prove this lemma by induction on $\G\vdash t:T$:
\begin{itemize}
\begin{description}
\item[(axSort)]
$\Type\in\interp{\Kind\sg}=\interp{\Kind}$ by definition,
\item[(axVar)]
......@@ -64,5 +64,5 @@
so $\interp{A\sg}=\interp{B\sg}$ and
since by induction hypothesis $t\sg\in\interp{A\sg}$, we have $t\sg\in\interp{B\sg}$.
\qedhere
\end{itemize}
\end{description}
\end{proof}
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