From 35e0a9b62b278b9ab9c1a9bb02b782f0670016d1 Mon Sep 17 00:00:00 2001 From: Michael Sippel Date: Thu, 8 Aug 2024 13:17:34 +0200 Subject: [PATCH] paper:work on syntax definition & substitutions --- paper/main.tex | 129 +++++++++++++++++++++++++++++++------------------ 1 file changed, 82 insertions(+), 47 deletions(-) diff --git a/paper/main.tex b/paper/main.tex index f0ea05a..d115285 100644 --- a/paper/main.tex +++ b/paper/main.tex @@ -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}