From 3f27afa2537f10a2f1aec4bf3692da28fef8e597 Mon Sep 17 00:00:00 2001 From: Michael Sippel Date: Wed, 7 Aug 2024 16:00:01 +0200 Subject: [PATCH] paper: simplify pseudo grammar --- paper/main.tex | 164 +++++++++++++++++++++++-------------------------- 1 file changed, 77 insertions(+), 87 deletions(-) diff --git a/paper/main.tex b/paper/main.tex index b77eeb7..f0ea05a 100644 --- a/paper/main.tex +++ b/paper/main.tex @@ -1,4 +1,4 @@ -\documentclass[10pt, nonacm]{acmart} +\documentclass[10pt, sigplan, nonacm]{acmart} \usepackage[utf8]{inputenc} \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\). 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] \label{gr:core} \begin{grammar} -\firstcase{ T_\seltype \textsf{$(\typenames, \typevars)$} }{ + +\firstcase{ T }{ \metavariable{\sigma} -}{Type Literal \quad \textsf{where $ \metavariable{\sigma} \in \typenames $}} +}{Base Type} \otherform{ - \metavariable{\alpha} -}{Type Variable \quad \textsf{where $ \metavariable{\alpha} \in \typevars $}} + \metavariable{\alpha} +}{Type Variable} \otherform{ - $$\typeterminal{\forall}$$ \metavariable{\alpha} \typeterminal{.} \quad \typenonterm{\typevars \cup \{\metavariable{\alpha}\}} + \typeterminal{\forall} \metavariable{\alpha} \typeterminal{.} \nonterm{T} }{Universal Type} \otherform{ - \typeterminal{<} \typenonterm{\typevars} \quad \typenonterm{\typevars} \typeterminal{>} -}{Specialization} + \typeterminal{<} \nonterm{T} \quad \nonterm{T} \typeterminal{>} +}{Specialized Type} \otherform{ - \typenonterm{\typevars} - \quad $$\typeterminal{\rightarrow}$$ \quad - \typenonterm{\typevars} + \nonterm{T} \quad \typeterminal{\rightarrow} \quad \nonterm{T} }{Function Type} \otherform{ - \typenonterm{\typevars} - \quad $$\typeterminal{\rightarrow_{morph}}$$ \quad - \typenonterm{\typevars} + \nonterm{T} \quad \typeterminal{\rightarrow_\text{morph}} \quad \nonterm{T} }{Morphism Type} \otherform{ - \typenonterm{\typevars} - \quad $$\typeterminal{\sim}$$ \quad - \typenonterm{\typevars} + \nonterm{T} \quad \typeterminal{\sim} \quad \nonterm{T} }{Ladder Type} -\otherform{ - $$\typeterminal{(}$$ \quad - \typenonterm{\typevars} - \quad $$\typeterminal{)}$$ -}{Parenthesis} - - - - $$\\$$ - - -\firstcase{ T_\selexpr \textsc{$(\typenames, \typevars, \exprvars)$} } +\firstcase{ E +% T_\selexpr +} { \metavariable{x} -} {Variable \quad \textsf{where $\metavariable{x} \in \exprvars$} } +} {Variable} \otherform{ $$ \exprterminal{\Lambda} \metavariable{\alpha} \quad \exprterminal{\mapsto} \quad $$ - \exprnonterm{\typevars \cup \{\metavariable{\alpha}\}}{\exprvars} + \nonterm{ E } }{Type Abstraction} \otherform{ $$ \exprterminal{\lambda} \metavariable{x} $$ - \exprterminal{:} \typenonterm{\typevars} + \exprterminal{:} \nonterm{ T } \quad $$\exprterminal{\mapsto}$$ \quad - \exprnonterm{\typevars}{\exprvars \cup \{\metavariable{x}\}} + \nonterm{ E } }{Value Abstraction} \otherform{ $$ \exprterminal{\lambda} \metavariable{x} $$ - \exprterminal{:} \typenonterm{\typevars} - \quad $$\exprterminal{\mapsto_{morph}}$$ \quad - \exprnonterm{\typevars}{\exprvars \cup \{\metavariable{x}\}} + \exprterminal{:} \nonterm{ T } + \quad $$\exprterminal{\mapsto_\text{morph}}$$ \quad + \nonterm{ E } }{Value Morphism} \otherform{ \exprterminal{let} \quad \metavariable{x} \quad \exprterminal{=} \quad - \exprnonterm{\typevars}{\exprvars} + \nonterm{ E } \quad \exprterminal{in} \quad - \exprnonterm{\typevars}{\exprvars \cup \{\metavariable{x}\}} + \nonterm{ E } }{Variable Binding} \otherform{ - \exprnonterm{\typevars}{\exprvars} + \nonterm{ E } \quad - \typenonterm{\typevars} + \nonterm{ T } }{Type Application} \otherform{ - \exprnonterm{\typevars}{\exprvars} + \nonterm{ E } \quad - \exprnonterm{\typevars}{\exprvars} + \nonterm{ E } }{Value Application} \otherform{ - \exprnonterm{\typevars}{\exprvars} + \nonterm{ E } \quad \exprterminal{as} \quad - \typenonterm{\typevars} -}{Type Cast} + \nonterm{ T } +}{Up-Cast} \otherform{ - \exprterminal{(} \quad - \exprnonterm{\typevars}{\exprvars} - \quad \exprterminal{)} -}{Parenthesis} + \nonterm{ E } + \quad + \exprterminal{to} + \quad + \nonterm{ T } +}{Transformation} +\otherform{\exprterminal{(} \quad \nonterm{E} \quad \exprterminal{)}}{Parenthesis} $$\\$$ -\firstcase{ T_\textsc{Val} \textsc{$(\typenames, \typevars, \exprvars)$} }{ +\firstcase{V}{ \exprterminal{\epsilon} }{Empty Value} -\otherform{ - \metavariable{x} \quad \valnonterm{\typevars}{\exprvars} -}{Value Conactenation} - \otherform{ \exprterminal{\Lambda} \metavariable{\alpha} \quad \exprterminal{\mapsto} \quad - \valnonterm{ \typevars \cup \{ \metavariable{\alpha} \} } -\{Type-Function Value} + \nonterm{ V } +}{Type-Abstraction Value} \otherform{ - \exprterminal{\lambda} \metavariable{x} \quad - \exprterminal{:} \quad - \typenonterm{\emptyset} \quad + \exprterminal{\lambda} \metavariable{x} + \exprterminal{:} + \nonterm{ T } \quad \exprterminal{\mapsto} \quad - \exprnonterm{\typevars}{\{\metavariable{x}\}} -}{Function Value} + \nonterm{ E } +}{Abstraction Value} \otherform{ - \valnonterm{ \typevars } \quad + \nonterm{ V } \quad \exprterminal{as} \quad - \typenonterm{ \typevars } -}{Value} + \nonterm{ T } +}{Cast Value} \end{grammar} \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} @@ -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\): \begin{enumerate} -\item \typeterminal{} \( \in \typenonterm{\emptyset}\)\\ +\item \typeterminal{}\\ %\( \in \typenonterm{\emptyset}\)\\ "sequence of characters" -\item \typeterminal{ \(\sim\) Char>} \( \in \typenonterm{\emptyset}\)\\ +\item \typeterminal{ \(\sim\) Char>}\\ %\( \in \typenonterm{\emptyset}\)\\ "sequence of decimal digits, where each digit is represented as character" -\item \typeterminal{ \(\rightarrow \mathbb{N} \rightarrow\) Item} \( \in \typenonterm{\{Item\}}\)\\ +\item \typeterminal{ \(\rightarrow \mathbb{N} \rightarrow\) Item}\\ %\( \in \typenonterm{\{Item\}}\)\\ "function that maps a sequence of items and a natural number to an item"\\ -Note: this type contains the free variable \typeterminal{Item} -\item \typeterminal{ \(\sim\) UTF-8 \(\rightarrow \mathbb{N} \rightarrow\) Char } \( \in \typenonterm{\emptyset}\)\\ +%Note: this type contains the free variable \typeterminal{Item} +\item \typeterminal{ \(\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" -\item \typeterminal{\(\forall\) Radix . \(\sim\) Char>} \(\in \typenonterm{\emptyset} \)\\ -"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}\) +\item \typeterminal{\(\forall\) Radix . \(\sim\) Char>}\\ %\(\in \typenonterm{\emptyset} \)\\ +"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}\) \item \typeterminal{ \(\forall\) SrcRadix.\\ \(\forall\) DstRadix.\\ \(\mathbb{N} \sim\) \(\sim\) \(\sim\) Char>\\ \(\rightarrow_{morph}\)\\ \(\mathbb{N} \sim\) \(\sim\) \(\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}" \end{enumerate} \end{example} @@ -254,8 +242,10 @@ Note: this type-term is \emph{ground} (i.e. \(\typevars = \emptyset\)), since \t \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 \}\), -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})\). -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. +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})\). +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} \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]{ \metavariable{x} \in \exprvars\\ - \metavariable{\tau} \in \typenonterm{\emptyset}\\ + \metavariable{\tau} \in \nonterm{T}\\ \metavariable{x}:\metavariable{\tau} \in \Gamma\\ }{ \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]{ - \metavariable{\tau} \in \typenonterm{\typevars \cup \{\metavariable{\alpha}\}} \\ - \metavariable{e} \in \exprnonterm{\typevars \cup \{ \metavariable{\alpha} \}}{\exprvars} \\ + \metavariable{\tau} \in \nonterm{T} \\ + \metavariable{e} \in \nonterm{E} \\ \Gamma \vdash \metavariable{e} : \metavariable{\tau} \\ }{ \Gamma \vdash (\exprterminal{\Lambda} \metavariable{\alpha} \exprterminal{\mapsto} \metavariable{e}) : \typeterminal{\forall}\metavariable{\alpha}\typeterminal{.}\metavariable{\tau} } \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} \\ - \metavariable{\sigma} \in \typenonterm{\typevars} + \metavariable{\sigma} \in \nonterm{T} }{ \Gamma \vdash ( \metavariable{e} \quad \metavariable{\sigma} ) : \{\metavariable{\alpha} \mapsto \metavariable{\sigma}\} \metavariable{\tau} } \inferrule[T-ValueAbs]{ - \metavariable{\sigma}, \metavariable{\tau} \in \typenonterm{\typevars} \\ - \metavariable{e} \in \exprnonterm{\typevars}{\exprvars \cup \{ \metavariable{x} \} } \\ + \metavariable{\sigma}, \metavariable{\tau} \in \nonterm{T} \\ + \metavariable{e} \in \nonterm{E} \\ \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} @@ -424,8 +414,8 @@ As usual, each rule is composed of premises (above the horizontal line) and a co }\and \inferrule[T-MorphAbs]{ - \metavariable{\sigma}, \metavariable{\tau} \in \typenonterm{\typevars} \\ - \metavariable{e} \in \exprnonterm{\typevars}{\exprvars \cup \{ \metavariable{x} \} } \\ + \metavariable{\sigma}, \metavariable{\tau} \in \nonterm{T} \\ + \metavariable{e} \in \nonterm{E} \\ \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} @@ -457,7 +447,7 @@ As usual, each rule is composed of premises (above the horizontal line) and a co \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\), which are given in \ref{def:evalrules}. @@ -559,7 +549,7 @@ Then \(\emptyset \vdash \metavariable{e'} : \metavariable{\tau}\) \end{lemma} -\subsection{Proof of Syntactic Type Soundness} +\subsection{Soundness} \begin{lemma}[\(\beta\)-Preservation] \label{lemma:beta-preservation}