syntaxAlchemist/ladder-calculus
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

paper: rename inference rules to match coq definitions

Browse source
This commit is contained in:
Michael Sippel 2024-09-04 12:45:33 +02:00
parent fd8ca35a27
commit 1bd55cd8c3
Signed by: senvas
GPG key ID: F96CF119C34B64A6
1 changed files with 27 additions and 17 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

44
paper/main.tex
View file

@ -531,18 +531,18 @@ can be derived from the context \(\Gamma\) where \(\metavariable{e} \in \nonterm
\begin{definition}[Syntactic Well-Typedness] \begin{definition}[Representational Well-Typedness]
An expression \(\metavariable{e} \in \nonterm{E}\) is \textbf{syntactically well-typed} if there exists a type \(\metavariable{\tau} \in \nonterm{T}\), An expression \(\metavariable{e} \in \nonterm{E}\) is \textbf{representationally well-typed} if there exists a type \(\metavariable{\tau} \in \nonterm{T}\),
such that \( \emptyset \vdash \metavariable{e} : \metavariable{\tau} \) by \ref{def:typerules}. such that \( \emptyset \vdash \metavariable{e} : \metavariable{\tau} \) by \ref{def:typerules}.
\end{definition} \end{definition}
\begin{definition}[Semantic Well-Typedness] \begin{definition}[Compatible Well-Typedness]
An expression \(\metavariable{e} \in \nonterm{E}\) is \textbf{semantically well-typed} if there exists a type \(\metavariable{\tau} \in \nonterm{T}\), An expression \(\metavariable{e} \in \nonterm{E}\) is \textbf{compatibly well-typed} if there exists a type \(\metavariable{\tau} \in \nonterm{T}\),
such that \( \emptyset \vdash \metavariable{e} :\approx \metavariable{\tau} \) by \ref{def:typerules} and \ref{def:semtyperules}. such that \( \emptyset \vdash \metavariable{e} :\approx \metavariable{\tau} \) by \ref{def:typerules} and \ref{def:semtyperules}.
\end{definition} \end{definition}
\begin{definition}[Syntactic Typing Relation] \begin{definition}["is" Typing Relation]
\label{def:typerules} \label{def:typerules}
\begin{mathpar} \begin{mathpar}
@ -626,30 +626,37 @@ such that \( \emptyset \vdash \metavariable{e} :\approx \metavariable{\tau} \) b
\end{mathpar} \end{mathpar}
\end{definition} \end{definition}
\begin{definition}[Semantic Typing Relation] \begin{definition}["compatible" Typing Relation]
\label{def:semtyperules} \label{def:semtyperules}
\begin{mathpar} \begin{mathpar}
\inferrule[T-NativeRepr]{ \inferrule[TCompat-NativeRepr]{
\Gamma\vdash \metavariable{e} : \metavariable{\tau} \Gamma\vdash \metavariable{e} : \metavariable{\tau}
}{ }{
\Gamma\vdash \metavariable{e} :\approx \metavariable{\tau} \Gamma\vdash \metavariable{e} :\approx \metavariable{\tau}
} }
\inferrule[T-CoercedRepr]{ \inferrule[TCompat-Let]{
\Gamma \vdash \metavariable{e} : \metavariable{\sigma} \\
\Gamma , \metavariable{x}:\metavariable{\sigma} \vdash \metavariable{t} :\approx \metavariable{\tau}
}{
\Gamma \vdash (\exprterminal{\text{let }}\metavariable{x}\exprterminal{\text{ = }}\metavariable{e}\exprterminal{\text{ in }} \metavariable{t}) :\approx \metavariable{\tau}
}
\inferrule[TCompat-Morph]{
\Gamma \vdash \metavariable{e} :\approx \metavariable{\tau}\\ \Gamma \vdash \metavariable{e} :\approx \metavariable{\tau}\\
% \metavariable{\tau} \precsim \metavariable{\tau'}\\ % \metavariable{\tau} \precsim \metavariable{\tau'}\\
%\exists \metavariable{h} \text{ s.t. } %\exists \metavariable{h} \text{ s.t. }
\Gamma \vdash \metavariable{h}: \typeterminal{\metavariable{\tau}\rightarrow_\text{morph}\metavariable{\tau'}} \metavariable{h}:\typeterminal{\metavariable{\tau}\rightarrow_\text{morph}\metavariable{\tau'}} \in \Gamma
}{ }{
\Gamma \vdash \metavariable{e} :\approx \metavariable{\tau'} \Gamma \vdash \metavariable{e} :\approx \metavariable{\tau'}
} }
\inferrule[TCompat-App]{
\inferrule[T-CompatibleApp]{ \Gamma \vdash \metavariable{f} : \metavariable{\sigma} \typeterminal{\rightarrow} \metavariable{\tau}\\
\Gamma \vdash \metavariable{f} : \metavariable{\sigma} \rightarrow \metavariable{\tau}\\
\Gamma \vdash \metavariable{a} :\approx \metavariable{\sigma} \Gamma \vdash \metavariable{a} :\approx \metavariable{\sigma}
}{ }{
\Gamma \vdash \exprterminal{(\metavariable{f} \text{ } \metavariable{a})} : \metavariable{\tau} \Gamma \vdash \exprterminal{(\metavariable{f} \text{ } \metavariable{a})} :\approx \metavariable{\tau}
} }
\end{mathpar} \end{mathpar}
\end{definition} \end{definition}
@ -775,13 +782,16 @@ Evaluation of an expression \(\metavariable{e} \in \nonterm{E}\) is defined by e
\exprterminal{\text{ in }}\metavariable{e} \exprterminal{\text{ in }}\metavariable{e}
\rightarrow_\beta \rightarrow_\beta
\{ \metavariable{x} \mapsto \metavariable{a} \} \metavariable{e} \{ \metavariable{x} \mapsto \metavariable{a} \} \metavariable{e}
}\and }
\inferrule[E-Ascribe]{
\inferrule[E-AppLamAscribe]{
}{ }{
\metavariable{e} \exprterminal{( \lambda \metavariable{x}:\metavariable{\sigma} \mapsto \metavariable{e} )}
\exprterminal{\text{ as }} \exprterminal{\text{ as }}
\metavariable{\tau} \typeterminal{\metavariable{\tau}}
\metavariable{e}
\rightarrow_\beta \rightarrow_\beta
\metavariable{v}
\metavariable{e} \metavariable{e}
} }
\end{mathpar} \end{mathpar}