From e0811ff06f2849262d66a85ead2a4e4f81432837 Mon Sep 17 00:00:00 2001 From: Jonathan Chan Date: Mon, 21 Apr 2025 14:42:32 -0400 Subject: [PATCH] Move stuff around to get rid of a big blank space --- cbpv.mng | 24 ++++++++++++------------ cbpv.pdf | 4 ++-- cbpv.tex | 24 ++++++++++++------------ 3 files changed, 26 insertions(+), 26 deletions(-) diff --git a/cbpv.mng b/cbpv.mng index 5ed10dc..bef6301 100644 --- a/cbpv.mng +++ b/cbpv.mng @@ -86,18 +86,7 @@ and the challenges posed by using Lean in \cref{sec:discussion}. \section{Syntax and Typing} \label{sec:syntax} -\begin{align*} - [[A]] &\Coloneqq [[Unit]] \mid [[A1 + A2]] \mid [[U B]] & \textit{value types} \\ - [[B]] &\Coloneqq [[A → B]] \mid [[F A]] & \textit{computation types} \\ - [[v]], [[w]] &\Coloneqq [[x]] \mid [[unit]] \mid [[inl v]] \mid [[inr v]] \mid [[thunk m]] & \textit{values} \\ - [[m]], [[n]] &\Coloneqq [[force v]] \mid [[λx. m]] \mid [[m v]] \mid [[ret v]] & \textit{computations} \\ - & \mid [[let x m n]] \\ - & \mid [[case v | y.m | z.n]] \\ - [[G]] &\Coloneqq [[•]] \mid [[G, x : A]] & \textit{typing contexts} \\ - [[s]] &\Coloneqq [[•]] \mid [[s, x ↦ v]] & \textit{simultaneous substitutions} -\end{align*} - -The grammar of the CBPV for this project is given above. +The grammar of the CBPV for this project is given below. Terms and their types are divided between \emph{values} and \emph{computations}. Values are variables, unit, injections into a sum type, or a thunked computation, while computations are forcing thunks, @@ -115,6 +104,17 @@ with $[[•]]$ as the identity substitution. Applying a substitution is represented as $[[v{s}]]$ and $[[m{s}]]$, and implemented in terms of renamings, which are mappings from variables to other variables. +% +\begin{align*} + [[A]] &\Coloneqq [[Unit]] \mid [[A1 + A2]] \mid [[U B]] & \textit{value types} \\ + [[B]] &\Coloneqq [[A → B]] \mid [[F A]] & \textit{computation types} \\ + [[v]], [[w]] &\Coloneqq [[x]] \mid [[unit]] \mid [[inl v]] \mid [[inr v]] \mid [[thunk m]] & \textit{values} \\ + [[m]], [[n]] &\Coloneqq [[force v]] \mid [[λx. m]] \mid [[m v]] \mid [[ret v]] & \textit{computations} \\ + & \mid [[let x m n]] \\ + & \mid [[case v | y.m | z.n]] \\ + [[G]] &\Coloneqq [[•]] \mid [[G, x : A]] & \textit{typing contexts} \\ + [[s]] &\Coloneqq [[•]] \mid [[s, x ↦ v]] & \textit{simultaneous substitutions} +\end{align*} This is not the usual complete CBPV language, since it's missing both value tuples and computation tuples. diff --git a/cbpv.pdf b/cbpv.pdf index c4d2293..6a02e38 100644 --- a/cbpv.pdf +++ b/cbpv.pdf @@ -1,3 +1,3 @@ version https://git-lfs.github.com/spec/v1 -oid sha256:3f9ad844241135ba18c1223004db36ab7dde032d8da90a76e1187f8ede357d46 -size 325129 +oid sha256:fbd568b1ed15f6c815a15f610ed84cc6fec339a72732f4dbdb2f4330563ebe8f +size 324611 diff --git a/cbpv.tex b/cbpv.tex index 9953df2..a952c9f 100644 --- a/cbpv.tex +++ b/cbpv.tex @@ -86,18 +86,7 @@ and the challenges posed by using Lean in \cref{sec:discussion}. \section{Syntax and Typing} \label{sec:syntax} -\begin{align*} - \ottnt{A} &\Coloneqq \kw{Unit} \mid \ottnt{A_{{\mathrm{1}}}} + \ottnt{A_{{\mathrm{2}}}} \mid \kw{U} \gap \ottnt{B} & \textit{value types} \\ - \ottnt{B} &\Coloneqq \ottnt{A} \rightarrow \ottnt{B} \mid \kw{F} \gap \ottnt{A} & \textit{computation types} \\ - \ottnt{v}, \ottnt{w} &\Coloneqq \ottmv{x} \mid \kw{unit} \mid \kw{inl} \gap \ottnt{v} \mid \kw{inr} \gap \ottnt{v} \mid \kw{thunk} \gap \ottnt{m} & \textit{values} \\ - \ottnt{m}, \ottnt{n} &\Coloneqq \kw{force} \gap \ottnt{v} \mid \lambda \ottmv{x} \mathpunct{.} \ottnt{m} \mid \ottnt{m} \gap \ottnt{v} \mid \kw{return} \gap \ottnt{v} & \textit{computations} \\ - & \mid \kw{let} \gap \ottmv{x} \leftarrow \ottnt{m} \gap \kw{in} \gap \ottnt{n} \\ - & \mid \kw{case} \gap \ottnt{v} \gap \kw{of} \gap \lbrace \kw{inl} \gap \ottmv{y} \Rightarrow \ottnt{m} \mathrel{;} \kw{inr} \gap \ottmv{z} \Rightarrow \ottnt{n} \rbrace \\ - \Gamma &\Coloneqq \cdot \mid \Gamma , \ottmv{x} \mathbin{:} \ottnt{A} & \textit{typing contexts} \\ - \sigma &\Coloneqq \cdot \mid \sigma , \ottmv{x} \mapsto \ottnt{v} & \textit{simultaneous substitutions} -\end{align*} - -The grammar of the CBPV for this project is given above. +The grammar of the CBPV for this project is given below. Terms and their types are divided between \emph{values} and \emph{computations}. Values are variables, unit, injections into a sum type, or a thunked computation, while computations are forcing thunks, @@ -115,6 +104,17 @@ with $ \cdot $ as the identity substitution. Applying a substitution is represented as $ \ottnt{v} [ \sigma ] $ and $ \ottnt{m} [ \sigma ] $, and implemented in terms of renamings, which are mappings from variables to other variables. +% +\begin{align*} + \ottnt{A} &\Coloneqq \kw{Unit} \mid \ottnt{A_{{\mathrm{1}}}} + \ottnt{A_{{\mathrm{2}}}} \mid \kw{U} \gap \ottnt{B} & \textit{value types} \\ + \ottnt{B} &\Coloneqq \ottnt{A} \rightarrow \ottnt{B} \mid \kw{F} \gap \ottnt{A} & \textit{computation types} \\ + \ottnt{v}, \ottnt{w} &\Coloneqq \ottmv{x} \mid \kw{unit} \mid \kw{inl} \gap \ottnt{v} \mid \kw{inr} \gap \ottnt{v} \mid \kw{thunk} \gap \ottnt{m} & \textit{values} \\ + \ottnt{m}, \ottnt{n} &\Coloneqq \kw{force} \gap \ottnt{v} \mid \lambda \ottmv{x} \mathpunct{.} \ottnt{m} \mid \ottnt{m} \gap \ottnt{v} \mid \kw{return} \gap \ottnt{v} & \textit{computations} \\ + & \mid \kw{let} \gap \ottmv{x} \leftarrow \ottnt{m} \gap \kw{in} \gap \ottnt{n} \\ + & \mid \kw{case} \gap \ottnt{v} \gap \kw{of} \gap \lbrace \kw{inl} \gap \ottmv{y} \Rightarrow \ottnt{m} \mathrel{;} \kw{inr} \gap \ottmv{z} \Rightarrow \ottnt{n} \rbrace \\ + \Gamma &\Coloneqq \cdot \mid \Gamma , \ottmv{x} \mathbin{:} \ottnt{A} & \textit{typing contexts} \\ + \sigma &\Coloneqq \cdot \mid \sigma , \ottmv{x} \mapsto \ottnt{v} & \textit{simultaneous substitutions} +\end{align*} This is not the usual complete CBPV language, since it's missing both value tuples and computation tuples.