paper: simplify pseudo grammar

coq/equiv.v

@@ -37,7 +37,7 @@ Include Terms.
 Module Equiv.
 
 
-(** Define all rewrite steps *)
+(** Define all rewrite steps $\label{coq:type-dist}$ *)
 
 Reserved Notation "S '-->distribute-ladder' T" (at level 40).
 Inductive type_distribute_ladder : type_term -> type_term -> Prop :=
@@ -111,7 +111,7 @@ Proof.
 Qed.
 
 
-(** Define the equivalence relation as reflexive, transitive hull. *)
+(** Define the equivalence relation as reflexive, transitive hull. $\label{coq:type-equiv}$ *)
 
 Reserved Notation " S '===' T " (at level 40).
 Inductive type_eq : type_term -> type_term -> Prop :=
@@ -163,7 +163,7 @@ Proof.
   apply IHtype_eq1.
 Qed.
 
-(** "flat" types do not contain ladders *)
+(** "flat" types do not contain ladders $\label{coq:type-flat}$ *)
 Inductive type_is_flat : type_term -> Prop :=
   | FlatUnit : (type_is_flat type_unit)
   | FlatVar : forall x, (type_is_flat (type_var x))

coq/subst.v

@@ -4,8 +4,7 @@ Require Import terms.
 Include Terms.
 
 Module Subst.
-
+(* scoped variable substitution in type terms $\label{coq:subst-type}$ *)
-(* scoped variable substitution in type terms *)
 Fixpoint type_subst (v:string) (n:type_term) (t0:type_term) :=
   match t0 with
   | type_var name => if (eqb v name) then n else t0

paper/appendix.tex

@@ -0,0 +1,30 @@
+
+\onecolumn
+\appendix
+
+
+\section{Coq Listings}
+This document lists the Coq-Sourcecode from commit
+\input{|"git log -n 1 --oneline | cut -d' ' -f1"}.
+
+
+\subsection{terms.v}
+\label{coq:terms}
+\inputminted[fontsize=\footnotesize, linenos, mathescape]{coq}{../coq/terms.v}
+
+\subsection{subst.v}
+\label{coq:subst}
+\inputminted[fontsize=\footnotesize, linenos, mathescape]{coq}{../coq/subst.v}
+
+\subsection{equiv.v}
+\label{coq:equiv}
+\inputminted[fontsize=\footnotesize, linenos, mathescape]{coq}{../coq/equiv.v}
+
+\subsection{typing.v}
+\label{coq:typing}
+\inputminted[fontsize=\footnotesize, linenos, mathescape]{coq}{../coq/typing.v}
+
+\subsection{smallstep.v}
+\label{coq:smallstep}
+\inputminted[fontsize=\footnotesize, linenos, mathescape]{coq}{../coq/smallstep.v}
+

paper/main.tex

@@ -1,10 +1,26 @@
-\documentclass[10pt, nonacm]{acmart}
+\documentclass[10pt, sigplan, nonacm]{acmart}
 
 \usepackage[utf8]{inputenc}
 \usepackage{formal-grammar}
 \usepackage[dvipsnames]{xcolor}
 \usepackage{mathpartir}
+\usepackage{hyperref}
+\usepackage{url}
 
+\usepackage{minted}
+\usemintedstyle{tango}
+
+\DeclareUnicodeCharacter{2200}{$\forall$}
+\DeclareUnicodeCharacter{03C3}{$\sigma$}
+\DeclareUnicodeCharacter{03C4}{$\tau$}
+\DeclareUnicodeCharacter{03BB}{$\lambda$}
+\DeclareUnicodeCharacter{21A6}{$\mapsto$}
+\DeclareUnicodeCharacter{039B}{$\Lambda$}
+\DeclareUnicodeCharacter{03B1}{$\alpha$}
+\DeclareUnicodeCharacter{03B2}{$\beta$}
+\DeclareUnicodeCharacter{03B3}{$\gamma$}
+\DeclareUnicodeCharacter{03B4}{$\delta$}
+\DeclareUnicodeCharacter{0393}{$\Gamma$}
 
 \newcommand{\metavariable}[1]{\textcolor{teal}{#1}}
 \newcommand{\typeterminal}[1]{\textcolor{brown}{#1}}
@@ -57,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 $}}
+}{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{>}
+	\typeterminal{<} \nonterm{T} \quad \nonterm{T} \typeterminal{>}
-}{Specialization}
+}{Specialized Type}
 
 \otherform{
-	\typenonterm{\typevars}
+	\nonterm{T} \quad \typeterminal{\rightarrow} \quad \nonterm{T}
-	\quad $$\typeterminal{\rightarrow}$$ \quad
-	\typenonterm{\typevars}
 }{Function Type}
 
 \otherform{
-	\typenonterm{\typevars}
+	\nonterm{T} \quad \typeterminal{\rightarrow_\text{morph}} \quad \nonterm{T}
-	\quad $$\typeterminal{\rightarrow_{morph}}$$ \quad
-	\typenonterm{\typevars}
 }{Morphism Type}
 
 \otherform{
-	\typenonterm{\typevars}
+	\nonterm{T} \quad \typeterminal{\sim} \quad \nonterm{T}
-	\quad $$\typeterminal{\sim}$$ \quad
-	\typenonterm{\typevars}
 }{Ladder Type}
 
