Commit c766a3f4 authored by Gaspard Ferey's avatar Gaspard Ferey

Proposition de condition de wellformedness.

parent 6ebc8b45
...@@ -35,6 +35,8 @@ ...@@ -35,6 +35,8 @@
We denote \(\mathcal{T}_{\mathcal{X}}\) the free algebra over the terms with variables in \(\mathcal{X}\). We denote \(\mathcal{T}_{\mathcal{X}}\) the free algebra over the terms with variables in \(\mathcal{X}\).
\end{definition} \end{definition}
Note: \(\mathcal{T}_{\mathcal{\emptyset}}\) is the set of closed terms.
\begin{definition} \begin{definition}
We define \(\mathfrak{R}_{\mathcal{X}}\) the set of pairs of terms: We define \(\mathfrak{R}_{\mathcal{X}}\) the set of pairs of terms:
\[\mathfrak{R}_{\mathcal{X}} \defn \{(t,u) \mid t,u \in \mathcal{T}_{\mathcal{X}}\} \] \[\mathfrak{R}_{\mathcal{X}} \defn \{(t,u) \mid t,u \in \mathcal{T}_{\mathcal{X}}\} \]
...@@ -44,6 +46,7 @@ ...@@ -44,6 +46,7 @@
We denote \(Dom(\Gamma)\) the domain of \(\Gamma\) defines as: We denote \(Dom(\Gamma)\) the domain of \(\Gamma\) defines as:
\begin{align*} \begin{align*}
Dom(\emptyset) &\defn \emptyset \\ Dom(\emptyset) &\defn \emptyset \\
Dom(\Gamma , \mathcal{R}) &\defn Dom(\Gamma) \\
Dom(\Gamma , x : A) &\defn Dom(\Gamma) \cup \{x\} Dom(\Gamma , x : A) &\defn Dom(\Gamma) \cup \{x\}
\end{align*} \end{align*}
\end{definition} \end{definition}
...@@ -121,4 +124,23 @@ ...@@ -121,4 +124,23 @@
{\Gamma \vdash t: B} {\Gamma \vdash t: B}
\end{rules} \end{rules}
\newpage
\section{A simple wellformedness condition}
On could start studying a very simple wellformedness condition.
\begin{rules}{A (perhaps too) simple rule for relation wellformedness}{Relation WF}
\inferrule{
\Gamma \vdash A : \ttype
\\
\Gamma \vdash t : A
\\
\Gamma \vdash u : A
}
{\Gamma \vdash \wf{\{(t,u)\}}}
\end{rules}
\end{document} \end{document}
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