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

paper: simplify pseudo grammar

Browse source
This commit is contained in:
Michael Sippel 2024-08-07 16:00:01 +02:00
parent f135a5ed43
commit 3f27afa253
Signed by: senvas
GPG key ID: F96CF119C34B64A6
1 changed files with 77 additions and 87 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

164
paper/main.tex
View file

@ -1,4 +1,4 @@
\documentclass[10pt, nonacm]{acmart} \documentclass[10pt, sigplan, nonacm]{acmart}
\usepackage[utf8]{inputenc} \usepackage[utf8]{inputenc}
\usepackage{formal-grammar} \usepackage{formal-grammar}
@ -73,151 +73,139 @@ which are already known from SystemF,
types can be of the form \(\tau_1 \sim \tau_2\) to denote a \emph{ladder type} to formalizes the notion of a type \(\tau_1\) being represented in terms of type \(\tau_2\). types can be of the form \(\tau_1 \sim \tau_2\) to denote a \emph{ladder type} to formalizes the notion of a type \(\tau_1\) being represented in terms of type \(\tau_2\).
Similar to SystemF, expressions can be \emph{variables}, \emph{type-abstractions}, \emph{} Similar to SystemF, expressions can be \emph{variables}, \emph{type-abstractions}, \emph{}
Coq definitions of the abstract syntax can be found in \hyperref[coq:terms]{\texttt{terms.v}}.
\begin{figure}[h] \begin{figure}[h]
\label{gr:core} \label{gr:core}
\begin{grammar} \begin{grammar}
\firstcase{ T_\seltype \textsf{$(\typenames, \typevars)$} }{
\firstcase{ T }{
\metavariable{\sigma} \metavariable{\sigma}
}{Type Literal \quad \textsf{where $ \metavariable{\sigma} \in \typenames $}} }{Base Type}
\otherform{ \otherform{
\metavariable{\alpha} \metavariable{\alpha}
}{Type Variable \quad \textsf{where $ \metavariable{\alpha} \in \typevars $}} }{Type Variable}
\otherform{ \otherform{
$$\typeterminal{\forall}$$ \metavariable{\alpha} \typeterminal{.} \quad \typenonterm{\typevars \cup \{\metavariable{\alpha}\}} \typeterminal{\forall} \metavariable{\alpha} \typeterminal{.} \nonterm{T}
}{Universal Type} }{Universal Type}
\otherform{ \otherform{
\typeterminal{<} \typenonterm{\typevars} \quad \typenonterm{\typevars} \typeterminal{>} \typeterminal{<} \nonterm{T} \quad \nonterm{T} \typeterminal{>}
}{Specialization} }{Specialized Type}
\otherform{ \otherform{
\typenonterm{\typevars} \nonterm{T} \quad \typeterminal{\rightarrow} \quad \nonterm{T}
\quad $$\typeterminal{\rightarrow}$$ \quad
\typenonterm{\typevars}
}{Function Type} }{Function Type}
\otherform{ \otherform{
\typenonterm{\typevars} \nonterm{T} \quad \typeterminal{\rightarrow_\text{morph}} \quad \nonterm{T}
\quad $$\typeterminal{\rightarrow_{morph}}$$ \quad
\typenonterm{\typevars}
}{Morphism Type} }{Morphism Type}
\otherform{ \otherform{
\typenonterm{\typevars} \nonterm{T} \quad \typeterminal{\sim} \quad \nonterm{T}
\quad $$\typeterminal{\sim}$$ \quad
\typenonterm{\typevars}
}{Ladder Type} }{Ladder Type}
\otherform{
$$\typeterminal{(}$$ \quad
\typenonterm{\typevars}
\quad $$\typeterminal{)}$$
}{Parenthesis}
$$\\$$ $$\\$$
\firstcase{ E
% T_\selexpr
\firstcase{ T_\selexpr \textsc{$(\typenames, \typevars, \exprvars)$} } }
{ \metavariable{x} { \metavariable{x}
} {Variable \quad \textsf{where $\metavariable{x} \in \exprvars$} } } {Variable}
\otherform{ \otherform{
$$ \exprterminal{\Lambda} \metavariable{\alpha} $$ \exprterminal{\Lambda} \metavariable{\alpha}
\quad \exprterminal{\mapsto} \quad $$ \quad \exprterminal{\mapsto} \quad $$
\exprnonterm{\typevars \cup \{\metavariable{\alpha}\}}{\exprvars} \nonterm{ E }
}{Type Abstraction} }{Type Abstraction}
\otherform{ \otherform{
$$ \exprterminal{\lambda} \metavariable{x} $$ $$ \exprterminal{\lambda} \metavariable{x} $$
\exprterminal{:} \typenonterm{\typevars} \exprterminal{:} \nonterm{ T }
\quad $$\exprterminal{\mapsto}$$ \quad \quad $$\exprterminal{\mapsto}$$ \quad
\exprnonterm{\typevars}{\exprvars \cup \{\metavariable{x}\}} \nonterm{ E }
}{Value Abstraction} }{Value Abstraction}
\otherform{ \otherform{
$$ \exprterminal{\lambda} \metavariable{x} $$ $$ \exprterminal{\lambda} \metavariable{x} $$
\exprterminal{:} \typenonterm{\typevars} \exprterminal{:} \nonterm{ T }
\quad $$\exprterminal{\mapsto_{morph}}$$ \quad \quad $$\exprterminal{\mapsto_\text{morph}}$$ \quad
\exprnonterm{\typevars}{\exprvars \cup \{\metavariable{x}\}} \nonterm{ E }
}{Value Morphism} }{Value Morphism}
\otherform{ \otherform{
\exprterminal{let} \quad \metavariable{x} \quad \exprterminal{=} \quad \exprterminal{let} \quad \metavariable{x} \quad \exprterminal{=} \quad
\exprnonterm{\typevars}{\exprvars} \nonterm{ E }
\quad \exprterminal{in} \quad \quad \exprterminal{in} \quad
\exprnonterm{\typevars}{\exprvars \cup \{\metavariable{x}\}} \nonterm{ E }
}{Variable Binding} }{Variable Binding}
\otherform{ \otherform{
\exprnonterm{\typevars}{\exprvars} \nonterm{ E }
\quad \quad
\typenonterm{\typevars} \nonterm{ T }
}{Type Application} }{Type Application}
\otherform{ \otherform{
\exprnonterm{\typevars}{\exprvars} \nonterm{ E }
\quad \quad
\exprnonterm{\typevars}{\exprvars} \nonterm{ E }
}{Value Application} }{Value Application}
\otherform{ \otherform{
\exprnonterm{\typevars}{\exprvars} \nonterm{ E }
\quad \quad
\exprterminal{as} \exprterminal{as}
\quad \quad
\typenonterm{\typevars} \nonterm{ T }
}{Type Cast} }{Up-Cast}
\otherform{ \otherform{
\exprterminal{(} \quad \nonterm{ E }
\exprnonterm{\typevars}{\exprvars} \quad
\quad \exprterminal{)} \exprterminal{to}
}{Parenthesis} \quad
\nonterm{ T }
}{Transformation}
\otherform{\exprterminal{(} \quad \nonterm{E} \quad \exprterminal{)}}{Parenthesis}
$$\\$$ $$\\$$
\firstcase{ T_\textsc{Val} \textsc{$(\typenames, \typevars, \exprvars)$} }{ \firstcase{V}{
\exprterminal{\epsilon} \exprterminal{\epsilon}
}{Empty Value} }{Empty Value}
\otherform{
\metavariable{x} \quad \valnonterm{\typevars}{\exprvars}
}{Value Conactenation}
\otherform{ \otherform{
\exprterminal{\Lambda} \metavariable{\alpha} \quad \exprterminal{\Lambda} \metavariable{\alpha} \quad
\exprterminal{\mapsto} \quad \exprterminal{\mapsto} \quad
\valnonterm{ \typevars \cup \{ \metavariable{\alpha} \} } \nonterm{ V }
\{Type-Function Value} }{Type-Abstraction Value}
\otherform{ \otherform{
\exprterminal{\lambda} \metavariable{x} \quad \exprterminal{\lambda} \metavariable{x}
\exprterminal{:} \quad \exprterminal{:}
\typenonterm{\emptyset} \quad \nonterm{ T } \quad
\exprterminal{\mapsto} \quad \exprterminal{\mapsto} \quad
\exprnonterm{\typevars}{\{\metavariable{x}\}} \nonterm{ E }
}{Function Value} }{Abstraction Value}
\otherform{ \otherform{
\valnonterm{ \typevars } \quad \nonterm{ V } \quad
\exprterminal{as} \quad \exprterminal{as} \quad
\typenonterm{ \typevars } \nonterm{ T }
}{Value} }{Cast Value}
\end{grammar} \end{grammar}
\caption{Syntax of the core calculus with colors for \metavariable{metavariables}, \typeterminal{type-level terminal symbols}, \exprterminal{expression-level terminal symbols} \caption{Syntax of the core calculus with colors for \metavariable{metavariables}, \typeterminal{type-level terminal symbols}, \exprterminal{expression-level terminal symbols}
where $\typenames, \typevars, \exprvars$ are mutually disjoint, countable sets of symbols to denote atomic type identifiers (\(\typenames\)), free typevariables (\(\typevars\)), and free expression variables (\(\exprvars\)). where $\typenames, \typevars, \exprvars$ are mutually disjoint, countable sets of symbols to denote atomic type identifiers (\(\typenames\)), typevariables (\(\typevars\)), and expression variables (\(\exprvars\)).
By default, assume \(\metavariable{\sigma} \in \typenames\), \(\metavariable{\alpha} \in \typevars\) and \(\metavariable{x} \in \exprvars\)
$$\\$$} $$\\$$}
\end{figure} \end{figure}
@ -228,25 +216,25 @@ Let \(\Sigma = \{ \text{Digit}, \text{Char}, \text{Seq}, \text{UTF-8}, \mathbb{N
The following terms are valid types over \(\Sigma\): The following terms are valid types over \(\Sigma\):
\begin{enumerate} \begin{enumerate}
\item \typeterminal{<Seq Char>} \( \in \typenonterm{\emptyset}\)\\ \item \typeterminal{<Seq Char>}\\ %\( \in \typenonterm{\emptyset}\)\\
"sequence of characters" "sequence of characters"
\item \typeterminal{<Seq <Digit 10> \(\sim\) Char>} \( \in \typenonterm{\emptyset}\)\\ \item \typeterminal{<Seq <Digit 10> \(\sim\) Char>}\\ %\( \in \typenonterm{\emptyset}\)\\
"sequence of decimal digits, where each digit is represented as character" "sequence of decimal digits, where each digit is represented as character"
\item \typeterminal{<Seq Item> \(\rightarrow \mathbb{N} \rightarrow\) Item} \( \in \typenonterm{\{Item\}}\)\\ \item \typeterminal{<Seq Item> \(\rightarrow \mathbb{N} \rightarrow\) Item}\\ %\( \in \typenonterm{\{Item\}}\)\\
"function that maps a sequence of items and a natural number to an item"\\ "function that maps a sequence of items and a natural number to an item"\\
Note: this type contains the free variable \typeterminal{Item} %Note: this type contains the free variable \typeterminal{Item}
\item \typeterminal{<Seq Char> \(\sim\) UTF-8 \(\rightarrow \mathbb{N} \rightarrow\) Char } \( \in \typenonterm{\emptyset}\)\\ \item \typeterminal{<Seq Char> \(\sim\) UTF-8 \(\rightarrow \mathbb{N} \rightarrow\) Char }\\ %\( \in \typenonterm{\emptyset}\)\\
"function that takes a sequence of chars, represented as UTF-8 string, and a natural number to return a character" "function that takes a sequence of chars, represented as UTF-8 string, and a natural number to return a character"
\item \typeterminal{\(\forall\) Radix . <Seq <Digit Radix> \(\sim\) Char>} \(\in \typenonterm{\emptyset} \)\\ \item \typeterminal{\(\forall\) Radix . <Seq <Digit Radix> \(\sim\) Char>}\\ %\(\in \typenonterm{\emptyset} \)\\
"given the parameter \typeterminal{Radix}, a sequence of digits where each digit is represented as character"\\ "given the parameter \typeterminal{Radix}, a sequence of digits where each digit is represented as character"
Note: this type-term is \emph{ground} (i.e. \(\typevars = \emptyset\)), since \typeterminal{Radix} is bound by \(\typeterminal{\forall}\) %Note: this type-term is \emph{ground} (i.e. \(\typevars = \emptyset\)), since \typeterminal{Radix} is bound by \(\typeterminal{\forall}\)
\item \typeterminal{ \item \typeterminal{
\(\forall\) SrcRadix.\\ \(\forall\) SrcRadix.\\
\(\forall\) DstRadix.\\ \(\forall\) DstRadix.\\
\(\mathbb{N} \sim\) <PosInt SrcRadix> \(\sim\) <Seq <Digit SrcRadix> \(\sim\) Char>\\ \(\mathbb{N} \sim\) <PosInt SrcRadix> \(\sim\) <Seq <Digit SrcRadix> \(\sim\) Char>\\
\(\rightarrow_{morph}\)\\ \(\rightarrow_{morph}\)\\
\(\mathbb{N} \sim\) <PosInt DstRadix> \(\sim\) <Seq <Digit DstRadix> \(\sim\) Char>\\ \(\mathbb{N} \sim\) <PosInt DstRadix> \(\sim\) <Seq <Digit DstRadix> \(\sim\) Char>\\
} \(\in \typenonterm{\emptyset} \)\\ }\\ %\(\in \typenonterm{\emptyset} \)\\
"morphism function that maps the \typeterminal{PosInt} representation of \(\typeterminal{\mathbb{N}}\) with radix \typeterminal{SrcRadix} to the \typeterminal{PosInt} representation of radix \typeterminal{DstRadix}" "morphism function that maps the \typeterminal{PosInt} representation of \(\typeterminal{\mathbb{N}}\) with radix \typeterminal{SrcRadix} to the \typeterminal{PosInt} representation of radix \typeterminal{DstRadix}"
\end{enumerate} \end{enumerate}
\end{example} \end{example}
@ -254,8 +242,10 @@ Note: this type-term is \emph{ground} (i.e. \(\typevars = \emptyset\)), since \t
\begin{definition}[Substitution in Types] \begin{definition}[Substitution in Types]
Given a type-variable assignment \(\psi_t = \{ \metavariable{\alpha_1} \mapsto \metavariable{\tau_1}, \quad \metavariable{\alpha_2} \mapsto \metavariable{\tau_2}, \quad \dots \}\), Given a type-variable assignment \(\psi_t = \{ \metavariable{\alpha_1} \mapsto \metavariable{\tau_1}, \quad \metavariable{\alpha_2} \mapsto \metavariable{\tau_2}, \quad \dots \}\),
the thereby induced, lexically scoped substitution \(\overline{\psi_t}\) replaces all \emph{free} occurences of the variables \(\metavariable{\alpha_i}\) in a type-term \(\metavariable{\xi} \in \typenonterm{\{\metavariable{\alpha_1}, \quad \metavariable{\alpha_2}, \quad \dots\}}\) recursively with the type-term given by \(\psi_t(\metavariable{\alpha_i})\). the thereby induced, substitution \(\overline{\psi_t}\) replaces all \emph{free} occurences of the variables \(\metavariable{\alpha_i}\) in a type-term \(\metavariable{\xi} \in \typenonterm{\{\metavariable{\alpha_1}, \quad \metavariable{\alpha_2}, \quad \dots\}}\) recursively with the type-term given by \(\psi_t(\metavariable{\alpha_i})\).
Lexical scoping is implemented by simply not substituting any bound occourences of variables \(\metavariable{\alpha_i}\). This allows to skip \(\alpha\)-conversion as done in classical \(\lambda\)-calculus. Occourences of bound variables \(\metavariable{\alpha_i}\) are
Coq definition is at \hyperref[coq:subst-type]{subst.v:\ref{coq:subst-type}}.
\[\overline{\psi_t} \metavariable{\xi} = \begin{cases} \[\overline{\psi_t} \metavariable{\xi} = \begin{cases}
\metavariable{\xi} \quad \text{if } \metavariable{\xi} \in \typenames\\ \metavariable{\xi} \quad \text{if } \metavariable{\xi} \in \typenames\\
@ -369,7 +359,7 @@ As usual, each rule is composed of premises (above the horizontal line) and a co
\inferrule[T-Variable]{ \inferrule[T-Variable]{
\metavariable{x} \in \exprvars\\ \metavariable{x} \in \exprvars\\
\metavariable{\tau} \in \typenonterm{\emptyset}\\ \metavariable{\tau} \in \nonterm{T}\\
\metavariable{x}:\metavariable{\tau} \in \Gamma\\ \metavariable{x}:\metavariable{\tau} \in \Gamma\\
}{ }{
\Gamma \vdash \metavariable{x}:\metavariable{\tau} \Gamma \vdash \metavariable{x}:\metavariable{\tau}
@ -385,25 +375,25 @@ As usual, each rule is composed of premises (above the horizontal line) and a co
\inferrule[T-TypeAbs]{ \inferrule[T-TypeAbs]{
\metavariable{\tau} \in \typenonterm{\typevars \cup \{\metavariable{\alpha}\}} \\ \metavariable{\tau} \in \nonterm{T} \\
\metavariable{e} \in \exprnonterm{\typevars \cup \{ \metavariable{\alpha} \}}{\exprvars} \\ \metavariable{e} \in \nonterm{E} \\
\Gamma \vdash \metavariable{e} : \metavariable{\tau} \\ \Gamma \vdash \metavariable{e} : \metavariable{\tau} \\
}{ }{
\Gamma \vdash (\exprterminal{\Lambda} \metavariable{\alpha} \exprterminal{\mapsto} \metavariable{e}) : \typeterminal{\forall}\metavariable{\alpha}\typeterminal{.}\metavariable{\tau} \Gamma \vdash (\exprterminal{\Lambda} \metavariable{\alpha} \exprterminal{\mapsto} \metavariable{e}) : \typeterminal{\forall}\metavariable{\alpha}\typeterminal{.}\metavariable{\tau}
} }
\inferrule[T-TypeApp]{ \inferrule[T-TypeApp]{
\metavariable{\tau} \in \typenonterm{\typevars \cup \{\metavariable{\alpha}\}} \\ \metavariable{\tau} \in \nonterm{T} \\
\Gamma \vdash \metavariable{e} : \typeterminal{\forall} \metavariable{\alpha} \typeterminal{.} \metavariable{\tau} \\ \Gamma \vdash \metavariable{e} : \typeterminal{\forall} \metavariable{\alpha} \typeterminal{.} \metavariable{\tau} \\
\metavariable{\sigma} \in \typenonterm{\typevars} \metavariable{\sigma} \in \nonterm{T}
}{ }{
\Gamma \vdash ( \metavariable{e} \quad \metavariable{\sigma} ) : \{\metavariable{\alpha} \mapsto \metavariable{\sigma}\} \metavariable{\tau} \Gamma \vdash ( \metavariable{e} \quad \metavariable{\sigma} ) : \{\metavariable{\alpha} \mapsto \metavariable{\sigma}\} \metavariable{\tau}
} }
\inferrule[T-ValueAbs]{ \inferrule[T-ValueAbs]{
\metavariable{\sigma}, \metavariable{\tau} \in \typenonterm{\typevars} \\ \metavariable{\sigma}, \metavariable{\tau} \in \nonterm{T} \\
\metavariable{e} \in \exprnonterm{\typevars}{\exprvars \cup \{ \metavariable{x} \} } \\ \metavariable{e} \in \nonterm{E} \\
\Gamma \vdash \metavariable{e} : \metavariable{\tau} \\ \Gamma \vdash \metavariable{e} : \metavariable{\tau} \\
}{ }{
\Gamma \vdash (\exprterminal{\lambda} \metavariable{x} \exprterminal{:} \metavariable{\sigma} \exprterminal{\mapsto} \metavariable{e}) : \metavariable{\sigma}\typeterminal{\rightarrow}\metavariable{\tau} \Gamma \vdash (\exprterminal{\lambda} \metavariable{x} \exprterminal{:} \metavariable{\sigma} \exprterminal{\mapsto} \metavariable{e}) : \metavariable{\sigma}\typeterminal{\rightarrow}\metavariable{\tau}
@ -424,8 +414,8 @@ As usual, each rule is composed of premises (above the horizontal line) and a co
}\and }\and
\inferrule[T-MorphAbs]{ \inferrule[T-MorphAbs]{
\metavariable{\sigma}, \metavariable{\tau} \in \typenonterm{\typevars} \\ \metavariable{\sigma}, \metavariable{\tau} \in \nonterm{T} \\
\metavariable{e} \in \exprnonterm{\typevars}{\exprvars \cup \{ \metavariable{x} \} } \\ \metavariable{e} \in \nonterm{E} \\
\Gamma \vdash \metavariable{e} : \metavariable{\tau} \\ \Gamma \vdash \metavariable{e} : \metavariable{\tau} \\
}{ }{
\Gamma \vdash (\exprterminal{\lambda} \metavariable{x} \exprterminal{:} \metavariable{\tau} \exprterminal{\mapsto_{morph}} \metavariable{e}) : \metavariable{\sigma}\typeterminal{\rightarrow_{morph}}\metavariable{\tau} \Gamma \vdash (\exprterminal{\lambda} \metavariable{x} \exprterminal{:} \metavariable{\tau} \exprterminal{\mapsto_{morph}} \metavariable{e}) : \metavariable{\sigma}\typeterminal{\rightarrow_{morph}}\metavariable{\tau}
@ -457,7 +447,7 @@ As usual, each rule is composed of premises (above the horizontal line) and a co
\end{definition} \end{definition}
\subsection{Evaluation Semantics} \subsection{Evaluation}
Evaluation of an expression \(\metavariable{e} \in \exprnonterm{\emptyset}{\emptyset}\) is defined by exhaustive application of the rewrite rules \(\rightarrow_\beta\) and \(\rightarrow_\delta\), Evaluation of an expression \(\metavariable{e} \in \exprnonterm{\emptyset}{\emptyset}\) is defined by exhaustive application of the rewrite rules \(\rightarrow_\beta\) and \(\rightarrow_\delta\),
which are given in \ref{def:evalrules}. which are given in \ref{def:evalrules}.
@ -559,7 +549,7 @@ Then \(\emptyset \vdash \metavariable{e'} : \metavariable{\tau}\)
\end{lemma} \end{lemma}
\subsection{Proof of Syntactic Type Soundness} \subsection{Soundness}
\begin{lemma}[\(\beta\)-Preservation] \begin{lemma}[\(\beta\)-Preservation]
\label{lemma:beta-preservation} \label{lemma:beta-preservation}