-\otherform{
-	$$\typeterminal{(}$$ \quad
-	\typenonterm{\typevars}
-    \quad $$\typeterminal{)}$$
-}{Parenthesis}
-
-
-
-
 $$\\$$
 
-
+\firstcase{ E
-
+% T_\selexpr
-\firstcase{ T_\selexpr \textsc{$(\typenames, \typevars, \exprvars)$} }
+}
 	{ \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}
+	\exprterminal{:} \nonterm{ T }
-    \quad $$\exprterminal{\mapsto_{morph}}$$ \quad
+    \quad $$\exprterminal{\mapsto_\text{morph}}$$ \quad
-	\exprnonterm{\typevars}{\exprvars \cup \{\metavariable{x}\}}
+	\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}
+    \nonterm{ T }
-}{Type Cast}
+}{Up-Cast}
 
 \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}
 }{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} \} }
+	\nonterm{ V }
-\{Type-Function Value}
+}{Type-Abstraction Value}
 
 \otherform{
-	\exprterminal{\lambda} \metavariable{x} \quad
+	\exprterminal{\lambda} \metavariable{x}
-	\exprterminal{:} \quad
+	\exprterminal{:}
-	\typenonterm{\emptyset} \quad
+	\nonterm{ T } \quad
 	\exprterminal{\mapsto} \quad
-	\exprnonterm{\typevars}{\{\metavariable{x}\}}
+	\nonterm{ E }
-}{Function Value}
+}{Abstraction Value}
 
 \otherform{
-	\valnonterm{ \typevars } \quad
+	\nonterm{ V } \quad
 	\exprterminal{as} \quad
-	\typenonterm{ \typevars }
+	\nonterm{ T }
-}{Value}
+}{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}
@@ -212,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{<Seq Char>} \( \in \typenonterm{\emptyset}\)\\
+\item \typeterminal{<Seq Char>}\\ %\( \in \typenonterm{\emptyset}\)\\
 "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"
-\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"\\
-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"
-\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{
 	\(\forall\) SrcRadix.\\
 	\(\forall\) DstRadix.\\
 	\(\mathbb{N} \sim\) <PosInt SrcRadix> \(\sim\) <Seq <Digit SrcRadix> \(\sim\) Char>\\
 	\(\rightarrow_{morph}\)\\
 	\(\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}"
 \end{enumerate}
 \end{example}
@@ -238,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})\).
+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}
 \metavariable{\xi} \quad \text{if } \metavariable{\xi} \in \typenames\\
@@ -296,10 +302,16 @@ in an expression \(
 
 \begin{definition}[Distributivity]
 \todo{}
+
+
+See \hyperref[coq:type-dist]{equiv.v:\ref{coq:type-dist}}.
 \end{definition}
 
 \begin{definition}[Equivalence Relation]
 \todo{}
+
+
+See \hyperref[coq:type-equiv]{equiv.v:\ref{coq:type-equiv}}.
 \end{definition}
 
 \subsubsection{Normal Forms}
@@ -347,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}
@@ -363,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{\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 (\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{\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 (\exprterminal{\lambda} \metavariable{x} \exprterminal{:} \metavariable{\sigma} \exprterminal{\mapsto} \metavariable{e}) : \metavariable{\sigma}\typeterminal{\rightarrow}\metavariable{\tau}
@@ -402,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{\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 (\exprterminal{\lambda} \metavariable{x} \exprterminal{:} \metavariable{\tau} \exprterminal{\mapsto_{morph}} \metavariable{e}) : \metavariable{\sigma}\typeterminal{\rightarrow_{morph}}\metavariable{\tau}
@@ -435,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}.
@@ -537,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}
@@ -717,5 +729,7 @@ pairs
 \subsection{Algebraic Datatypes}
 \todo{}
 
+\input{appendix}
+
 \end{document}