From c766a3f42a61cb27c55ded2bccf0742a5a298831 Mon Sep 17 00:00:00 2001 From: Gaspard Ferey Date: Fri, 20 Apr 2018 14:26:22 +0200 Subject: [PATCH] Proposition de condition de wellformedness. --- LaTeX/lfmt.tex | 22 ++++++++++++++++++++++ 1 file changed, 22 insertions(+) diff --git a/LaTeX/lfmt.tex b/LaTeX/lfmt.tex index 0172f2d..a7ad5c7 100644 --- a/LaTeX/lfmt.tex +++ b/LaTeX/lfmt.tex @@ -35,6 +35,8 @@ We denote $$\mathcal{T}_{\mathcal{X}}$$ the free algebra over the terms with variables in $$\mathcal{X}$$. \end{definition} +Note: $$\mathcal{T}_{\mathcal{\emptyset}}$$ is the set of closed terms. + \begin{definition} 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}}\}$ @@ -44,6 +46,7 @@ We denote $$Dom(\Gamma)$$ the domain of $$\Gamma$$ defines as: \begin{align*} Dom(\emptyset) &\defn \emptyset \\ + Dom(\Gamma , \mathcal{R}) &\defn Dom(\Gamma) \\ Dom(\Gamma , x : A) &\defn Dom(\Gamma) \cup \{x\} \end{align*} \end{definition} @@ -121,4 +124,23 @@ {\Gamma \vdash t: B} \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} -- 2.24.1