Compare commits
No commits in common. "3f27afa2537f10a2f1aec4bf3692da28fef8e597" and "c7794d8a89c93104b8096907f18bf883bad335da" have entirely different histories.
3f27afa253
...
c7794d8a89
4 changed files with 92 additions and 135 deletions
|
|
@ -37,7 +37,7 @@ Include Terms.
|
|||
Module Equiv.
|
||||
|
||||
|
||||
(** Define all rewrite steps $\label{coq:type-dist}$ *)
|
||||
(** Define all rewrite steps *)
|
||||
|
||||
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. $\label{coq:type-equiv}$ *)
|
||||
(** Define the equivalence relation as reflexive, transitive hull. *)
|
||||
|
||||
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 $\label{coq:type-flat}$ *)
|
||||
(** "flat" types do not contain ladders *)
|
||||
Inductive type_is_flat : type_term -> Prop :=
|
||||
| FlatUnit : (type_is_flat type_unit)
|
||||
| FlatVar : forall x, (type_is_flat (type_var x))
|
||||
|
|
|
|||
|
|
@ -4,7 +4,8 @@ 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
|
||||
|
|
|
|||
|
|
@ -1,30 +0,0 @@
|
|||
|
||||
\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}
|
||||
|
||||
186
paper/main.tex
186
paper/main.tex
|
|
@ -1,26 +1,10 @@
|
|||
\documentclass[10pt, sigplan, nonacm]{acmart}
|
||||
\documentclass[10pt, 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}}
|
||||
|
|
@ -73,139 +57,151 @@ 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 }{
|
||||
\firstcase{ T_\seltype \textsf{$(\typenames, \typevars)$} }{
|
||||
\metavariable{\sigma}
|
||||
}{Base Type}
|
||||
}{Type Literal \quad \textsf{where $ \metavariable{\sigma} \in \typenames $}}
|
||||
|
||||
\otherform{
|
||||
\metavariable{\alpha}
|
||||
}{Type Variable}
|
||||
}{Type Variable \quad \textsf{where $ \metavariable{\alpha} \in \typevars $}}
|
||||
|
||||
\otherform{
|
||||
\typeterminal{\forall} \metavariable{\alpha} \typeterminal{.} \nonterm{T}
|
||||
$$\typeterminal{\forall}$$ \metavariable{\alpha} \typeterminal{.} \quad \typenonterm{\typevars \cup \{\metavariable{\alpha}\}}
|
||||
}{Universal Type}
|
||||
|
||||
\otherform{
|
||||
\typeterminal{<} \nonterm{T} \quad \nonterm{T} \typeterminal{>}
|
||||
}{Specialized Type}
|
||||
\typeterminal{<} \typenonterm{\typevars} \quad \typenonterm{\typevars} \typeterminal{>}
|
||||
}{Specialization}
|
||||
|
||||
\otherform{
|
||||
\nonterm{T} \quad \typeterminal{\rightarrow} \quad \nonterm{T}
|
||||
\typenonterm{\typevars}
|
||||
\quad $$\typeterminal{\rightarrow}$$ \quad
|
||||
\typenonterm{\typevars}
|
||||
}{Function Type}
|
||||
|
||||
\otherform{
|
||||
\nonterm{T} \quad \typeterminal{\rightarrow_\text{morph}} \quad \nonterm{T}
|
||||
\typenonterm{\typevars}
|
||||
\quad $$\typeterminal{\rightarrow_{morph}}$$ \quad
|
||||
\typenonterm{\typevars}
|
||||
}{Morphism Type}
|
||||
|
||||
\otherform{
|
||||
\nonterm{T} \quad \typeterminal{\sim} \quad \nonterm{T}
|
||||
\typenonterm{\typevars}
|
||||
\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}
|
||||
} {Variable \quad \textsf{where $\metavariable{x} \in \exprvars$} }
|
||||
|
||||
\otherform{
|
||||
$$ \exprterminal{\Lambda} \metavariable{\alpha}
|
||||
\quad \exprterminal{\mapsto} \quad $$
|
||||
\nonterm{ E }
|
||||
\exprnonterm{\typevars \cup \{\metavariable{\alpha}\}}{\exprvars}
|
||||
}{Type Abstraction}
|
||||
|
||||
\otherform{
|
||||
$$ \exprterminal{\lambda} \metavariable{x} $$
|
||||
\exprterminal{:} \nonterm{ T }
|
||||
\exprterminal{:} \typenonterm{\typevars}
|
||||
\quad $$\exprterminal{\mapsto}$$ \quad
|
||||
\nonterm{ E }
|
||||
\exprnonterm{\typevars}{\exprvars \cup \{\metavariable{x}\}}
|
||||
}{Value Abstraction}
|
||||
|
||||
\otherform{
|
||||
$$ \exprterminal{\lambda} \metavariable{x} $$
|
||||
\exprterminal{:} \nonterm{ T }
|
||||
\quad $$\exprterminal{\mapsto_\text{morph}}$$ \quad
|
||||
\nonterm{ E }
|
||||
\exprterminal{:} \typenonterm{\typevars}
|
||||
\quad $$\exprterminal{\mapsto_{morph}}$$ \quad
|
||||
\exprnonterm{\typevars}{\exprvars \cup \{\metavariable{x}\}}
|
||||
}{Value Morphism}
|
||||
|
||||
\otherform{
|
||||
\exprterminal{let} \quad \metavariable{x} \quad \exprterminal{=} \quad
|
||||
\nonterm{ E }
|
||||
\exprnonterm{\typevars}{\exprvars}
|
||||
\quad \exprterminal{in} \quad
|
||||
\nonterm{ E }
|
||||
\exprnonterm{\typevars}{\exprvars \cup \{\metavariable{x}\}}
|
||||
}{Variable Binding}
|
||||
|
||||
\otherform{
|
||||
\nonterm{ E }
|
||||
\exprnonterm{\typevars}{\exprvars}
|
||||
\quad
|
||||
\nonterm{ T }
|
||||
\typenonterm{\typevars}
|
||||
}{Type Application}
|
||||
|
||||
\otherform{
|
||||
\nonterm{ E }
|
||||
\exprnonterm{\typevars}{\exprvars}
|
||||
\quad
|
||||
\nonterm{ E }
|
||||
\exprnonterm{\typevars}{\exprvars}
|
||||
}{Value Application}
|
||||
|
||||
\otherform{
|
||||
\nonterm{ E }
|
||||
\exprnonterm{\typevars}{\exprvars}
|
||||
\quad
|
||||
\exprterminal{as}
|
||||
\quad
|
||||
\nonterm{ T }
|
||||
}{Up-Cast}
|
||||
\typenonterm{\typevars}
|
||||
}{Type Cast}
|
||||
|
||||
\otherform{
|
||||
\nonterm{ E }
|
||||
\quad
|
||||
\exprterminal{to}
|
||||
\quad
|
||||
\nonterm{ T }
|
||||
}{Transformation}
|
||||
\otherform{\exprterminal{(} \quad \nonterm{E} \quad \exprterminal{)}}{Parenthesis}
|
||||
\exprterminal{(} \quad
|
||||
\exprnonterm{\typevars}{\exprvars}
|
||||
\quad \exprterminal{)}
|
||||
}{Parenthesis}
|
||||
|
||||
|
||||
$$\\$$
|
||||
|
||||
\firstcase{V}{
|
||||
\firstcase{ T_\textsc{Val} \textsc{$(\typenames, \typevars, \exprvars)$} }{
|
||||
\exprterminal{\epsilon}
|
||||
}{Empty Value}
|
||||
|
||||
\otherform{
|
||||
\metavariable{x} \quad \valnonterm{\typevars}{\exprvars}
|
||||
}{Value Conactenation}
|
||||
|
||||
\otherform{
|
||||
\exprterminal{\Lambda} \metavariable{\alpha} \quad
|
||||
\exprterminal{\mapsto} \quad
|
||||
\nonterm{ V }
|
||||
}{Type-Abstraction Value}
|
||||
\valnonterm{ \typevars \cup \{ \metavariable{\alpha} \} }
|
||||
\{Type-Function Value}
|
||||
|
||||
\otherform{
|
||||
\exprterminal{\lambda} \metavariable{x}
|
||||
\exprterminal{:}
|
||||
\nonterm{ T } \quad
|
||||
\exprterminal{\lambda} \metavariable{x} \quad
|
||||
\exprterminal{:} \quad
|
||||
\typenonterm{\emptyset} \quad
|
||||
\exprterminal{\mapsto} \quad
|
||||
\nonterm{ E }
|
||||
}{Abstraction Value}
|
||||
\exprnonterm{\typevars}{\{\metavariable{x}\}}
|
||||
}{Function Value}
|
||||
|
||||
\otherform{
|
||||
\nonterm{ V } \quad
|
||||
\valnonterm{ \typevars } \quad
|
||||
\exprterminal{as} \quad
|
||||
\nonterm{ T }
|
||||
}{Cast Value}
|
||||
\typenonterm{ \typevars }
|
||||
}{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\)), typevariables (\(\typevars\)), and expression variables (\(\exprvars\)).
|
||||
By default, assume \(\metavariable{\sigma} \in \typenames\), \(\metavariable{\alpha} \in \typevars\) and \(\metavariable{x} \in \exprvars\)
|
||||
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\)).
|
||||
$$\\$$}
|
||||
|
||||
\end{figure}
|
||||
|
|
@ -216,25 +212,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}
|
||||
\item \typeterminal{<Seq Char> \(\sim\) UTF-8 \(\rightarrow \mathbb{N} \rightarrow\) Char }\\ %\( \in \typenonterm{\emptyset}\)\\
|
||||
Note: this type contains the free variable \typeterminal{Item}
|
||||
\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} \)\\
|
||||
"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 . <Seq <Digit 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\) <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}
|
||||
|
|
@ -242,10 +238,8 @@ The following terms are valid types over \(\Sigma\):
|
|||
|
||||
\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, 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}}.
|
||||
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.
|
||||
|
||||
\[\overline{\psi_t} \metavariable{\xi} = \begin{cases}
|
||||
\metavariable{\xi} \quad \text{if } \metavariable{\xi} \in \typenames\\
|
||||
|
|
@ -302,16 +296,10 @@ 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}
|
||||
|
|
@ -359,7 +347,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 \nonterm{T}\\
|
||||
\metavariable{\tau} \in \typenonterm{\emptyset}\\
|
||||
\metavariable{x}:\metavariable{\tau} \in \Gamma\\
|
||||
}{
|
||||
\Gamma \vdash \metavariable{x}:\metavariable{\tau}
|
||||
|
|
@ -375,25 +363,25 @@ As usual, each rule is composed of premises (above the horizontal line) and a co
|
|||
|
||||
|
||||
\inferrule[T-TypeAbs]{
|
||||
\metavariable{\tau} \in \nonterm{T} \\
|
||||
\metavariable{e} \in \nonterm{E} \\
|
||||
\metavariable{\tau} \in \typenonterm{\typevars \cup \{\metavariable{\alpha}\}} \\
|
||||
\metavariable{e} \in \exprnonterm{\typevars \cup \{ \metavariable{\alpha} \}}{\exprvars} \\
|
||||
\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 \nonterm{T} \\
|
||||
\metavariable{\tau} \in \typenonterm{\typevars \cup \{\metavariable{\alpha}\}} \\
|
||||
\Gamma \vdash \metavariable{e} : \typeterminal{\forall} \metavariable{\alpha} \typeterminal{.} \metavariable{\tau} \\
|
||||
\metavariable{\sigma} \in \nonterm{T}
|
||||
\metavariable{\sigma} \in \typenonterm{\typevars}
|
||||
}{
|
||||
\Gamma \vdash ( \metavariable{e} \quad \metavariable{\sigma} ) : \{\metavariable{\alpha} \mapsto \metavariable{\sigma}\} \metavariable{\tau}
|
||||
}
|
||||
|
||||
|
||||
\inferrule[T-ValueAbs]{
|
||||
\metavariable{\sigma}, \metavariable{\tau} \in \nonterm{T} \\
|
||||
\metavariable{e} \in \nonterm{E} \\
|
||||
\metavariable{\sigma}, \metavariable{\tau} \in \typenonterm{\typevars} \\
|
||||
\metavariable{e} \in \exprnonterm{\typevars}{\exprvars \cup \{ \metavariable{x} \} } \\
|
||||
\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}
|
||||
|
|
@ -414,8 +402,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 \nonterm{T} \\
|
||||
\metavariable{e} \in \nonterm{E} \\
|
||||
\metavariable{\sigma}, \metavariable{\tau} \in \typenonterm{\typevars} \\
|
||||
\metavariable{e} \in \exprnonterm{\typevars}{\exprvars \cup \{ \metavariable{x} \} } \\
|
||||
\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}
|
||||
|
|
@ -447,7 +435,7 @@ As usual, each rule is composed of premises (above the horizontal line) and a co
|
|||
\end{definition}
|
||||
|
||||
|
||||
\subsection{Evaluation}
|
||||
\subsection{Evaluation Semantics}
|
||||
|
||||
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}.
|
||||
|
|
@ -549,7 +537,7 @@ Then \(\emptyset \vdash \metavariable{e'} : \metavariable{\tau}\)
|
|||
|
||||
\end{lemma}
|
||||
|
||||
\subsection{Soundness}
|
||||
\subsection{Proof of Syntactic Type Soundness}
|
||||
|
||||
\begin{lemma}[\(\beta\)-Preservation]
|
||||
\label{lemma:beta-preservation}
|
||||
|
|
@ -729,7 +717,5 @@ pairs
|
|||
\subsection{Algebraic Datatypes}
|
||||
\todo{}
|
||||
|
||||
\input{appendix}
|
||||
|
||||
\end{document}
|
||||
|
||||
|
|
|
|||
Loading…
Reference in a new issue