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

paper:work on syntax definition & substitutions

Browse source
This commit is contained in:
Michael Sippel 2024-08-08 13:17:34 +02:00
parent 3f27afa253
commit 35e0a9b62b
Signed by: senvas
GPG key ID: F96CF119C34B64A6
1 changed files with 82 additions and 47 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

129
paper/main.tex
View file

@ -116,6 +116,13 @@ $$\\$$
{ \metavariable{x}
} {Variable}
\otherform{
\exprterminal{let} \quad \metavariable{x} \quad \exprterminal{=} \quad
\nonterm{ E }
\quad \exprterminal{in} \quad
\nonterm{ E }
}{Variable Binding}
\otherform{
$$ \exprterminal{\Lambda} \metavariable{\alpha}
\quad \exprterminal{\mapsto} \quad $$
@ -136,13 +143,6 @@ $$\\$$
\nonterm{ E }
}{Value Morphism}
\otherform{
\exprterminal{let} \quad \metavariable{x} \quad \exprterminal{=} \quad
\nonterm{ E }
\quad \exprterminal{in} \quad
\nonterm{ E }
}{Variable Binding}
\otherform{
\nonterm{ E }
\quad
@ -161,23 +161,25 @@ $$\\$$
\exprterminal{as}
\quad
\nonterm{ T }
}{Up-Cast}
}{Ascription}
\otherform{
\nonterm{ E }
\quad
\exprterminal{to}
\quad
\nonterm{ T }
}{Transformation}
\otherform{\exprterminal{(} \quad \nonterm{E} \quad \exprterminal{)}}{Parenthesis}
%\otherform{
% \nonterm{ E }
% \quad
% \exprterminal{to}
% \quad
% \nonterm{ T }
%}{Transformation}
%\otherform{\exprterminal{(} \quad \nonterm{E} \quad \exprterminal{)}}{Parenthesis}
$$\\$$
\firstcase{V}{
\exprterminal{\epsilon}
}{Empty Value}
\nonterm{ V } \quad
\exprterminal{as} \quad
\nonterm{ T }
}{Ascribed Value}
\otherform{
\exprterminal{\Lambda} \metavariable{\alpha} \quad
@ -193,19 +195,14 @@ $$\\$$
\nonterm{ E }
}{Abstraction Value}
\otherform{
\nonterm{ V } \quad
\exprterminal{as} \quad
\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\)), typevariables (\(\typevars\)), and expression variables (\(\exprvars\)).
By default, assume \(\metavariable{\sigma} \in \typenames\), \(\metavariable{\alpha} \in \typevars\) and \(\metavariable{x} \in \exprvars\)
By default, assume \(\metavariable{\sigma} \in \typenames\), \(\metavariable{\alpha} \in \typevars\) and \(\metavariable{x} \in \exprvars\).
For simplicity, we write \(\metavariable{e} \in \nonterm{E}\) to say that the term \metavariable{e} is contained in the language generated by the nonterminal \(\nonterm{E}\).
$$\\$$}
\end{figure}
@ -242,9 +239,9 @@ 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
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 \nonterm{T}\) recursively with the type-term given by \(\psi_t(\metavariable{\alpha_i})\)
, while occurences of bound variables are left untouched.
Further, we assume that for all \(\tau_i\), all variable names are disjunct with the free variables of the term to which the substitution is applied.
Coq definition is at \hyperref[coq:subst-type]{subst.v:\ref{coq:subst-type}}.
\[\overline{\psi_t} \metavariable{\xi} = \begin{cases}
@ -261,9 +258,39 @@ Coq definition is at \hyperref[coq:subst-type]{subst.v:\ref{coq:subst-type}}.
\[\overline{\psi_t} \metavariable{e} = \begin{cases}
\metavariable{e} \quad \text{ if } \metavariable{e} \text{ is a variable}
\exprterminal{\Lambda \metavariable{\alpha} \mapsto} \overline{\psi_t}\metavariable{e'} \quad \text{ if \metavariable{e} is of the form } \exprterminal{\Lambda \metavariable{\alpha} \mapsto \metavariable{e'}}\\
\exprterminal{\lambda \metavariable{x} : }\overline{\psi_t}\metavariable{\tau} \exprterminal{\mapsto} \overline{\psi_t}\metavariable{e'} \quad \text{ if \metavariable{e} is of the form } \exprterminal{\lambda \metavariable{x} : \metavariable{\tau} \mapsto \metavariable{e'}}\\
\exprterminal{\lambda \metavariable{x} : }\overline{\psi_t}\metavariable{\tau} \exprterminal{\mapsto_\text{morph}} \overline{\psi_t}\metavariable{e'} \quad \text{ if \metavariable{e} is of the form } \exprterminal{\lambda \metavariable{x} : \metavariable{\tau} \mapsto_\text{morph} \metavariable{e'}}\\
\\
\exprterminal{\text{let } \metavariable{x} = }\overline{\psi_t}\metavariable{a} \exprterminal{\text{ in }} \overline{\psi_t}\metavariable{e'}
\quad \text{ if \metavariable{e} is of the form }
\exprterminal{\text{let } \metavariable{x} = \metavariable{a} \text{ in } \metavariable{e'}}
\\
\exprterminal{\Lambda \metavariable{\alpha} \mapsto} \overline{\psi_t}\metavariable{e'}
\quad \text{ if \metavariable{e} is of the form } \exprterminal{\Lambda \metavariable{\alpha} \mapsto \metavariable{e'}}
\\
\exprterminal{\lambda \metavariable{x} : }\overline{\psi_t}\metavariable{\tau} \exprterminal{\mapsto} \overline{\psi_t}\metavariable{e'}
\quad \text{ if \metavariable{e} is of the form } \exprterminal{\lambda \metavariable{x} : \metavariable{\tau} \mapsto \metavariable{e'}}
\\
\exprterminal{\lambda \metavariable{x} : }\overline{\psi_t}\metavariable{\tau} \exprterminal{\mapsto_\text{morph}} \overline{\psi_t}\metavariable{e'}
\quad \text{ if \metavariable{e} is of the form } \exprterminal{\lambda \metavariable{x} : \metavariable{\tau} \mapsto_\text{morph} \metavariable{e'}}
\\
\overline{\psi_t} \metavariable{e'} \overline{\psi_t}\metavariable{\tau}
\quad \text{ if \metavariable{e} is of the form }
\exprterminal{( \metavariable{e'} \metavariable{\tau} )}
\\
\overline{\psi_t} \metavariable{e_1} \overline{\psi_t} \metavariable{e_2}
\quad \text{ if \metavariable{e} is of the form }
\exprterminal{(\metavariable{e_1} \metavariable{e_2})}
\\
\overline{\psi_t} \metavariable{e'} \exprterminal{\text{ as }} \overline{\psi_t}\metavariable{\tau}
\quad \text{ if \metavariable{e} is of the form }
\exprterminal{ \metavariable{e'} \text{ as } \metavariable{\tau} }
\end{cases}\]
@ -276,23 +303,31 @@ Coq definition is at \hyperref[coq:subst-type]{subst.v:\ref{coq:subst-type}}.
\begin{definition}[Substitution in Expressions]
\todo{complete}
Given an expression-variable assignment \(\psi_e = \{ \metavariable{x_1} \mapsto \metavariable{t_1}, \quad \metavariable{x_2} \mapsto \metavariable{t_2}, \quad \dots \}\),
the thereby induced, lexically scoped substitution \(\overline{\psi_e}\) replaces all \emph{free} occurences of the expression variables \(\metavariable{x_i}\)
in an expression \(
e \in
\exprnonterm
{\typevars}
{\{\metavariable{x_1}, \quad \metavariable{x_2}, \quad \dots\}}
\). 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_e}\) replaces all \emph{free} occurences of the expression variables \(\metavariable{x_i}\)
in an expression \(e \in \nonterm{E} \) with the \(\psi_e(\metavariable{x_i})\)
\[\overline{\psi_e} \metavariable{e} = \begin{cases}
\metavariable{e} \quad \text{if } \metavariable{e} \in \exprvars \text{ and } \metavariable{e} \notin \text{Dom}(\psi_e)\\
\metavariable{t} \quad \text{if } \metavariable{e} \in \exprvars \text{ and } (\metavariable{e}\mapsto\metavariable{t}) \in \psi_e\\
\exprterminal{\text{let } \metavariable{x} \text{ = }} \overline{\psi_e}\metavariable{a} \exprterminal{\text{ in }} \overline{\psi_e}\metavariable{e'}
\quad \text{if }
\\
\exprterminal{\lambda\metavariable{x}:\metavariable{\tau} \mapsto } \overline{\psi_e} \metavariable{e'}
\quad \text{if \metavariable{e} is of the form }
\exprterminal{\lambda\metavariable{x}:\metavariable{\tau} \mapsto \metavariable{e'}}
\text{ and } \metavariable{x} \notin \text{Dom}(\psi_e)
\\
\exprterminal{\lambda\metavariable{x}:\metavariable{\tau} \mapsto } \overline{\psi_e \setminus \{\metavariable{x} \mapsto \metavariable{t}\}} \metavariable{e'}
\quad \text{if \metavariable{e} is of the form }
\exprterminal{\lambda\metavariable{x}:\metavariable{\tau} \mapsto \metavariable{e'}}
\text{ and } (\metavariable{x}\mapsto\metavariable{t}) \in \psi_e
\\
\[\overline{\psi} \metavariable{e} = \begin{cases}
\metavariable{e} \quad \text{if } \metavariable{\xi} \in \typenames\\
\metavariable{\tau} \quad \text{if } (\metavariable{\xi} \mapsto \metavariable{\tau}) \in \psi\\
\typeterminal{\forall} \metavariable{\alpha} \typeterminal{.} \overline{\psi}\metavariable{\xi'} \quad \text{if } \metavariable{\xi} \text{ is of the form } \typeterminal{\forall} \metavariable{\alpha} \typeterminal{.} \metavariable{\xi'} \text{ and } \metavariable{\alpha} \notin \text{Dom}(\psi)\\
\typeterminal{\forall} \metavariable{\alpha} \typeterminal{.} \metavariable{\xi'} \quad \text{if } \metavariable{\xi} \text{ is of the form } \typeterminal{\forall} \metavariable{\alpha} \typeterminal{.} \metavariable{\xi'} \text{ and } \metavariable{\alpha} \in \text{Dom}(\psi)\\
\typeterminal{<} (\overline{\psi} \metavariable{\xi_1}) \quad (\overline{\psi} \metavariable{\xi_2}) \typeterminal{>} \quad \text{if } \metavariable{\xi} \text{ is of the form } \typeterminal{<} \metavariable{\xi_1} \quad \metavariable{\xi_2} \typeterminal{>}\\
(\overline{\psi} \metavariable{\xi_1}) \typeterminal{\rightarrow} (\overline{\psi} \metavariable{\xi_2}) \quad \text{if } \metavariable{\xi} \text{ is of the form } \metavariable{\xi_1} \typeterminal{\rightarrow} \metavariable{\xi_2}\\
(\overline{\psi} \metavariable{\xi_1}) \typeterminal{\rightarrow_{morph}} (\overline{\psi} \metavariable{\xi_2}) \quad \text{if } \metavariable{\xi} \text{ is of the form } \metavariable{\xi_1} \typeterminal{\rightarrow_{morph}} \metavariable{\xi_2}\\
(\overline{\psi} \metavariable{\xi_1}) \typeterminal{\sim} (\overline{\psi} \metavariable{\xi_2}) \quad \text{if } \metavariable{\xi} \text{ is of the form } \metavariable{\xi_1} \typeterminal{\sim} \metavariable{\xi_2}\\
\end{cases}\]
\end{definition}