\section{Proofs of Section~\ref{sec:correctness}}\label{app:correctness}
\begin{theorem}[Soundness]
	Let $s$ be a Space KAM\xspace reachable state such that there is a derivation $\pi\;\triangleright\wtjudg{}{w}{s}{\star}$. Then 
	\begin{enumerate}
		\item \emph{Termination}: there is a run $\rho:s\mathrm{\Rew{SpKAM\xspace}}^*s_{f}$ to a final state. Moreover,
		\item \emph{Space bound}: $w=\lm\rho$.	
	\end{enumerate}
\end{theorem}

\begin{proof}
	The proof is by induction on $\size\pi$ and case analysis on whether $s$ is final. If $s$ is final then the run $\rho$ in the statement is given by the empty run. Therefore, we have $\lm\rho = \sizes$ and the required space bound becomes $w= \sizes$, which is given by \refprop{weight-of-final-states-is-right}. If $s$ is not final then $s\mathrm{\Rew{SpKAM\xspace}}{\state'}$. By examining all the transition rules. We set $A:=\arr{\mathcal{A}_1^{k_{1}}}{\arr{\cdots}{\arr{\mathcal{A}_n^{k_{n}}}{\star}}}$ and $S:=S_1\cdotsS_n$.
	\begin{itemize}
		\item Case $\tomachhole{\seavsym}$, i.e.\xspace
		$s=\spkamstate{tx}{e}S$ and 
		${\state'}=\spkamstatet{ 
			e|_t}{e(x)\cdotS}$. The type derivation $\pi$ typing  $s$ has the following shape:
		\[
		\infer[\textsc{T-st}]{\wtjudg{}{\max_i\{w',u,v_i\}}{\spkamstate{tx}eS}{\star}}{
			\infer[\textsc{T-@}_{2}]{\wtjudg{\Gamma\uplusx:\mathcal{A}}{w'}{tx}{A} }{\wtjudg{\Gamma}{w'}{t}{\arr{\mathcal{A}}{A}}}
			&
			\pi_{e}\;\triangleright\wtjudg{}{u}{e}{\Gamma\uplusx:\mathcal{A}}
			&
			\wtjudg{}{v_i}{S_i}{\mathcal{A}_i^{k_{i}}} 
		}
		\]
		with $w = \max_i\{w',v_i,u\}$. By \reflemma{multiset-splitting}, there are two derivations $\pi_{\Gamma}\;\triangleright\wtjudg{}{u_{\Gamma}}{e|_{\dom\Gamma}}{\Gamma}$ and $\pi_{x:\mathcal{A}}\;\triangleright\wtjudg{}{u_{x:\mathcal{A}}}{e(x)}{x:\mathcal{A}}$ such that $\size{\pi_{e}} = \size{\pi_{\Gamma}} + \size{\pi_{x:\mathcal{A}}}$ and $u = \max\set{u_{\Gamma}, u_{x:\mathcal{A}}}$. By the environment domain invariant (\reflemma{spkam-invariants}), $\dom\Gamma = \fvt$. Moreover, $\pi_{x:\mathcal{A}}$ is necessarily the conclusion of a unary $\textsc{T-env}$ rule of premise $\pi_{\mathcal{A}}\;\triangleright\wtjudg{}{u_{\mathcal{A}}}{e(x)}{\mathcal{A}}$ for which $\size{\pi_{\mathcal{A}}} = \size{\pi_{x:\mathcal{A}}}$ and $u_{\mathcal{A}} = u_{x:\mathcal{A}}$.
		Then, ${\state'}$ can be typed by the following derivation $\tyd'$:
		\[\tyd' := 
		\infer[\textsc{T-st}]{\wtjudg{}{\max_i\{w',u_{\Gamma},u_{\mathcal{A}},v_i\}}{\spkamstatet{ 
					e|_t}{e(x)\cdotS}}{\star}}{
			\wtjudg{\Gamma'}{w'}{t}{\arr{\mathcal{A}}{A}}
			&
			\pi_{\Gamma}\;\triangleright \wtjudg{}{u_{\Gamma}}{e|_t}{\Gamma}
			&
			\pi_{\mathcal{A}}\;\triangleright \wtjudg{}{u_{\mathcal{A}}}{e(x)}{\mathcal{A}}
			&
			\wtjudg{}{v_i}{S_i}{\mathcal{A}_i^{k_{i}}} 
		}
		\]
		Since $\size{\pi_{e}} = \size{\pi_{\Gamma}} + \size{\pi_{x:\mathcal{A}}} = \size{\pi_{\Gamma}} + \size{\pi_{\mathcal{A}}}$, we have $\size\pi > \size\tyd'$ (beccause the $\textsc{T-@}_{2}$ rule is removed), and so we can apply the \textit{i.h.}\xspace, obtaining a run $\sigma: {\state'} \mathrm{\Rew{SpKAM\xspace}}^{*} s_{f}$ to a final state such that $\max_i\{w',u_{\Gamma},u_{\mathcal{A}},v_i\} = \lm\sigma$. Then there is a run $\rho:s \mathrm{\Rew{SpKAM\xspace}}^{*} s_{f}$, proving the first part of the statement (termination).
		
		For the space bound, note that, since $u = \max\set{u_{\Gamma}, u_{x:\mathcal{A}}} = \max\set{u_{\Gamma}, u_{\mathcal{A}}}$, we have $w = \max_i\{w',u_{\Gamma},u_{\mathcal{A}},v_i\}$. Additionally, $\sizes \leq \size{\state'}$, because by the environment domain invariant $e|_t$ removes at most $e(x)$ from $e$, which is however added to the stack. Then $\lm\rho = \lm\sigma = \max_i\{w',u_{\Gamma},u_{\mathcal{A}},v_i\} = w$, proving the second part of the statement.
	
	
		\item Case $\tomachhole{\seanvsym}$, i.e.\xspace $s=\spkamstate{tu}{e}S$ 
		and 
		${\state'}=\spkamstatet{ 
			e|_t}{(u,e|_u)\cdotS}$. 
		
		
		The type derivation $\pi$ typing  $s$ has the following shape:
		\[
		\infer[\textsc{T-st}]{\wtjudg{}{\max_i\{w_1,w_2,v_i,u\}}{\spkamstate{tu}eS}{\star}}{
			\infer[\textsc{T-@}_{1}]{\wtjudg{\Gamma\uplus\Delta}{\max\{w_1,w_2\}}{tu}{A } }{\wtjudg{\Gamma}{w_1}{t}{\arr{\mathcal{A}^{k}}{A}}
				& 
				\wtjudg{\Delta}{w_2}{u}{\mathcal{A}^{k}}& \Gamma\# \Delta}
			&
			\wtjudg{}{u}{e}{\Gamma\uplus\Delta}
			&
			\wtjudg{}{v_i}{S_i}{\mathcal{A}_i^{k_{i}}} 
		}
		\]
		with $w = \max_i\{w_1,w_2,v_i,u\}$. By \reflemmap{multiset-splitting}{env}, there are two derivations $\pi_{\Gamma}\;\triangleright\wtjudg{}{u_{\Gamma}}{e|_{\dom\Gamma}}{\Gamma}$ and $\pi_{\Delta}\;\triangleright\wtjudg{}{u_{\Delta}}{e|_{\dom\Delta}}{\Delta}$ such that $\size{\pi_{e}} = \size{\pi_{\Gamma}} + \size{\pi_{\Delta}}$ and $u = \max\set{u_{\Gamma}, u_{\Delta}}$. By the environment domain invarian (\reflemma{spkam-invariants}), $\dom\Gamma = \fvt$ and $\dom\Delta = \fvu$.		Then, ${\state'}$ can be typed by the following derivation $\tyd'$:
		\[\tyd' := 
		\infer[\textsc{T-st}]{\wtjudg{}{
				\max_i\{w_{1},w_{2},v_i,u_{\Gamma},u_{\Delta}\}}{\spkamstatet{ 
					e|_t}{(u,e|_u)\cdotS}}{\star}}{
			\wtjudg{\Gamma}{w_1}{t}{\arr{\mathcal{A}^{k}}{A}}
			&
			\wtjudg{}{u_{\Gamma}}{e|_t}{\Gamma}
			&
			\infer[\textsc{T-cl}]{\wtjudg{}{\max\{w_{2},u_{\Delta}\}
				}{(u,e|_u)}{\mathcal{A}^k}}{\wtjudg{\Delta}{w_2}{u}{\mathcal{A}^{k}}&&
				\wtjudg{}{u_{\Delta}}{e|_u}{\Delta}}
			&
			\wtjudg{}{v_i}{S_i}{\mathcal{A}_i^{k_{i}}} 
		}
		\]
		Since $\size{\pi_{e}} = \size{\pi_{\Gamma}} + \size{\pi_{\Delta}}$, we have $\size\pi > \size\tyd'$ (beccause the $\textsc{T-@}_{2}$ rule is removed and rule $\textsc{T-cl}$ does not count for the size), and so we can apply the \textit{i.h.}\xspace, obtaining a run $\sigma: {\state'} \mathrm{\Rew{SpKAM\xspace}}^{*} s_{f}$ to a final state such that $\max_i\{w_{1},w_{2},v_i,u_{\Gamma},u_{\Delta}\} = \lm\sigma$. Then there is a run $\rho:s \mathrm{\Rew{SpKAM\xspace}}^{*} s_{f}$, proving the first part of the statement (termination).
		
		For the space bound, note that, since $u = \max\set{u_{\Gamma}, u_{\Delta}}$, we have $\max_i\{w_{1},w_{2},v_i,u_{\Gamma},u_{\Delta}\} = \max_i\{w_{1},w_{2},v_i,u\} = w$. Additionally, $\sizes \leq \size{\state'}$, because by the environment domain invariant all the pointer is $e$ are in $e|_t$ or in $e|_{u}$. Then $\lm\rho = \lm\sigma = \max_i\{w',u_{\Gamma},u_{\mathcal{A}},v_i\} = w$, proving the second part of the statement.
	
	
		\item Case $\tomachhole{\bwsym}$, i.e.\xspace $s=\spkamstate{\la\vart}{e}{c\cdotS}$ 
		and 
		${\state'}=\spkamstatet{ 
			e}{S}$. The type derivation $\pi$ typing  $s$ has the following shape:
		\[
		\infer[\textsc{T-st}]{\wtjudg{}{\max_i\{w',\size\Gamma+\sizeA+k,u,v,v_i\}}{\spkamstate{\la\vart}e{c\cdotS}}{\star}}{
			\infer[\textsc{T-}\lambda_{2}]{\wtjudg{\Gamma}{\max\{w',\size\Gamma+\sizeA+k\}}{\lambdax.t}{\arr{\mset{\,}^{k}}{A}}}
			{\wtjudg{\Gamma}{w'}{t}{A} & x\notin\dom\Gamma}
			&
			\wtjudg{}{u}{e}{\Gamma}
			&
			\wtjudg{}{v}{c}{\mset{\,}^k}
			&
			\wtjudg{}{v_i}{S_i}{\mathcal{A}_i^{k_{i}}} 
		}\]
		with $w = \max_i\{w',\size\Gamma+\sizeA+k,u,v,v_i\}$. The target state ${\state'}$ can be typed by the following derivation $\tyd'$:
		\[\tyd' :=
		\infer[\textsc{T-st}]{\wtjudg{}{\max_i\{w',u,v_i\}}{\spkamstateteS}{\star}}{
			\wtjudg{\Gamma}{w'}{t}{A} & x\notin\dom\Gamma
			&
			\wtjudg{}{u}{e}{\Gamma}
			&
			\wtjudg{}{v_i}{S_i}{\mathcal{A}_i^{k_{i}}} 
		}\]
		Since the $\textsc{T-}\lambda_{2}$ rule is removed, we have $\size\pi>\size\tyd'$, and so we can apply the \textit{i.h.}\xspace, obtaining a run $\sigma: {\state'} \mathrm{\Rew{SpKAM\xspace}}^{*} s_{f}$ to a final state such that $\max_i\{w',u,v_i\} = \lm\sigma$. Then there is a run $\rho:s \mathrm{\Rew{SpKAM\xspace}}^{*} s_{f}$, proving the first part of the statement (termination).
		
		For the space bound, note that:
		\begin{itemize}
			\item $\sizes =  \size\Gamma+\sizeA+k$ by \reflemma{space-bound-on-current-state}, giving $w = \max_i\{w',\sizes,u,v,v_i\}$. 
			\item $v=0$ by \reflemmap{dry-env-clos}{two}, giving $w = \max_i\{w',\sizes,u,v_i\}$.
		\end{itemize}
		Now, there are two cases:
		\begin{itemize}
			\item $\lm\rho = \lm\sigma$: that is, $\sizes \leq \lm\sigma = \max_i\{w',u,v_i\}$. Then $\sizes \leq \max_i\{w',u,v_i\}$, and so $w = \max_i\{w',\sizes,u,v_i\} = \max_i\{w',u,v_i\} =_{\textit{i.h.}\xspace} \lm\sigma = \lm\rho$.
			
			\item $\lm\rho > \lm\sigma$: that is, $\sizes > \lm\sigma = \max_i\{w',u,v_i\}$. Then $\sizes > \max_i\{w',u,v_i\}$, and so $w = \max_i\{w',\sizes,u,v_i\} = \sizes = \lm\rho$.
		\end{itemize}
		
	
	
		\item Case $\tomachhole{\bnwsym}$, i.e.\xspace $s=\spkamstate{\la\vart}{e}{c\cdotS}$ 
		and 
		${\state'}=\spkamstatet{ 
			\esub{x}{c}\cdote}{S}$. The type derivation $\pi$ typing  $s$ has the following shape:
		\[
		\infer[\textsc{T-st}]{\wtjudg{}{\max_i\{w',v,v_i,u\}}{\spkamstate{\la\vart}e{c\cdotS}}{\star}}{
			\infer[\textsc{T-}\lambda_{1}]{\wtjudg{\Gamma}{w'}{\lambdax.t}{\arr{\mathcal{A}^{k}}{A}}} 
			{\wtjudg{\Gamma,x:\mathcal{A}^{k}}{w'}{t}{A}}
			&
			\wtjudg{}{u}{e}{\Gamma}
			&
			\wtjudg{}{v}{c}{\mathcal{A}^k}
			&
			\wtjudg{}{v_i}{S_i}{\mathcal{A}_i^{k_{i}}} 
		}\]
		with $w = \max_i\{w',v,v_i,u\}$. The target state ${\state'}$ can be typed by the following derivation $\tyd'$:
		\[\tyd':=
		\infer[\textsc{T-st}]{\wtjudg{}{\max_i\{w',v,v_i,u\}} {\spkamstatet{\esubxc\cdote}S}{\star}}{
			\wtjudg{\Gamma,x:\mathcal{A}^{k}}{w'}{t}{A}
			&
			\infer[\textsc{T-env}]{\wtjudg{}{\max\{u,v\}}{\esubxc\cdote}{\Gamma,x:\mathcal{A}^{k}}} {\wtjudg{}{u}{e}{\Gamma}&\wtjudg{}{v}{c}{\mathcal{A}^k}}
			&
			\wtjudg{}{v_i}{S_i}{\mathcal{A}_i^{k_{i}}} 
		}\]
		Since the $\textsc{T-}\lambda_{1}$ rule is removed and the $\textsc{T-env}$ rule does not count for the size of type derivations, we have $\size\pi>\size\tyd'$, and so we can apply the \textit{i.h.}\xspace, obtaining a run $\sigma: {\state'} \mathrm{\Rew{SpKAM\xspace}}^{*} s_{f}$ to a final state such that $\max_i\{w',v,v_i,u\} = \lm\sigma$. Then there is a run $\rho:s \mathrm{\Rew{SpKAM\xspace}}^{*} s_{f}$, proving the first part of the statement (termination).
		
		For the space bound, note that 
		$$\sizes \ \ =\ \   \sizee + \size{c\cdotS} \ \ =\ \   \sizee + \sizec + \sizeS \ \ =\ \   \size{\esubxc\cdote} + \sizeS \ \ =\ \  \size{\state'}.$$
		and so the space bound follows from the \textit{i.h.}\xspace
	
	
		\item Case $\tomachhole{\subsym}$, i.e.\xspace $s=\spkamstatex
		{\esubx{(u,e)}}S$ and
		${\state'}=\spkamstateueS$. The type derivation $\pi$ typing  $s$ has the following shape:
		\[
		\infer[\textsc{T-st}]{\wtjudg{}{\max_i\{k+\sizeA,u,w',v_i\}}{\spkamstatex
				{\esubx{(u,e)}}S}{\star}}{
			\infer[\textsc{T-Var}]{\wtjudg{x:\mset{A}^k}{k+\size{A}}{x}{A}}{} 
			&
			\infer[\textsc{T-env}]{\wtjudg{}{\max\{u,w'\}}{\esubx{(u,e)}}{x:\msetA^k}} {
				\infer[\textsc{T-cl}]{
					\wtjudg{}{\max\{u,w'\}}{(u,e)}{\msetA^k}
				}{
					\wtjudg{\Gamma}{w'}{u}{\msetA^k }
					&
					\wtjudg{}{u}{e}{\Gamma} 
				} 
			}
			&
			\wtjudg{}{v_i}{S_i}{\mathcal{A}_i^{k_{i}}} 
		}
		\]
		with $w = \max_i\{k+\sizeA,u,w',v_i\}$. The target state ${\state'}$ can be typed by the following derivation $\tyd'$:
		\[\tyd':=
		\infer[\textsc{T-st}]{\wtjudg{}{\max_i\{w',u,v_i\}}{\spkamstateueS}{\star}}{
			\wtjudg{\Gamma}{w'}{u}{A } 
			&
			\wtjudg{}{u}{e}{\Gamma}
			&
			\wtjudg{}{v_i}{S_i}{\mathcal{A}_i^{k_{i}}} 
		}
		\]
		Since the $\textsc{T-Var}$ rule is removed, we have $\size\pi>\size\tyd'$, and so we can apply the \textit{i.h.}\xspace, obtaining a run $\sigma: {\state'} \mathrm{\Rew{SpKAM\xspace}}^{*} s_{f}$ to a final state such that $1+\max_i\{w',u,v_i\} = \lm\sigma$. Then there is a run $\rho:s \mathrm{\Rew{SpKAM\xspace}}^{*} s_{f}$, proving the first part of the statement (termination).
		
		For the space bound, note that $\sizes =  k+\sizeA$ by \reflemma{space-bound-on-current-state}, giving $w = \max_i\{\sizes,u,w',v_i\}$. 
		Now, there are two cases:
		\begin{itemize}
			\item $\lm\rho = \lm\sigma$: that is, $\sizes \leq \lm\sigma = \max_i\{w',u,v_i\}$. Then $\sizes \leq \max_i\{w',u,v_i\}$, and so $w = \max_i\{\sizes,u,w',v_i\} = \max_i\{w',u,v_i\} =_{\textit{i.h.}\xspace} \lm\sigma = \lm\rho$.
			
			\item $\lm\rho > \lm\sigma$: that is, $\sizes > \lm\sigma = \max_i\{w',u,v_i\}$. Then $\sizes > \max_i\{w',u,v_i\}$, and so $w = \max_i\{\sizes,u,w',v_i\} = \sizes = \lm\rho$.
		\end{itemize}
		
	\end{itemize}
\end{proof}
\section{Proofs of Section~\ref{sec:time}}\label{app:time}

\begin{lemma}\label{l:dry-env-clos-time}
	\hfill
	\begin{enumerate}
		\item\label{p:dry-env-clos-time-one} If $\pi\;\triangleright \wtjudg{}{w}{e}{\Gamma}$ and $\Gamma$ is dry, then $w = 0$.
		\item\label{p:dry-env-clos-time-two} If $\pi\;\triangleright \wtjudg{}{w}{c}{[\,]^k}$, then $w = 0$.
	\end{enumerate}
	
\end{lemma}

\begin{proof}
	By mutual induction on $e$ and $c$.
	\begin{enumerate}
		\item $\pi$ has the following form:
		\[
		\infer[\textsc{T-env}]{\wtjudg{}{\sum\set{w_x|x\in\dome}}{e}{\Gamma}}{\wtjudg{}{w_x}{e(x)}{\Gamma(x)}}\]
		with $w =\sum\set{w_x|x\in\dome}$. Two cases:
		\begin{enumerate}
			\item $e$ is empty, i.e.\xspace $e = \epsilon$: then $w = 0$ and $\Gamma$ is the empty type environment, for which $\size\Gamma = 0$. Therefore, we have $w = 0$, validating the statement.
			
			\item $e$ is not empty, i.e.\xspace $e \neq \epsilon$:
			Since $\Gamma$ is dry,  then $\wtjudg{}{w_x}{e(x)}{[\,]^{k_{x}}}$ for some $k_{x}$. By \textit{i.h.}\xspace (point 2), $w_x=0$ and thus $w =\sum\set{w_x|x\in\dome}=0$.
		\end{enumerate}
		\item   Let $e(x):=(t,e)$. Then $\pi$ has the following form: 
		
		\[
		\infer[\textsc{T-cl}]{\wtjudg{}{0+v}{(t,e)}{[\,]^{k_{x}}}}{
			\infer[\textsc{T-none}]{\wtjudg{\Delta}{0}{t}{[\,]^{k_{x}}}}{\Delta \text{ is dry}} && \wtjudg{}{v}{e}{\Delta}}
		\]
		
		By \textit{i.h.}\xspace (point 1) $v=0$. Thus $w=v=0$.
	\end{enumerate}
\end{proof}

\begin{lemma}[The weight of final states is their low-level time]
	Let $s$ be a final state and $\pi\;\triangleright \wtjudg{}{w}{s}{\star}$. Then $w = \sizes$.
\end{lemma}
\begin{proof}
	Final states have the shape $\spkamstate{\la\vart}e\epsilon$. Then $\pi$ has the following shape:
	\[
	\infer[\textsc{T-st}]{\wtjudg{}{v+\size\Gamma}{\spkamstate{\la\vart}e\epsilon}{\star}}{
		\infer[\textsc{T-}\lambda_\star]{\wtjudg{\Gamma}{\size\Gamma}{\lambdax.t}{\star}}{
			\dom\Gamma = \fv{\la\vart} & \Gamma\mbox{ is dry}}
		&
		\wtjudg{}{v}{e}{\Gamma}
	}
	\]
	with $w = v+\size\Gamma$. By \reflemmap{dry-env-clos-time}{one}, $v=0$. Then $w =_{\reflemmap{env-clos-size}{one}} \sizee =\sizes$.
\end{proof}

\begin{lemma}[Multi-set splitting]
	\label{l:multiset-splitting-time}
	\hfill
	\begin{enumerate}
		\item \emph{Terms}: let $\pi \;\triangleright \wtjudg{\Gamma}{w}{t}{\mathcal{A}^{k}\uplus\mathcal{B}^{k}}$ with $k= 1+\size\Gamma$. Then there exists two type derivations $\pi_{\mathcal{A}} \;\triangleright \wtjudg{\Gamma_{\mathcal{A}}}{w_{\mathcal{A}}}{t}{\mathcal{A}^{k}}$ and $\pi_{\mathcal{B}} \;\triangleright \wtjudg{\Gamma_{\mathcal{B}}}{w_{\mathcal{B}}}{t}{\mathcal{B}^{k}}$ such that $\Gamma_{\mathcal{A}} \# \Gamma_{\mathcal{B}}$, $\Gamma = \Gamma_{\mathcal{A}} \uplus \Gamma_{\mathcal{B}}$, $\size\pi = \size{\pi_{\mathcal{A}}} + \size{\pi_{\mathcal{B}}}$ and $w = w_{\mathcal{A}}+w_{\mathcal{B}}$.
		
		\item \emph{Closures}: let $\pi \;\triangleright \wtjudg{}{w}{c}{\mathcal{A}^{k}\uplus\mathcal{B}^{k}}$. Then there exists two type derivations $\pi_{\mathcal{A}} \;\triangleright \wtjudg{}{w_{\mathcal{A}}}{c}{\mathcal{A}^{k}}$ and $\pi_{\mathcal{B}} \;\triangleright \wtjudg{}{w_{\mathcal{B}}}{c}{\mathcal{B}^{k}}$ such that $\size\pi = \size{\pi_{\mathcal{A}}} + \size{\pi_{\mathcal{B}}}$ and $w = w_{\mathcal{A}}+w_{\mathcal{B}}$.
		
		\item \label{p:multiset-splitting-time-env}
		\emph{Environments}: let $\Gamma$ and $\Delta$ summable and $\pi \;\triangleright \wtjudg{}{w}{e}{\Gamma\uplus\Delta}$. Then there exists two type derivations $\pi_{\Gamma} \;\triangleright \wtjudg{}{w_{\Gamma}}{e|_{\dom\Gamma}}{\Gamma}$ and $\pi_{\Delta} \;\triangleright \wtjudg{}{w_{\Delta}}{e|_{\dom\Delta}}{\Delta}$ such that $\size\pi = \size{\pi_{\Gamma}} + \size{\pi_{\Delta}}$ and $w = w_{\Gamma}+w_{\Delta}$.
	\end{enumerate}
\end{lemma}
\begin{proof}
	The proof goes in the same way of the proof of \reflemma{multiset-splitting}.
\end{proof}

\begin{theorem}[Quantitative Time Soundness]
	Let $s$ be a Space KAM\xspace reachable state such that there is a derivation $\pi\;\triangleright\wtjudg{}{w}{s}{\star}$. Then the run $\rho:s\mathrm{\Rew{SpKAM\xspace}}^*s_{f}$ to the final state is such that
	$w=\lmt\rho$.	
\end{theorem}

\begin{proof}
	The proof is by induction on $\size\pi$ and case analysis on whether $s$ is final. If $s$ is final then the run $\rho$ in the statement is given by the empty run. Therefore, we have $\lmt\rho = \sizes$ and the required time bound becomes $w= \sizes$, which is given by \reflemma{weight-of-final-states-is-right-time}. If $s$ is not final then $s\mathrm{\Rew{SpKAM\xspace}}{\state'}$. By examining all the transition rules. We set $A:=\arr{\mathcal{A}_1^{k_{1}}}{\arr{\cdots}{\arr{\mathcal{A}_n^{k_{n}}}{\star}}}$ and $S:=S_1\cdotsS_n$.
	\begin{itemize}
		\item Case $\tomachhole{\seavsym}$, i.e.\xspace
		$s=\spkamstate{tx}{e}S$ and 
		${\state'}=\spkamstatet{ 
			e|_t}{e(x)\cdotS}$. The type derivation $\pi$ typing  $s$ has the following shape:
		\[
		\infer[\textsc{T-st}]{\wtjudg{}{w'+k+\size\Gamma+\sizeA+u+\sum_i v_i}{\spkamstate{tx}eS}{\star}}{
			\infer[\textsc{T-@}_{2}]{\wtjudg{\Gamma\uplusx:\mathcal{A}^k}{w'+k+\size\Gamma+\sizeA}{tx}{A} }{\wtjudg{\Gamma}{w'}{t}{\arr{\mathcal{A}^k}{A}}}
			&
			\pi_{e}\;\triangleright\wtjudg{}{u}{e}{\Gamma\uplusx:\mathcal{A}^k}
			&
			\wtjudg{}{v_i}{S_i}{\mathcal{A}_i^{k_{i}}} 
		}
		\]
		with $w = w'+k+\size\Gamma+\sizeA+u+\sum_i v_i$. By \reflemmap{multiset-splitting-time}{env}, there are two derivations $\pi_{\Gamma}\;\triangleright\wtjudg{}{u_{\Gamma}}{e|_{\dom\Gamma}}{\Gamma}$ and $\pi_{x:\mathcal{A}}\;\triangleright\wtjudg{}{u_{x:\mathcal{A}}}{e(x)}{x:\mathcal{A}}$ such that $\size{\pi_{e}} = \size{\pi_{\Gamma}} + \size{\pi_{x:\mathcal{A}}}$ and $u = u_{\Gamma}+ u_{x:\mathcal{A}}$. By the environment domain invariant (\reflemma{spkam-invariants}), $\dom\Gamma = \fvt$. Moreover, $\pi_{x:\mathcal{A}}$ is necessarily the conclusion of a unary $\textsc{T-env}$ rule of premise $\pi_{\mathcal{A}}\;\triangleright\wtjudg{}{u_{\mathcal{A}}}{e(x)}{\mathcal{A}}$ for which $\size{\pi_{\mathcal{A}}} = \size{\pi_{x:\mathcal{A}}}$ and $u_{\mathcal{A}} = u_{x:\mathcal{A}}$.
		Then, ${\state'}$ can be typed by the following derivation $\tyd'$:
		\[\tyd' := 
		\infer[\textsc{T-st}]{\wtjudg{}{w'+u_{\Gamma}+u_{\mathcal{A}}+\sum_i v_i}{\spkamstatet{ 
					e|_t}{e(x)\cdotS}}{\star}}{
			\wtjudg{\Gamma'}{w'}{t}{\arr{\mathcal{A}^k}{A}}
			&
			\pi_{\Gamma}\;\triangleright \wtjudg{}{u_{\Gamma}}{e|_t}{\Gamma}
			&
			\pi_{\mathcal{A}}\;\triangleright \wtjudg{}{u_{\mathcal{A}}}{e(x)}{\mathcal{A}^k}
			&
			\wtjudg{}{v_i}{S_i}{\mathcal{A}_i^{k_{i}}} 
		}
		\]
		Since $\size{\pi_{e}} = \size{\pi_{\Gamma}} + \size{\pi_{x:\mathcal{A}}} = \size{\pi_{\Gamma}} + \size{\pi_{\mathcal{A}}}$, we have $\size\pi > \size\tyd'$ (beccause the $\textsc{T-@}_{2}$ rule is removed), and so we can apply the \textit{i.h.}\xspace, obtaining a run $\sigma: {\state'} \mathrm{\Rew{SpKAM\xspace}}^{*} s_{f}$ to a final state such that $w'+u_{\Gamma}+u_{\mathcal{A}}+\sum_i v_i = \lmt\sigma$.
		
		For the time bound, note that, since $u = u_{\Gamma}+ u_{x:\mathcal{A}} = u_{\Gamma}+ u_{\mathcal{A}}$, we have $w = w'+k+\size\Gamma+\sizeA+u_{\Gamma}+ u_{\mathcal{A}}+\sum_i v_i=\sizes+w'+u_{\Gamma}+ u_{\mathcal{A}}+\sum_i v_i$. Then $\lmt\rho = \sizes+\lmt\sigma = w'+u_{\Gamma}+u_{\mathcal{A}}+\sum v_i+k+\size\Gamma+\sizeA = w$.
	
	
		\item Case $\tomachhole{\seanvsym}$, i.e.\xspace $s=\spkamstate{tu}{e}S$ 
		and 
		${\state'}=\spkamstatet{ 
			e|_t}{(u,e|_u)\cdotS}$. 
		
		
		The type derivation $\pi$ typing  $s$ has the following shape:
		\[
		\infer[\textsc{T-st}]{\wtjudg{}{w_1+w_2+\size{\Gamma\uplus\Delta}+\sizeA +\sum_i v_i+u}{\spkamstate{tu}eS}{\star}}{
			\infer[\textsc{T-@}_{1}]{\wtjudg{\Gamma\uplus\Delta}{w_1+w_2+\size{\Gamma\uplus\Delta}+\sizeA}{tu}{A } }{\wtjudg{\Gamma}{w_1}{t}{\arr{\mathcal{A}^{k}}{A}}
				& 
				\wtjudg{\Delta}{w_2}{u}{\mathcal{A}^{k}}& \Gamma\# \Delta}
			&
			\wtjudg{}{u}{e}{\Gamma\uplus\Delta}
			&
			\wtjudg{}{v_i}{S_i}{\mathcal{A}_i^{k_{i}}} 
		}
		\]
		with $w = w_1+w_2+\size{\Gamma\uplus\Delta}+\sizeA +\sum_i v_i+u$. By \reflemmap{multiset-splitting-time}{env}, there are two derivations $\pi_{\Gamma}\;\triangleright\wtjudg{}{u_{\Gamma}}{e|_{\dom\Gamma}}{\Gamma}$ and $\pi_{\Delta}\;\triangleright\wtjudg{}{u_{\Delta}}{e|_{\dom\Delta}}{\Delta}$ such that $\size{\pi_{e}} = \size{\pi_{\Gamma}} + \size{\pi_{\Delta}}$ and $u = u_{\Gamma}+ u_{\Delta}$. By the environment domain invarian (\reflemma{spkam-invariants}), $\dom\Gamma = \fvt$ and $\dom\Delta = \fvu$.		Then, ${\state'}$ can be typed by the following derivation $\tyd'$:
		\[\tyd' := 
		\infer[\textsc{T-st}]{\wtjudg{}{
				w_{1}+w_{2}+\sum_i v_i+u_{\Gamma}+u_{\Delta}}{\spkamstatet{ 
					e|_t}{(u,e|_u)\cdotS}}{\star}}{
			\wtjudg{\Gamma}{w_1}{t}{\arr{\mathcal{A}^{k}}{A}}
			&
			\wtjudg{}{u_{\Gamma}}{e|_t}{\Gamma}
			&
			\infer[\textsc{T-cl}]{\wtjudg{}{w_{2}+u_{\Delta}
				}{(u,e|_u)}{\mathcal{A}^k}}{\wtjudg{\Delta}{w_2}{u}{\mathcal{A}^{k}}&&
				\wtjudg{}{u_{\Delta}}{e|_u}{\Delta}}
			&
			\wtjudg{}{v_i}{S_i}{\mathcal{A}_i^{k_{i}}} 
		}
		\]
		Since $\size{\pi_{e}} = \size{\pi_{\Gamma}} + \size{\pi_{\Delta}}$, we have $\size\pi > \size\tyd'$ (beccause the $\textsc{T-@}_{2}$ rule is removed and rule $\textsc{T-cl}$ does not count for the size), and so we can apply the \textit{i.h.}\xspace, obtaining a run $\sigma: {\state'} \mathrm{\Rew{SpKAM\xspace}}^{*} s_{f}$ to a final state such that $w_{1}+w_{2}+\sum_i v_i+u_{\Gamma}+u_{\Delta} = \lmt\sigma$.
		
		For the time bound, note that, since $u = u_{\Gamma}+ u_{\Delta}$, we have $w_{1}+w_{2}+\size{\Gamma\uplus\Delta}+\sizeA+\sum_i v_i+u_{\Gamma}+u_{\Delta} = w_{1}+w_{2}+\size{\Gamma\uplus\Delta}+\sizeA+\sum_i v_i+u = w$. Then $\lmt\rho = \lmt\sigma + \sizes = w$.
	
	
		\item Case $\tomachhole{\bwsym}$, i.e.\xspace $s=\spkamstate{\la\vart}{e}{c\cdotS}$ 
		and 
		${\state'}=\spkamstatet{ 
			e}{S}$. The type derivation $\pi$ typing  $s$ has the following shape:
		\[
		\infer[\textsc{T-st}]{\wtjudg{}{w'+\size\Gamma+\sizeA+k+u+v +\sum_i v_i}{\spkamstate{\la\vart}e{c\cdotS}}{\star}}{
			\infer[\textsc{T-}\lambda_{2}]{\wtjudg{\Gamma}{w'+\size\Gamma+\sizeA+k}{\lambdax.t}{\arr{\mset{\,}^{k}}{A}}}
			{\wtjudg{\Gamma}{w'}{t}{A} & x\notin\dom\Gamma}
			&
			\wtjudg{}{u}{e}{\Gamma}
			&
			\wtjudg{}{v}{c}{\mset{\,}^k}
			&
			\wtjudg{}{v_i}{S_i}{\mathcal{A}_i^{k_{i}}} 
		}\]
		with $w = w'+\size\Gamma+\sizeA+k+u+v +\sum_i v_i$. The target state ${\state'}$ can be typed by the following derivation $\tyd'$:
		\[\tyd' :=
		\infer[\textsc{T-st}]{\wtjudg{}{w'+u+\sum_i v_i}{\spkamstateteS}{\star}}{
			\wtjudg{\Gamma}{w'}{t}{A} & x\notin\dom\Gamma
			&
			\wtjudg{}{u}{e}{\Gamma}
			&
			\wtjudg{}{v_i}{S_i}{\mathcal{A}_i^{k_{i}}} 
		}\]
		Since the $\textsc{T-}\lambda_{2}$ rule is removed, we have $\size\pi>\size\tyd'$, and so we can apply the \textit{i.h.}\xspace, obtaining a run $\sigma: {\state'} \mathrm{\Rew{SpKAM\xspace}}^{*} s_{f}$ to a final state such that $w'+u+\sum_i v_i = \lmt\sigma$.
		
		For the time bound, since $v=0$ by \reflemmap{dry-env-clos-time}{two}, we have that $\lmt\rho = \sizes+\lmt\sigma=w$.
		
	
	
		\item Case $\tomachhole{\bnwsym}$, i.e.\xspace $s=\spkamstate{\la\vart}{e}{c\cdotS}$ 
		and 
		${\state'}=\spkamstatet{ 
			\esub{x}{c}\cdote}{S}$. The type derivation $\pi$ typing  $s$ has the following shape:
		\[
		\infer[\textsc{T-st}]{\wtjudg{}{\size\Gamma+\sizeA+k+w'+v +\sum_i v_i +u}{\spkamstate{\la\vart}e{c\cdotS}}{\star}}{
			\infer[\textsc{T-}\lambda_{1}]{\wtjudg{\Gamma}{w'+\size\Gamma+\sizeA+k}{\lambdax.t}{\arr{\mathcal{A}^{k}}{A}}} 
			{\wtjudg{\Gamma,x:\mathcal{A}^{k}}{w'}{t}{A}}
			&
			\wtjudg{}{u}{e}{\Gamma}
			&
			\wtjudg{}{v}{c}{\mathcal{A}^k}
			&
			\wtjudg{}{v_i}{S_i}{\mathcal{A}_i^{k_{i}}} 
		}\]
		with $w = \size\Gamma+\sizeA+k+w'+v +\sum_i v_i +u$. The target state ${\state'}$ can be typed by the following derivation $\tyd'$:
		\[\tyd':=
		\infer[\textsc{T-st}]{\wtjudg{}{w'+v+\sum_i v_i+u} {\spkamstatet{\esubxc\cdote}S}{\star}}{
			\wtjudg{\Gamma,x:\mathcal{A}^{k}}{w'}{t}{A}
			&
			\infer[\textsc{T-env}]{\wtjudg{}{u+v}{\esubxc\cdote}{\Gamma,x:\mathcal{A}^{k}}} {\wtjudg{}{u}{e}{\Gamma}&\wtjudg{}{v}{c}{\mathcal{A}^k}}
			&
			\wtjudg{}{v_i}{S_i}{\mathcal{A}_i^{k_{i}}} 
		}\]
		Since the $\textsc{T-}\lambda_{1}$ rule is removed and the $\textsc{T-env}$ rule does not count for the size of type derivations, we have $\size\pi>\size\tyd'$, and so we can apply the \textit{i.h.}\xspace, obtaining a run $\sigma: {\state'} \mathrm{\Rew{SpKAM\xspace}}^{*} s_{f}$ to a final state such that $w'+v+\sum_i v_i+u = \lmt\sigma$.
		
		For the time bound, note that 
		$\lmt\rho = \sizes+\lmt\sigma=w$.
	
	
		\item Case $\tomachhole{\subsym}$, i.e.\xspace $s=\spkamstatex
		{\esubx{(u,e)}}S$ and
		${\state'}=\spkamstateueS$. The type derivation $\pi$ typing  $s$ has the following shape:
		\[
		\infer[\textsc{T-st}]{\wtjudg{}{k+\sizeA+u+w'+\sum_i v_i}{\spkamstatex
				{\esubx{(u,e)}}S}{\star}}{
			\infer[\textsc{T-Var}]{\wtjudg{x:\mset{A}^k}{k+\size{A}}{x}{A}}{} 
			&
			\infer[\textsc{T-env}]{\wtjudg{}{u+w'}{\esubx{(u,e)}}{x:\msetA^k}} {
				\infer[\textsc{T-cl}]{
					\wtjudg{}{u+w'}{(u,e)}{\msetA^k}
				}{
					\wtjudg{\Gamma}{w'}{u}{\msetA^k }
					&
					\wtjudg{}{u}{e}{\Gamma} 
				} 
			}
			&
			\wtjudg{}{v_i}{S_i}{\mathcal{A}_i^{k_{i}}} 
		}
		\]
		with $w = k+\sizeA+u+w'+\sum_i v_i$. The target state ${\state'}$ can be typed by the following derivation $\tyd'$:
		\[\tyd':=
		\infer[\textsc{T-st}]{\wtjudg{}{w'+u+\sum_i v_i}{\spkamstateueS}{\star}}{
			\wtjudg{\Gamma}{w'}{u}{A } 
			&
			\wtjudg{}{u}{e}{\Gamma}
			&
			\wtjudg{}{v_i}{S_i}{\mathcal{A}_i^{k_{i}}} 
		}
		\]
		Since the $\textsc{T-Var}$ rule is removed, we have $\size\pi>\size\tyd'$, and so we can apply the \textit{i.h.}\xspace, obtaining a run $\sigma: {\state'} \mathrm{\Rew{SpKAM\xspace}}^{*} s_{f}$ to a final state such that $w'+u+\sum_i v_i = \lmt\sigma$.
		
		For the time bound, note that $\lmt\rho = \sizes+\lmt\sigma=w$.
		
	\end{itemize}
\end{proof}
\section{Weights Capture the Space of the Space KAM\xspace}\label{sec:correctness}
This section is devoted to the proof of our main result, that is, the fact that the wieght of a type judgment (assigning type $\star$ to a closed term $t$) captures the space used by the (complete run on $t$ of the) Space KAM\xspace. The proof is carried out in a rather standard way. First, we prove soundness, that is the fact that typable terms terminate, and moreover that their evaluation respects the weight. Second, we prove completeness, that is the fact that all terminating terms are typable. 
\subsection{Preliminary Properties}
The first property that we prove here is qualitative, that is, it does not concern weights or indices\footnote{When a definition or a statement does not rest on weights, we do not report them, for the sake of readability.}. It is simply the already mentioned fact that the domain of type contexts is exactly the set of free variables of the typed term. This is the type analog of the environment domain invariant of the Space KAM\xspace.
\begin{lemma}[Type contexts domain invariant]
	\label{l:tye-invariant}
	\hfill
	\begin{enumerate}
		\item If $\pi\;\triangleright \tjudg{\Gamma}{t}{A}$ then $\dom\Gamma = \fvt$.
		\item If $\pi\;\triangleright \tjudg{\Gamma}{t}{\mathcal{A}}$ then $\dom\Gamma = \fvt$.
	\end{enumerate}
\end{lemma}

\begin{proof}
	By induction on $\pi$.
\end{proof}

Then, we have two quantitative properties.
Before stating them, we need to introduce the definition of typed Space KAM\xspace states. The idea is very simple, and it is due to de Carvalho~\cite{deCarvalho18}. In order to state quantitative properties that involve abstract machines, we type the execution of the abstract machine itself. We have already mentioned that type environments correspond to the Space KAM\xspace environments, and that closure types correspond to Space KAM\xspace closures. In \reffig{kamtypes}, the connection is made formal.

\begin{figure}[t]
	\[
	\begin{array}{c@{\hspace{1cm}}c@{\hspace{1cm}}c}
	\infer[\textsc{T-env}]{\wtjudg{}{\max\set{w_x|x\in\dome}}{e}{\Gamma}} 
	{\wtjudg{}{w_x}{e(x)}{\Gamma(x)}&&\forallx\in\dome}
	&
	\infer[\textsc{T-cl}]{\wtjudg{}{\max\{w,v\}}{(t,e)}{\mathcal{A}^{k}}}{ 
		\wtjudg{}{w}{e}{\Gamma} 
		&& 
		\wtjudg{\Gamma}{v}{t}{\mathcal{A}^{k}} }
	\\\\
	\multicolumn{2}{c}{
		\infer[\textsc{T-st}]{\wtjudg{}{\max_i\{w,v_i,u\}}{\spkamstatete{c_1\cdotsc_n}}{\star}}{
			\wtjudg{\Gamma}{w}{t}{\arr{\mathcal{A}_1^{k_{1}}}{\arr{\cdots}{\arr{\mathcal{A}_n^{k_{n}}}{\star} } } } 
			&
			\wtjudg{}{u}{e}{\Gamma}
			&
			\wtjudg{}{v_i}{c_i}{\mathcal{A}_i^{k_{i}}} 
		}
	}
	\end{array}
	\]
	
	\caption{Typing rules for the machine components of the Space KAM\xspace.}
	\label{fig:kamtypes}
\end{figure}

The next lemma states that the size of a closure is equal to the size of its type, for every closure, and similarly for environments.
\begin{lemma}[Types capture the size of closures and environments]
	\label{l:env-clos-size}
	\hfill
	\begin{enumerate}
		\item \label{p:env-clos-size-one} 
		If $\pi\;\triangleright \tjudg{}{e}{\Gamma}$ then $\sizee = \size\Gamma$.
		\item \label{p:env-clos-size-two} 
		If $\pi\;\triangleright \tjudg{}{c}{\mathcal{A}^{k}}$ then $\sizec = k$.
	\end{enumerate}
\end{lemma}

The lemma expresses one of the key properties of the type system, which has an almost \emph{magical} feeling. At first sight, indeed, the indices on multi types are completely arbitrary, as the typing rules do not seem to impose strong constraint. Surprisingly, instead, when one builds the type derivation of a closure, then the indices are uniquely determined, and they capture \emph{exactly} the size of the closure.

\begin{proof}
	By mutual induction on $e$ and $c$.
	\begin{enumerate}
		\item $\pi$ has the following form:
		\[
		\infer[\textsc{T-env}]{\tjudg{}{e}{\Gamma}}{\tjudg{}{e(x)}{\Gamma(x)}}\] Let $\Gamma(x) = \mathcal{A}_{x}^{k_{x}}$. By \textit{i.h.}\xspace (point 2), $\size{e(x)} = k_{x}$. 
		Then $\sizee = \sum_{x\in\dome}\size{e(x)} =_{\textit{i.h.}\xspace}  \sum_{x\in\dome}k_{x} = \size\Gamma$.
		
		\item $\pi$ has the following form:
		\[\infer[\textsc{T-cl}]{\tjudg{}{(t,e)}{\mathcal{A}^{k}}}{ 
			\tjudg{}{e}{\Gamma} 
			&& 
			\tjudg{\Gamma}{t}{\mathcal{A}^{k}} }\]
		with $c = (t,e)$. By \textit{i.h.}\xspace (point 1) applied to $e$, we have $\sizee = \size\Gamma$. Since the typing of $t$ comes necessarily from a rule $\textsc{T-none}$ or $\textsc{T-many}$, we have $k = 1+ \size\Gamma$. Then $\sizec = 1 +\sizee =_{\textit{i.h.}\xspace} 1+ \size\Gamma = k$.
	\end{enumerate}
\end{proof}

The second easy property is the fact that the size of a state is given by the size 
of the types in the judgment for its code, which give the size of the stack and 
the environment.

\begin{lemma}[Judgments capture the size of the corresponding state]
	\label{l:space-bound-on-current-state}
	If \[
	\infer[\textsc{T-st}]{\tjudg{}{(t,c_1\cdotsc_n,e)}{\star}}{
		\tjudg{\Gamma}{t}{\arr{\mathcal{A}_1^{k_{1}}}{\arr{\cdots}{\arr{\mathcal{A}_n^{k_{n}}}{\star} } } } 
		&
		\tjudg{}{c_i}{\mathcal{A}_i^{k_{i}}} 
		&
		\tjudg{}{e}{\Gamma}
	}
	\]
	then $\size\Gamma + \sum_{i=1}^{n} k_{i} = \sizes$.	
\end{lemma}

\begin{proof}
	We have:
	\[
	\infer[\textsc{T-st}]{\tjudg{}{(t,c_1\cdotsc_n,e)}{\star}}{
		\tjudg{\Gamma}{t}{\arr{\mathcal{A}_1^{k_{1}}}{\arr{\cdots}{\arr{\mathcal{A}_n^{k_{n}}}{\star} } } } 
		&
		\tjudg{}{c_i}{\mathcal{A}_i^{k_{i}}} 
		&
		\tjudg{}{e}{\Gamma}
	}
	\]
	By definition, $\sizes = \sizee + \size{c_1\cdotsc_n} =  \sizee +\sum_{i=1}^{n}\size{c_i}$ . By \reflemma{env-clos-size}, $\sizee = \size\Gamma$ and $\size{c_{i}} = k_{i}$ for $1\leq i\leq n$. Then $\sizes = \size\Gamma + \sum_{i=1}^{n} k_{i}$.
\end{proof}

\subsection{Soundness}
Soundness is the fact that on typed states the Space KAM\xspace terminates. Here it is refined with our space analysis, showing that the weight of the type judgment is exactly the maximum space used by the run of the Space KAM\xspace.

The proof technique is mostly standard. It is based on a subject reduction property plus a space analysis of final states. What is slightly unusual is that  subject reduction is not stated as an independent property, it is instead plugged into the proof of soundness. This is needed to prove the space bound.

\paragraph{Space Analysis of Final States.} To prove that the weight system 
correctly measures the size of final states, we need an auxiliary lemma ensuring 
that closures and environments typed with empty types and dry type contexts induce 
null weight on their judgment.

\begin{lemma}[Empty types and dry type environments induce null weight]
	\label{l:dry-env-clos}
	\hfill
	\begin{enumerate}
		\item \label{p:dry-env-clos-one} 
		If $\pi\;\triangleright \wtjudg{}{w}{e}{\Gamma}$ and $\Gamma$ is dry, then $w = 0$.
		\item \label{p:dry-env-clos-two} 
		If $\pi\;\triangleright \wtjudg{}{w}{c}{[\,]^{k}}$, then $w = 0$.
	\end{enumerate}
\end{lemma}

\begin{proof}
	By mutual induction on $e$ and $c$.
	\begin{enumerate}
		\item $\pi$ has the following form:
		\[
		\infer[\textsc{T-env}]{\wtjudg{}{\max\set{w_x|x\in\dome}}{e}{\Gamma}}{\wtjudg{}{w_x}{e(x)}{\Gamma(x)}}\]
		with $w =\max\set{w_x|x\in\dome}$. Two cases:
		\begin{enumerate}
			\item $e$ is empty, i.e.\xspace $e = \epsilon$: then $w = 0$ and $\Gamma$ is the empty type environment, for which $\size\Gamma = 0$. Therefore, we have $w = 0 =\size\Gamma$, validating the statement.
			
			\item $e$ is not empty, i.e.\xspace $e \neq \epsilon$:
			Since $\Gamma$ is dry,  then $\wtjudg{}{w_x}{e(x)}{[\,]^{k_{x}}}$ for some $k_{x}$. By \textit{i.h.}\xspace (point 2), $w_{x}  = 0$. Then $w =\max\set{w_x|x\in\dome} =0$.
		\end{enumerate}
		\item $\pi$ has the following form:
		\[\infer[\textsc{T-cl}]{\wtjudg{}{\max\set{v,u}}{(t,e)}{[\,]^{k}}}{ 
			\wtjudg{}{v}{e}{\Gamma} 
			&& 
			\wtjudg{\Gamma}{u}{t}{[\,]^{k}} }\]
		with $c = (t,e)$ and $w = \max\set{v,u}$. Since the typing of $t$ comes necessarily from a rule $\textsc{T-none}$, $\Gamma$ is dry, $u = 0$. Then we can apply the \textit{i.h.}\xspace (point 1) to $e$, obtaining $v = 0$. Thus we have $w = 0$.
	\end{enumerate}
\end{proof}


\begin{proposition}[The weight of final states is their space]
	\label{prop:weight-of-final-states-is-right}
	Let $s$ be a final state and $\pi\;\triangleright \tjudgw{}{w}{s}{\star}$. Then $w = \sizes$.
\end{proposition}
\begin{proof}
	Final states have the shape $\spkamstate{\la\vart}e\epsilon$. Then $\pi$ has the following shape:
	\[
	\infer[\textsc{T-st}]{\wtjudg{}{\max\{v,\size\Gamma\}}{\spkamstate{\la\vart}e\epsilon}{\star}}{
		\infer[\textsc{T-}\lambda_\star]{\wtjudg{\Gamma}{\size{\Gamma}}{\lambdax.t}{\star}}{
			\dom\Gamma = \fv{\la\vart} & \Gamma\mbox{ is dry}}
		&
		\wtjudg{}{v}{e}{\Gamma}
	}
	\]
	with $w = \max\{v,\size\Gamma\}$. By \reflemmap{dry-env-clos}{one}, $v = 0$. Therefore, $w = \size\Gamma$ and so $w =  \sizee = \sizes$.
\end{proof}


\paragraph{Soundness.} Soundness shall be proved by induction on the size of type derivation, which is defined ignoring some typing rules, as follows.
\begin{definition}[Type derivations size]
	The size $\size\pi$ of a type derivation $\pi$ is its number of rules without counting rules $\textsc{T-many}$, $\textsc{T-none}$, $\textsc{T-cl}$, and $\textsc{T-env}$.
\end{definition}

The subject reduction argument shall need the following auxiliary lemma.

\begin{lemma}[Multi-set splitting]
	\label{l:multiset-splitting}
	\hfill
	\begin{enumerate}
		\item \emph{Terms}: let $\pi \;\triangleright \wtjudg{\Gamma}{w}{t}{\mathcal{A}^{k}\uplus\mathcal{B}^{k}}$ with $k= 1+\size\Gamma$. Then there exists two type derivations $\pi_{\mathcal{A}} \;\triangleright \wtjudg{\Gamma_{\mathcal{A}}}{w_{\mathcal{A}}}{t}{\mathcal{A}^{k}}$ and $\pi_{\mathcal{B}} \;\triangleright \wtjudg{\Gamma_{\mathcal{B}}}{w_{\mathcal{B}}}{t}{\mathcal{B}^{k}}$ such that $\Gamma_{\mathcal{A}} \# \Gamma_{\mathcal{B}}$, $\Gamma = \Gamma_{\mathcal{A}} \uplus \Gamma_{\mathcal{B}}$, $\size\pi = \size{\pi_{\mathcal{A}}} + \size{\pi_{\mathcal{B}}}$ and $w = \max\set{w_{\mathcal{A}},w_{\mathcal{B}}}$.
		
		\item \emph{Closures}: let $\pi \;\triangleright \wtjudg{}{w}{c}{\mathcal{A}^{k}\uplus\mathcal{B}^{k}}$. Then there exists two type derivations $\pi_{\mathcal{A}} \;\triangleright \wtjudg{}{w_{\mathcal{A}}}{c}{\mathcal{A}^{k}}$ and $\pi_{\mathcal{B}} \;\triangleright \wtjudg{}{w_{\mathcal{B}}}{c}{\mathcal{B}^{k}}$ such that $\size\pi = \size{\pi_{\mathcal{A}}} + \size{\pi_{\mathcal{B}}}$ and $w = \max\set{w_{\mathcal{A}},w_{\mathcal{B}}}$.
		
		\item \label{p:multiset-splitting-env}
		\emph{Environments}: let $\Gamma$ and $\Delta$ summable and $\pi \;\triangleright \wtjudg{}{w}{e}{\Gamma\uplus\Delta}$. Then there exists two type derivations $\pi_{\Gamma} \;\triangleright \wtjudg{}{w_{\Gamma}}{e|_{\dom\Gamma}}{\Gamma}$ and $\pi_{\Delta} \;\triangleright \wtjudg{}{w_{\Delta}}{e|_{\dom\Delta}}{\Delta}$ such that $\size\pi = \size{\pi_{\Gamma}} + \size{\pi_{\Delta}}$ and $w = \max\set{w_{\Gamma},w_{\Delta}}$.
	\end{enumerate}
\end{lemma}

\begin{proof}
	\hfill
	\begin{enumerate}
		\item Suppose that $\mathcal{A}^{k} = [\,]^{k}$. Then $\mathcal{A}^{k}\uplus\mathcal{B}^{k} = \mathcal{B}^{k}$. Now, let $\Gamma_{\mathcal{A}}$ be defined as the unique dry type context such that $\dom{\Gamma_{\mathcal{A}}} = \dom\Gamma$ and it is summable with $\Gamma$---note that necessarily $\size\Gamma = \size{\Gamma_{\mathcal{A}}}$. By \reflemma{tye-invariant}, $\dom\Gamma = \fvt$, and so we obtain the following derivation:
		\[\infer[\textsc{T-none}]{\wtjudg{\Gamma_{\mathcal{A}}}{0}{t}{[\,]^{1+\size{\Gamma_{\mathcal{A}}}}}}{}\]
		which is the $\pi_{\mathcal{A}}$ of the statement. We also take $\pi_{\mathcal{B}} := \pi$, and the statement holds. 
		
		If $\mathcal{B}^{k} = [\,]^{k}$ the proof is as in the previous case.
		
		Assume now that both $\mathcal{A}^{k}$ and $\mathcal{B}^{k}$ are non-empty, say $\mathcal{A}^{k}= \mset{A_{1},\ldots,A_{m}}^{k}$ and $\mathcal{B}^{k}= \mset{A_{m+1},\ldots,A_{n}}^{k}$. Then $\pi$ has the following shape:
		\[\infer[\textsc{T-many}]{\wtjudg{\uplus_{i=1}^n\Gamma_i}{\max_{i}\set{v_{i}}}{t}{\mset{A_1,\mydots,A_n}^{1+\size{\uplus_{i=1}^n\Gamma_i}}}}
		{\wtjudg{\Gamma_i}{v_{i}}{t}{A_i} & 1\leq i\leq n & \#_i\Gamma_{i}}\]
		and the two derivations $\pi_{\mathcal{A}}$ and $\pi_{\mathcal{B}}$ are obtained as follows
		\[\pi_{\mathcal{A}}:=\ \ \ \infer[\textsc{T-many}]{\wtjudg{\uplus_{i=1}^m\Gamma_i}{\max_{i}\set{v_{i}}}{t}{\mset{A_1,\mydots,A_m}^{1+\size{\uplus_{i=1}^m\Gamma_i}}}}
		{\wtjudg{\Gamma_i}{v_{i}}{t}{A_i} & 1\leq i\leq m & \#_i\Gamma_{i}}\]
		and
		\[\pi_{\mathcal{B}}:=\ \ \ \infer[\textsc{T-many}]{\wtjudg{\uplus_{i=m+1}^n\Gamma_i}{\max_{i}\set{v_{i}}}{t}{\mset{A_{m+1},\mydots,A_n}^{1+\size{\uplus_{i=m+1}^n\Gamma_i}}}}
		{\wtjudg{\Gamma_i}{v_{i}}{t}{A_i} & m+1\leq i\leq n & \#_i\Gamma_{i}}\]
		which clearly satisfy the statement.
		\item If $c = (t,e)$ then $\pi$ has the following form 
		\[\infer[\textsc{T-cl}]{\wtjudg{}{\max\{w,v\}}{(t,e)}{\mathcal{A}^{k}}}{ 
			\wtjudg{}{w}{e}{\Gamma} 
			&& 
			\wtjudg{\Gamma}{v}{t}{\mathcal{A}^{k}} }\]
		Then the \textit{i.h.}\xspace (point 1) applied to the right premise gives two derivations for $t$ with respect to $\mathcal{A}^{k}$ and $\mathcal{B}^{k}$. In particular it gives two summable type contexts $\Gamma_{\mathcal{A}}$ and $\Gamma_{\mathcal{B}}$ with which one applies the \textit{i.h.}\xspace (point 3) to the left premise, obtaining two derivations for $e$ with respect to $\Gamma_{\mathcal{A}}$ and $\Gamma_{\mathcal{B}}$. Pairing the respective derivations for $t$ and $e$ one obtains the statement.
		
		\item If $e$ is empty then both $\Gamma$ and $\Delta$ are empty and the statement trivially holds. Otherwise, it follows from applying the \textit{i.h.}\xspace (point 2) for each variable in $\dom\Gamma \cap \dom\Delta$.
	\end{enumerate}
\end{proof}

\begin{theorem}[Soundness]
	Let $s$ be a Space KAM\xspace reachable state such that there is a derivation $\pi\;\triangleright\tjudgw{}{w}{s}{\star}$. Then 
	\begin{enumerate}
		\item \emph{Termination}: there is a run $\rho:s\mathrm{\Rew{SpKAM\xspace}}^*s_{f}$ to a final state. Moreover,
		\item \emph{Space bound}: $w=\lm\rho$.	
	\end{enumerate}
\end{theorem}

\begin{proof}
	The proof is by induction on $\size\pi$ and case analysis on whether $s$ is final. If $s$ is final then the run $\rho$ in the statement is given by the empty run. Therefore, we have $\lm\rho = \sizes$ and the required space bound becomes $w= \sizes$, which is given by \refprop{weight-of-final-states-is-right}. If $s$ is not final then $s\mathrm{\Rew{SpKAM\xspace}}{\state'}$. By examining all the transition rules. We set $A:=\arr{\mathcal{A}_1^{k_{1}}}{\arr{\cdots}{\arr{\mathcal{A}_n^{k_{n}}}{\star}}}$ and $S:=S_1\cdotsS_n$. We report just one case that illustrates the methodology. The other ones can be found in Appendix~\ref{app:correctness}.
	
	Case $\tomachhole{\seavsym}$, i.e.\xspace
		$s=\spkamstate{tx}{e}S$ and 
		${\state'}=\spkamstatet{ 
			e|_t}{e(x)\cdotS}$. The type derivation $\pi$ typing  $s$ has the following shape:
		\[
		\infer[\textsc{T-st}]{\wtjudg{}{\max_i\{w',u,v_i\}}{\spkamstate{tx}eS}{\star}}{
			\infer[\textsc{T-@}_{2}]{\wtjudg{\Gamma\uplusx:\mathcal{A}}{w'}{tx}{A} }{\wtjudg{\Gamma}{w'}{t}{\arr{\mathcal{A}}{A}}}
			&
			\pi_{e}\;\triangleright\wtjudg{}{u}{e}{\Gamma\uplusx:\mathcal{A}}
			&
			\wtjudg{}{v_i}{S_i}{\mathcal{A}_i^{k_{i}}} 
		}
		\]
		with $w = \max_i\{w',v_i,u\}$. By \reflemma{multiset-splitting}, there are two derivations $\pi_{\Gamma}\;\triangleright\wtjudg{}{u_{\Gamma}}{e|_{\dom\Gamma}}{\Gamma}$ and $\pi_{x:\mathcal{A}}\;\triangleright\wtjudg{}{u_{x:\mathcal{A}}}{e(x)}{x:\mathcal{A}}$ such that $\size{\pi_{e}} = \size{\pi_{\Gamma}} + \size{\pi_{x:\mathcal{A}}}$ and $u = \max\set{u_{\Gamma}, u_{x:\mathcal{A}}}$. By the environment domain invariant (\reflemma{spkam-invariants}), $\dom\Gamma = \fvt$. Moreover, $\pi_{x:\mathcal{A}}$ is necessarily the conclusion of a unary $\textsc{T-env}$ rule of premise $\pi_{\mathcal{A}}\;\triangleright\wtjudg{}{u_{\mathcal{A}}}{e(x)}{\mathcal{A}}$ for which $\size{\pi_{\mathcal{A}}} = \size{\pi_{x:\mathcal{A}}}$ and $u_{\mathcal{A}} = u_{x:\mathcal{A}}$.
		Then, ${\state'}$ can be typed by the following derivation $\tyd'$:
		\[\tyd' := 
		\infer[\textsc{T-st}]{\wtjudg{}{\max_i\{w',u_{\Gamma},u_{\mathcal{A}},v_i\}}{\spkamstatet{ 
					e|_t}{e(x)\cdotS}}{\star}}{
			\wtjudg{\Gamma'}{w'}{t}{\arr{\mathcal{A}}{A}}
			&
			\pi_{\Gamma}\;\triangleright \wtjudg{}{u_{\Gamma}}{e|_t}{\Gamma}
			&
			\pi_{\mathcal{A}}\;\triangleright \wtjudg{}{u_{\mathcal{A}}}{e(x)}{\mathcal{A}}
			&
			\wtjudg{}{v_i}{S_i}{\mathcal{A}_i^{k_{i}}} 
		}
		\]
		Since $\size{\pi_{e}} = \size{\pi_{\Gamma}} + \size{\pi_{x:\mathcal{A}}} = \size{\pi_{\Gamma}} + \size{\pi_{\mathcal{A}}}$, we have $\size\pi > \size\tyd'$ (beccause the $\textsc{T-@}_{2}$ rule is removed), and so we can apply the \textit{i.h.}\xspace, obtaining a run $\sigma: {\state'} \mathrm{\Rew{SpKAM\xspace}}^{*} s_{f}$ to a final state such that $\max_i\{w',u_{\Gamma},u_{\mathcal{A}},v_i\} = \lm\sigma$. Then there is a run $\rho:s \mathrm{\Rew{SpKAM\xspace}}^{*} s_{f}$, proving the first part of the statement (termination).
		
		For the space bound, note that, since $u = \max\set{u_{\Gamma}, u_{x:\mathcal{A}}} = \max\set{u_{\Gamma}, u_{\mathcal{A}}}$, we have $w = \max_i\{w',u_{\Gamma},u_{\mathcal{A}},v_i\}$. Additionally, $\sizes \leq \size{\state'}$, because by the environment domain invariant $e|_t$ removes at most $e(x)$ from $e$, which is however added to the stack. Then $\lm\rho = \lm\sigma = \max_i\{w',u_{\Gamma},u_{\mathcal{A}},v_i\} = w$, proving the second part of the statement.
	
	
\end{proof}

As a corollary, we can transfer back the soundness result from typed \emph{states} to typed \emph{terms}.

\begin{corollary}[Soundness, on Terms]
	Let $t$ be a closed $\lambda$-term. If there exists $\pi\;\triangleright\tjudgw{}{w}{t}{\star}$, then there exists a complete Space KAM\xspace run $\rho$ from $t$ such that $\lm\rho=w$.
\end{corollary}

\subsection{Completeness}
Completeness is the fact that all states on which the Space KAM\xspace terminates are typable. Here the proof technique is standard: we show that final states are typable, that a subject expansion property holds, and then we infer completeness. We do not perform any space analysis, since it  already follows from the soundness part, once we know that a state is typable.

\paragraph{Final States are Typable.} To prove that every final state is typable, we need an auxiliary lemma ensuring that closures and environments can always be typed with empty types and dry type contexts.
\begin{lemma}[Closures and environments are typable]
	\label{l:exists-dry-env-clos}
	\hfill
	\begin{enumerate}
		\item \label{p:exists-dry-env-clos-one} 
		There exists a dry type context $\Gamma$ and a derivation $\pi\;\triangleright \tjudg{}{e}{\Gamma}$ for every environment $e$.
		\item \label{p:exists-dry-env-clos-two} 
		There exist $k$ and a derivation $\pi\;\triangleright \tjudg{}{c}{[\,]^{k}}$ for every closure $c$.
	\end{enumerate}
\end{lemma}

\begin{proof}
	By mutual induction on $e$ and $c$.
	\begin{enumerate}
		\item If $e$ is empty then $\Gamma$ is the empty type context. Otherwise, by \textit{i.h.}\xspace (point 2), for every closure $e(x)$ with $x\in\dome$ there exists $k_{x}$ and a derivation $\pi\;\triangleright \tjudg{}{c}{[\,]^{k_{}}}$. Then $\pi$ is defined as follows:
		\[
		\infer[\textsc{T-env}]{\tjudg{}{e}{\Gamma}}{\tjudg{}{e(x)}{\Gamma(x)}}\]
		
		\item Let $c = (t,e)$. By the environments domain invariant (\reflemma{spkam-invariants}), $\dome = \fvt$. By \textit{i.h.}\xspace (point 1), there exists a dry type context $\Gamma$ and a derivation $\pi\;\triangleright \tjudg{}{e}{\Gamma}$. Since $\dome = \fvt$, we can  apply rule $\textsc{T-none}$ deriving a judgment $\tjudg{\Gamma}{t}{[\,]^{1+\size\Gamma}}$. Then $\pi$ is defined as follows:
		\[\infer[\textsc{T-cl}]{\tjudg{}{(t,e)}{[\,]^{1+\size\Gamma}}}{ 
			\tjudg{}{e}{\Gamma} 
			&& 
			\tjudg{\Gamma}{t}{[\,]^{1+\size\Gamma}} }\]
	\end{enumerate}
\end{proof}

\begin{proposition}[Final states are typable]
	\label{prop:final-states-are-typable}
	Let $s$ be a final state. Then there exists a type derivation $\pi\;\triangleright \tjudg{}{s}{\star}$.
\end{proposition}
\begin{proof}
	Final states have the shape $\spkamstate{\la\vart}e\epsilon$. By \reflemmap{exists-dry-env-clos}{one}, there is a type derivation $\tjudg{}{e}{\Gamma}$ with $\Gamma$ dry. By the environments domain invariant (\reflemma{spkam-invariants}), $\dome = \fv{\la\vart}$. Then $\pi$ is defined as follows:
	\[
	\infer[\textsc{T-st}]{\tjudg{}{\spkamstate{\la\vart}e\epsilon}{\star}}{
		\infer[\textsc{T-}\lambda_\star]{\tjudg{\Gamma}{\lambdax.t}{\star}}{
			\dom\Gamma = \fv{\la\vart} & \Gamma \mbox{ is dry}}
		&
		\tjudg{}{e}{\Gamma}
	}
	\]
\end{proof}

\paragraph{Subject Expansion.} The proof of subject expansion is standard. There is only one delicate point, in expanding the application transitions $\tomachhole{\seanvsym}$ and $\tomachhole{\seavsym}$, where one needs to ensure that the two type contexts for the premises of the application are summable.
\begin{proposition}[Subject expansion]
	\label{prop:sub-exp}
	If $s\mathrm{\Rew{SpKAM\xspace}}{\state'}$ and there exists 
	$\tyd'\;\triangleright\tjudg{}{\state'}\star$, then there exists 
	$\pi\;\triangleright\tjudg{}s\star$.
\end{proposition}

\begin{proof}
	There are three cases that require something more than simply reading backwards the subject reduction argument in the proof of the correctness theorem. One is $\tomachhole{\bwsym}$, where in addition one needs to type the garbage collected closure, but this is ensured by \reflemmap{exists-dry-env-clos}{one}. The other two are the application transitions $\tomachhole{\seanvsym}$ and $\tomachhole{\seavsym}$. We treat $\tomachhole{\seanvsym}$, the case of $\tomachhole{\seavsym}$ is analogous. We have $s=\spkamstate{tu}{e}{c_1\cdotsc_n} \tomachhole{\seanvsym} \spkamstatet{ 
		e|_t}{(u,e|_u)\cdotc_1\cdotsc_n} = {\state'}$.
	The type derivation $\tyd'$ typing  ${\state'}$ has the following shape:
	\[\tyd' = 
	\infer[\textsc{T-st}]{\tjudg{}{\spkamstatet{ 
				e|_t}{(u,e|_u)\cdotc_1\cdotsc_n}}{\star}}{
		\tjudg{\Gamma}{t}{\arr{\mathcal{A}^{k}}{A}}
		&
		\tjudg{}{e|_t}{\Gamma}
		&
		\infer[\textsc{T-cl}]{\tjudg{}{(u,e|_u)}{\mathcal{A}^k}}{\tjudg{\Delta}{u}{\mathcal{A}^{k}}&&
			\tjudg{}{e|_u}{\Delta}}
		&
		\tjudg{}{c_i}{\mathcal{A}_i^{k_{i}}} 
	}
	\]
	Assuming that $\Gamma \#\Delta$, that we shall prove below, the type derivation $\pi$ for $s$ is given by:	
	\[
	\pi := 
	\infer[\textsc{T-st}]{\tjudg{}{\spkamstate{tu}e{c_1\cdotsc_n}}{\star}}{
		\infer[\textsc{T-@}_{1}]{\tjudg{\Gamma\uplus\Delta}{tu}{A
		} }{\tjudg{\Gamma}{t}{\arr{\mathcal{A}^{k}}{A}}
			& 
			\tjudg{\Delta}{u}{\mathcal{A}^{k}}& \Gamma\# \Delta}
		&
		\tjudg{}{e}{\Gamma\uplus\Delta}
		&
		\tjudg{}{c_i}{\mathcal{A}_i^{k_{i}}} 
	}
	\]
	where the derivation for $\tjudg{}{e}{\Gamma\uplus\Delta}$ is obtained by an omitted and straightforward \emph{multi-sets merging} lemma dual to the multi-sets splitting lemma (\reflemma{multiset-splitting}) used for correctness.
	
	We now prove $\Gamma \#\Delta$, which is the additional bit not present in the proof of subject reduction. Let $x \in \dom\Gamma \cap \dom\Delta$. Then $e_{t}(x) = e_{u}(x) = e(x) = c$ for some closure $c$. By \reflemmap{env-clos-size}{two}, we have both $\Gamma(x) = \mathcal{B}_{1}^{\sizec}$ and $\Delta(x) = \mathcal{B}_{2}^{\sizec}$ for some multi types $\mathcal{B}_{1}$ and $\mathcal{B}_{2}$, that is, $\Gamma \#\Delta$.
	
\end{proof}




\begin{theorem}[Completeness]
	Let $s$ a reachable state and $\rho:s\mathrm{\Rew{SpKAM\xspace}}^*s_{f}$ be a KAM\xspace run to a final state $s_{f}$. Then there exist $\pi\;\triangleright\tjudg{}{s}{\star}$.	
\end{theorem}

\begin{proof}
	By induction on the length $\size\rho$ of $\rho$. If $\size\rho = 0$ then $s = s_{f}$, and the existence of a typing derivation for $s$ is given by \refprop{final-states-are-typable}. If $\size\rho > 0$ then $\rho$ is given by a transition $s\mathrm{\Rew{SpKAM\xspace}}{\state'}$ followed by an execution $\sigma: {\state'} \mathrm{\Rew{SpKAM\xspace}}^{*} s_{f}$. By \textit{i.h.}\xspace, we obtain $\pi\;\triangleright\tjudg{}{{\state'}}{\star}$, and by subject expansion (\refprop{sub-exp}) we obtain $\pi\;\triangleright\tjudg{}{s}{\star}$.
\end{proof}

Again, as a corollary, we can transfer the completeness property from \emph{states} to \emph{terms}.
\begin{corollary}[Completeness, on Terms]
	If $t$ is a closed $\lambda$-term such that there exists a complete Space KAM\xspace run from $t$, then there exists $\pi\;\triangleright\tjudg{}{t}{\star}$.
\end{corollary}

Putting together quantitative soundness and completeness gives the quantitative correctness of the closure type system.
\begin{theorem}[Correctness]
	Let $t$ be a closed $\lambda$-term. Then there exists a complete Space KAM\xspace run $\rho$ from $t$ such that $\lm\rho=w$ if and only if there exists $\pi\;\triangleright\tjudgw{}{w}{t}{\star}$.
\end{theorem}
\section{Introduction}
Type systems are a key aspect of programming languages, ensuring good behavior during the execution of programs, such as absence of errors, termination, or properties such as productivity,  safety, and reachability properties.
For functional programming languages, types tend to have the structure of a logical system, to the point that, in the paradigmatic case of the simply typed $\l$-calculus, the type system is \emph{isomorphic} to the natural deduction presentation of intuitionistic logic. This is the celebrated \emph{Curry-Howard correspondence}. 

In the theory of the $\l$-calculus, there is another use of types that has been studied at length by experts, but it is less known to the wider research community on programming languages. Historically, it was introduced by Coppo and Dezani{-}Ciancaglini as the study of \emph{intersection types} \cite{DBLP:journals/aml/CoppoD78}. At first sight, such types are simply a slight variation on simple types, in which one can assign a finite set of types to a term, thus providing a form of finite polymorphism. While some forms of intersection types can be used for programming purposes (see \citet{DBLP:conf/pldi/FreemanP91,DBLP:journals/mscs/Pierce97,DBLP:journals/jacm/FrischCB08,DBLP:conf/birthday/Dezani-Ciancaglini18} or the recent survey by \citet{DBLP:conf/lics/BonoD20}), they have mainly played a more theoretical role, so far. 

Similarly to simple types, intersection types ensure termination. In contrast to most notions of types, however, they also \emph{characterize} termination, that is, they type \emph{all} terminating $\l$-terms. Intersection types have proved to be remarkably flexible, as by tuning details of the type system it is possible to characterize different forms of termination (weak/strong full normalization, head/weak/call-by-value evaluation) for various kinds of $\l$-calculi (with pattern matching, state, probabilities, and more). Termination being only \emph{semi-decidable}, type inference cannot be decidable, which is why standard intersection types are somewhat incompatible with programming practice. As already pointed out, restricted forms of intersection types do find applications in programming languages, but the restrictions usually break the characterization of termination, namely their most peculiar trait.

\paragraph{Abstracting Computation.} The impractical aspect of intersection types can be understood as coming from the fact that inferring a type for $t$ is very similar to normalizing $t$. There is a variant of intersection types where the idempotency of intersections $A\cap A = A$ is dropped, which we refer to as \emph{multi types}, because non-idempotent intersections can be seen as multi-sets. \citet{DBLP:conf/icfp/NeergaardM04} show that, for multi types, type inference is \emph{equivalent} to normalization of the term to type. Careful here: this is \emph{not} a Curry-Howard correspondence, where normalization corresponds to cut (or detour) elimination from the type derivation, which goes through \emph{many} derivations. Here normalization corresponds to  inference of a \emph{single} type derivation, without any rewriting involved. 

The undecidability of type inference is balanced by the fact that, intuitively, multi types fully capture the computing mechanism itself, despite looking very different from a computing device. The $\l$-calculus is already a quite abstract notion of computational model, if compared with Turing or random access machines, but it retains the idea of computation as a state transition system. Multi types push things a level further, as the entire dynamics of normalization is captured by a single \emph{static} type derivation. 

\paragraph{Bounding Computation.} The literature has not really focussed on the relationship between the two processes of normalization and multi type inference, because such a type inference is impractical. Instead, multi type derivations have been used as \emph{exhaustive transcriptions} of the normalization process, from which to extract information about the normalization process itself. The information usually amounts to bound 
\begin{enumerate}
\item the number of steps to normal form, and 
\item  the size of the normal form itself,
\end{enumerate}
according to various notions of reduction (weak head/head/leftmost, for instance). The first such results are de Carvalho's bounds on the length of runs of the Krivine abstract machine~\cite{krivine_call-by-name_2007} (shortened to KAM) and of an extension of the KAM to (strong) leftmost evaluation \cite{deCarvalho07,deCarvalho18}. 
Such a \emph{de Carvalho correspondence} was shortly afterwards extended to strong 
normalization by Bernadet and Lengrand \cite{Bernadet-Lengrand2013} and to linear 
logic proof nets by de Carvalho, Pagani, and Tortora de Falco 
\cite{DBLP:journals/tcs/CarvalhoPF11}. The interest in such a correspondence is 
that it provides an abstract viewpoint on quantitative operational aspects. 
Moreover, the set of multi type judgment for a term $t$ is a syntactic 
presentation of the relational semantics of $t$, a paradigmatic denotational 
model of the $\l$-calculus.


\paragraph{Multi Types and Reasonable Cost Models.} When de Carvalho developed his 
correspondence in 2007, it was known that the number of steps in the weak 
$\l$-calculus is a reasonable time cost model (where \emph{reasonable} roughly 
means equivalent up to a \emph{polynomial} to the time cost model of Turing 
machines), as first proved by Blelloch and Greiner 
\cite{DBLP:conf/fpca/BlellochG95}. The reasonable time cost model of the strong 
(that is, unrestricted) $\l$-calculus was instead unclear (because the techniques 
for the weak case do not work in the strong case), thus it was also unclear to 
what extent the bounds extracted from multi type derivations are related to the 
time complexity of $\l$-terms. In 2014, Accattoli and Dal Lago showed that the 
number of leftmost $\beta$ steps is a reasonable time cost model for strong 
evaluation \cite{accattoli_leftmost-outermost_2016}, clarifying the situation. In 
2018, Accattoli, Graham-Lengrand, and Kesner revisited the de Carvalho 
correspondence and refined it according to the new understanding of time for the 
$\l$-calculus \cite{accattoli_tight_2018}. Their work triggered a systematic 
extension of the de Carvalho correspondence to many $\l$-calculi and abstract 
machines \cite{DBLP:conf/aplas/AccattoliG18,DBLP:conf/esop/AccattoliGL19, 
DBLP:conf/fossacs/KesnerPV21,DBLP:conf/flops/BucciarelliKRV20, 
DBLP:conf/csl/KesnerV22,DBLP:conf/lics/KesnerV20,DBLP:conf/types/AlvesKV19,DBLP:journals/pacmpl/LagoFR21,POPL2021}.

In a recent work \cite{LICS2021}, Accattoli, Dal Lago, and Vanoni pushed  the 
correspondence into a new direction, by extracting the first \emph{space} bounds 
from multi type derivations. Additionally, they use these bounds to disprove a 
conjecture about reasonable space for the $\l$-calculus. Namely, their bounds 
apply to Mackie's and Danos \& Regnier's \emph{interaction abstract 
machine}~\cite{mackie_geometry_1995,DBLP:conf/lics/DanosHR96,DR99,PPDP2020} (which 
is the computational machinery behind Girard's Geometry of 
Interaction~\cite{GIRARD1989221} and Abramsky, Jagadeesan, and Malacaria's game semantics \cite{DBLP:journals/iandc/AbramskyJM00}) and prove that its use of space---that was conjectured to be reasonable---is in fact \emph{unreasonable}.

\paragraph{Reasonable Space.} It is only very recently that results about reasonable space for the $\l$-calculus have started to appear, under the impulse of the advances about reasonable time. Forster, Kunze, and Roth showed that the maximum size of $\l$-terms during evaluation---the natural space cost model---is reasonable \cite{DBLP:journals/pacmpl/ForsterKR20} (that is, it is \emph{linearly} related to the space of Turing machines, as prescribed by Slot and van Emde Boas \cite{DBLP:journals/iandc/SlotB88,DBLP:books/el/leeuwen90/Boas90}). Such a notion of space, however, cannot account for logarithmic space, which is the smallest robust space class, playing the role of $\P$ for space. To study logarithmic space, indeed, one needs a separation between \emph{input} space and \emph{work} space, which cannot be modeled taking as space the size of $\l$-terms. 
Very recently, Accattoli, Dal Lago, and Vanoni have also shown that the space used 
by the \emph{Space KAM\xspace}, a variant over the KAM, is a reasonable space cost model 
accounting for logarithmic space \cite{LICS2022}, solving the longstanding open 
problem. The Space KAM\xspace tweaks the KAM in two orthogonal ways:
\begin{enumerate}
\item \emph{Space optimizations}: it performs two space optimizations, \emph{environment unchaining} and \emph{eager garbage collection}. Unchaining is a folklore optimization that prevents space leaks, that is, it keeps the environment compact. Eager garbage collection maximizes the reuse of space. Essentially, alive closures are compacted and dead closures are removed as soon as possible.

\item \emph{No environment sharing nor pointers}:  the sharing of environments 
used in the implementation of the KAM is \emph{disabled}, and additionally 
environments (as well as the argument stack) are \emph{not} represented as linked 
lists (via pointers). Environments and stacks are instead simply unstructured 
\emph{strings}. These changes are somewhat counter-intuitive but they are in fact 
mandatory for reasonable space, see \cite{LICS2022} for extensive discussions.
\end{enumerate}

Accattoli, Dal Lago, and Vanoni also show results about two \emph{time} cost 
models for the Space KAM\xspace: if time is defined as the number of $\beta$ steps (which is 
the natural, high-level cost model), then the machine is unreasonable (more 
precisely, the overhead of the machine is not polynomial), while if time is 
considered as the time taken by the Space KAM\xspace implementation, then it turns out to be 
a reasonable cost model. Therefore, the Space KAM\xspace is reasonable for both time and 
space, even if for such a simultaneous reasonability one has to pick an unusual 
and low-level notion of time.

\paragraph{Multi Types and Reasonable Space} In this paper, we develop a de Carvalho correspondence for the Space KAM\xspace from which we extract the \emph{space} cost of machine runs. It is the first such correspondence measuring a reasonable notion of space for the $\l$-calculus. And as it is typical of intersection and multi types, the type system characterizes---and thus provides the \emph{exact} space consumption---for \emph{all} terminating $\l$-terms (with respect to (weak) CbN\xspace evaluation).

De Carvalho seminal work is about the KAM, and relies on the fact that one can see the KAM transition rules as deductive rules of the multi type system. Since the Space KAM\xspace is an optimized machine, with modified transitions, we do modify the type system in order to obtain the same correspondence. The key points of the type system are the following ones:
\begin{itemize} 
\item \emph{Unusual weakening}: the handling of garbage collection induces an unusual approach to \emph{weakening}. The reason is that the Space KAM\xspace and the type system implement \emph{weak} evaluation, which does not inspect abstraction bodies, but the definition of garbage is \emph{strong}, as it depends also on occurrences inside abstractions. 

\item \emph{Indices}: multi types associated to arguments have an index, which is simply a natural number. These indices reflect the size of the \emph{closure} that shall be built for that argument by the Space KAM\xspace. They seem arbitrary at first, but if a closed term is typable with a ground type then the indices are uniquely determined, and they capture \emph{exactly} the size of closures. Judgments carry a \emph{weight}, which is another natural number, this time corresponding to the maximum space used by the Space KAM\xspace in the run represented by the derivation ending on that judgment.

\item \emph{Soundness proof}: soundness of the type system---that is, \emph{$t$ typable with weight $w$ implies that the Space KAM\xspace run on $t$ ends and has space cost $w$}---follows a slightly unusual pattern.  We merge together the statements of subject reduction and soundness, which are usually disentangled in the literature. The merge helps proving the space bound.

\item \emph{Abstraction of the space cost}: the type system actually counts 
\emph{the maximum number of closures} used by the Space KAM\xspace. Roughly, the 
\emph{actual space} is obtained by multiplying such a number by the logarithm of 
the size of the initial term, which corresponds to the size of the \emph{code 
pointer} in every closure. More precisely, the simulation of Turing machines 
within a linear overhead in \cite{LICS2022} rests on some technicalities for which 
not all code pointers have the same size. Here, we abstract away from those 
technicalities, and simply count the number of closures. Still, by fine tuning the 
type system, at the cost of losing clearness, one could recover all the 
information.
\end{itemize}

A further contribution of the paper is that, after the study of space, we slightly modify the weights on judgments as to extract the exact \emph{time} cost of runs, instead of the space cost. Therefore, we are able to measure both reasonable time and reasonable space using the same underlying type system decorated with different weights.

\paragraph{Abstracting the Space KAM\xspace} For proving that the two type systems capture the time and the space of the Space KAM\xspace, we extend the typing rules the states and data structures of the Space KAM\xspace. The exact bounds for a term $t$, however, can be read out \emph{directly} from the typing of $t$, with no need to type states of the Space KAM\xspace. Thus, the extension of the type system to machine states is only a technical tool for the proof of the correspondence. This fact shows that the type system allows us to manipulate the time and space complexities of a term abstracting away from the machine on which these measures are defined. This is the main contribution of the paper.









\section{Conclusions}
This paper is set in the recent trend aiming at analyzing complexity properties of $\l$-terms through the use of multi types (a.k.a. non-idempotent intersection types). Taking advantage of a recent result about a reasonable  space measure for the call-by-name $\l$-calculus, we craft a multi type system able to reflect such a measure on typed $\l$-terms. 

There are at least two interesting directions for future work. Firstly, we would 
like to adapt the type system to cover call-by-value evaluation, where a notion of 
reasonable space measure is known~\cite{LICS2022}, too. Secondly, it would be 
interesting to understand what happens in the case of infinite computations. In 
these cases, the space consumption can be either finite, if the machine cycles, or 
infinite. In the former case, a newly devised (coinductive) type system could give 
the space bound. In the latter case, one could be interested in asymptotic 
properties, e.g.\xspace ``during the (infinite) execution, the space consumption is 
logarithmic in time''. This kind of properties could be useful in applications 
that have to do with infinite data, such as stream processing, and in general with 
lazy infinite (coinductive) data structures. For designing the type system, one 
might possibly build on Vial's study of infinitary evaluation based on a variant 
of multi types \cite{DBLP:conf/lics/Vial17}.


\bibliographystyle{ACM-Reference-Format}

\section{Preliminaries}
Here we gently introduce the technical tools that are going to be used and refined along the paper, namely the $\l$-calculus, Krivine's abstract machine, and multi types.

\paragraph{Reasonable Cost Models.} Before starting with the technical discussion, we recall Slot and van Emde Boas' invariance thesis \cite{DBLP:journals/iandc/SlotB88} (also called strong, extended, efficient, modern, or
complexity-theoretic Church(-Turing) thesis in the literature), that states: 
\emph{reasonable computational theories\footnote{Slot and van Emde Boas speak of 
\emph{machines} rather than \emph{computational theories} because they are mainly 
discussing Turing and random access machines. Since the $\l$-calculus is not 
formulated as a machine, we prefer to speak of \emph{computational theory} (and 
avoid \emph{computational model} for the collision with \emph{cost model}).} 
simulate each other with polynomially bounded overhead in time and a linear 
overhead in space}. The rationale behind this thesis is that, under these 
constraints, complexity classes such as \textsf{LOGSPACE}, $\P$, and $\mathsf{PSPACE}$ 
become robust, i.e.\xspace theory-independent. We invite the reader to consult 
\citet{DBLP:journals/entcs/Accattoli18,LICS2022} for more details.


\subsection{The Closed Call-by-Name $\l$-Calculus}
Let $\mathcal{V}$ be a countable set 
of variables. 
Terms of the \emph{$\lambda$-calculus} $\Lambda$ are defined as follows:
\[
\begin{array}{rrcl}
\textsc{$\l$-terms}\quad\quad & t,u,r & ::= & 
x\in\mathcal{V}\; \; \mbox{\Large{$\mid$}}\;\; \lambda x.t\; \; \mbox{\Large{$\mid$}}\;\; 
tu.
\end{array}
\]
\emph{Free} and \emph{bound variables} are defined as 
usual: $\la\vart$ binds $x$ in $t$.
Terms are considered modulo $\alpha$-equivalence, and 
$t\isub\varu$ denotes capture-avoiding (meta-level) substitution of 
all the free occurrences of $x$ for $u$ in $t$.
The operational semantics of the $\l$-calculus is given by just one rewriting 
rule, called the $\beta$-rule:
\[
(\la\vart)u\mapsto_\betat\isub\varu
\]
Terms like $(\la\vart)u$, called reducible expressions, or \emph{redexes}, can 
occur as sub-terms inside a bigger term. Restricting the 
$\beta$-rule to only some of the redexes, i.e.\xspace defining a \emph{reduction 
	strategy}, gives rise to the different 
$\l$-calculi. In this paper we deal mainly with a very simple fragment, 
which we call Closed Call-by-Name\xspace (shortened to Closed \cbn). It is dubbed \emph{closed}, because we consider 
only 
closed terms, i.e.\xspace terms which do not have any free variable, and 
\emph{call-by-name}, because 
arguments are substituted inside function bodies unevaluated. Moreover, Closed \cbn 
is a \emph{weak} strategy, sometimes called  \emph{weak head reduction}, because it 
does not 
evaluate under abstractions\footnote{Which is common practice in functional 
	programming languages.} (which are its all and only normal forms), and 
because it evaluates only the head redex. We can define Closed \cbn reduction via the following rule that can only be applied at top level:
\[
(\lax t) u r_1 \ldots 
r_h \ \ \Rew{wh} \ \ t \isubx u 
r_1 \ldots r_h \ \ \ \\ \  h\geq 0.
\]
For instance, we have $(\lax\vartwox\var) t \Rew{wh} \la\vartwot\tm$ and $(\lax\vartwox\var) t u \Rew{wh} (\la\vartwot\tm) u$ but $r ((\lax\vartwox\var) t u) \not \Rew{wh} r ((\la\vartwot\tm) u)$ and $\laz((\lax\vartwox\var) t u) \not \Rew{wh} \laz((\la\vartwot\tm) u)$.

It is easily seen that weak head reduction is deterministic.

\begin{example}
	In the remainder of this paper, we are going to present different evaluation mechanisms for the $\l$-calculus. For each of them, we are going to develop a complete example. Each of these examples is based on the execution of the $\l$-term $(\lax(\lay(\la\varthreex)(xy))x)\symfont{I}$ where $\symfont{I}:=\la a a$ is the identity combinator. Here we show its Closed \cbn evaluation, that takes 3 $\beta$-steps.
	\[
	(\lax(\lay(\la\varthreex)(xy))x)\symfont{I} \Rew{wh} (\lay(\laz\symfont{I})(\Idy))\symfont{I} \Rew{wh} (\laz\symfont{I})(\symfont{I}\Id) \Rew{wh} \symfont{I}
	\]
\end{example}

\begin{figure}
	\input{machines/KAM}
	\caption{KAM\xspace data structures and transitions.}
	\label{fig:KAM}
\end{figure}

\subsection{The Krivine Abstract Machine}
The KAM is a 
standard environment-based machine for Closed \cbn, often defined as in 
Fig.~\ref{fig:KAM}. 
The machine evaluates closed $\l$-terms to weak head normal form via three 
transitions, the union of which is noted $\mathrm{\Rew{KAM\xspace}}$: 
\begin{itemize}
	\item $\tomachhole{\seasym}$ looks for redexes descending on the left of topmost 
	applications 
	of the active term, accumulating arguments on the stack; 
	\item $\tomachhole{\beta}$ fires a $\beta$ redex (given by an abstraction as active 
	term 
	having as argument the first entry of the stack) but delays the associated 
	meta-level substitutions, adding a corresponding explicit substitution to 
	the 
	environment;
	\item $\tomachhole{\subsym}$ is a form of micro-step substitution: when the active 
	term is $x$, the machine looks up the environment and retrieves the 
	delayed replacement for $x$.
\end{itemize}
The data structures used by the KAM\xspace are \emph{local environments}, 
\emph{closures}, and a \emph{stack}. \emph{Local environments}, that we shall 
simply refer to as \emph{environments}, are defined by mutual induction with 
\emph{closures}.
The idea is that every (potentially open) term $t$ occurring in a state comes 
with an 
environment $e$ that \emph{closes} it, thus forming a 
closure $c = (t,e)$, and, in turn, environments are lists of entries 
$\esubxc$ associating to each open variable $x$ of $t$, a closure 
$c$ i.e.\xspace, intuitively, a closed term.
The \emph{stack} simply collects the closures associated to the arguments met 
during the search for $\beta$-redexes.

A state $s$ of the KAM\xspace is the pair $(c,S)$ of a 
closure $c$ and a stack $S$, but we rather see it as a triple 
$(t,e,S)$ by spelling out the two components of the closure $c = 
(t,e)$.
Initial states of the KAM\xspace
are defined as $\compil{t_{0}}:=\kstate{t_{0}}{\epsilon}{\epsilon}$ 
(where $t_{0}$ is a closed $\l$-term, and also the code). A state is \emph{final} if no transitions apply. A \emph{run} $\rho: s \tomachhole{}^*{\state'}$ is a possibly empty sequence of transitions, the length of which is noted 
$\size\rho$. If $a$ is a transition label, $\sizeparam\rho a$ 
is the number of $a$ transitions in $\rho$. An \emph{initial run} is a run from an initial state $\compilt$, and it is also called \emph{a run from $t$}. A state $s$ is \emph{reachable} if it 
is the target state of an initial run. A \emph{complete run} is an initial run ending on a final state.
In a state $\spkamstateteS$ that is reachable by an initial state $\compil{t_{0}}$, $t$ is always a sub-term of $t_0$. For this reason $t_{0}$ has a special role during the execution. Indeed, any sub-term $t$ of $t_{0}$ can be seen as a pointer to $t_{0}$ which we call the \emph{initial immutable code}. 

The key point in the proof of the correctness of the KAM\xspace is that there is a bijection between $\Rew{wh}$ steps and $\tomachhole{\beta}$ transitions, so that we can identify the two. In particular, KAM\xspace states can be \emph{decoded} to $\lambda$-terms via the following decoding function $\unf\cdot$ for closures and states: 
\[\begin{array}{rrcl@{\hspace{2cm}}rcl}
\textsc{Closures}
&
\unf{(t, \epsilon)} & := & t
&
\unf{(t, \esubxc\conse)} & := & 
\unf{(t\isubx{\unfc},e)}

\\[3pt]
\textsc{States}
&
\unf{(t, e, \epsilon)} & := & \unf{(t, e)}
&
\unf{(t, e, S\consc)} & := & \unf{(t, e, 
	S)}\, \unfc
\end{array}\]

\begin{theorem}[KAM Correctness~\citep{DBLP:conf/icfp/AccattoliBM14}]
	The KAM\xspace implements Closed \cbn, that is, there is a complete $\Rew{wh}$-sequence 
	$t \Rew{wh}^{n} u$ if and only if there is a complete run $\rho: 
	\compilt \mathrm{\Rew{KAM\xspace}}^{*} s$ such that $\unfs = u$ and 
	$\sizeb\rho = n$.
\end{theorem}
\begin{example}
	We provide the KAM\xspace execution of our example term $(\lax(\lay(\la\varthreex)(xy))x)\symfont{I}$.
	\[
	\begin{array}{l|l|ll}
	\mathsf{Term}   & 
	\mathsf{Environment} & \mathsf{Stack}\\
	\cline{1-3}
	(\lax(\lay(\la\varthreex)(xy))x)\symfont{I} & \epsilon & \epsilon & \tomachhole{\seasym}\\
	\lax(\lay(\la\varthreex)(xy))x & \epsilon & (\symfont{I},\epsilon) & \tomachhole{\beta}\\
	(\lay(\la\varthreex)(xy))x & \esubx{(\symfont{I},\epsilon)} & \epsilon & \tomachhole{\seasym}\\
	\lay(\la\varthreex)(xy) & \esubx{(\symfont{I},\epsilon)} & (x,\esubx{(\symfont{I},\epsilon)}) & \tomachhole{\beta} \\
	(\la\varthreex)(xy) & \esuby{(x,\esubx{(\symfont{I},\epsilon)})} \cdot \esubx{(\symfont{I},\epsilon)}=:e & \epsilon & \tomachhole{\seasym}\\
	\la\varthreex & \esuby{(x,\esubx{(\symfont{I},\epsilon)})} \cdot \esubx{(\symfont{I},\epsilon)} & (xy,e) & \tomachhole{\beta}\\
	x & \esubz{(xy,e)}\cdot \esuby{(x,\esubx{(\symfont{I},\epsilon)})} \cdot \esubx{(\symfont{I},\epsilon)} & \epsilon & \tomachhole{\subsym}\\
	\symfont{I} & \epsilon & \epsilon
	\end{array}
	\]
	We can observe that the evaluation takes 7 steps, of which 3 are $\beta$-steps, 3 are $\tomachhole{\seasym}$-steps, and 1 is a $\tomachhole{\subsym}$-step.
\end{example}

\subsection{Closed \cbn Multi Types}
We give in this section an introduction to multi types, also known as \emph{non-idempotent 
intersection types}. First, we consider them from the 
\emph{qualitative} point 
of view, and then we refine our analysis \emph{quantitatively}. We will review 
them quite quickly, inviting the reader to consult \citep{BKV17} about the 
qualitative part, and \citep{DBLP:journals/jfp/AccattoliGK20} about the 
quantitative one. Multi types are 
deeply related to linear logic in how they keep track of the use of resources, and in 
particular their grammar is reminiscent of 
the (call-by-name, in our case) translation $(\cdot)^\dagger$ of intuitionistic 
logic into linear 
logic $(A\to B)^\dagger=\,!A^\dagger\multimap B^\dagger$. Semantically, they can 
be seen as a syntactical presentation of the relational 
model~\citep{DBLP:journals/apal/BucciarelliE01} of the $\l$-calculus, induced by the relational semantics of linear logic via the CbN\xspace translation $(\cdot)^\dagger$. 

The grammar for types is based on \emph{two} layers of types, defined in a
mutually recursive way, linear types $A$ and finite multi sets $\mathcal{A}$ of 
linear types, this can also be considered a non-idempotent variant of 
\citet{DBLP:journals/tcs/Bakel92} strict types.
\[
\begin{array}{rrcll}
\textsc{Linear 
	types}&A,\linty'&::=&\star\; \; \mbox{\Large{$\mid$}}\;\;\arr{\mathcal{A}}{A}

\\[3pt]
\textsc{Multi 
	types}&\mathcal{A},\mathcal{B}&::=&\mset{A_1,\ldots,A_n} \qquad 
n\geq 0
\end{array}
\]

Note that there is a ground 
type $\star$, which can be thought as 
the type of normal forms, that in Closed \cbn are precisely abstractions. Note also 
that arrow (linear) types $\arr{\mathcal{A}}{A}$ 
can have a multiset only on the left. The empty multiset is noted $[\,]$, 
and the union of two multisets $\mathcal{A}$ and $\mathcal{B}$ is noted $\mathcal{A}\uplus\mathcal{B}$. 

Type environments, ranged over by $\Gamma,\Delta$ are partial maps
from variables to multi types such that only finitely
many variables are mapped to non-empty multi types, and we write $\Gamma = 
x_1:\mathcal{A}_1,\ldots,x_n:\mathcal{A}_n$ if 
$\dom\Gamma = \set{x_1,\ldots,x_n}$.
Given two type environments $\Gamma,\Delta$, the expression
$\Gamma\uplus\Delta$ stands for the type environment
assigning to every variable $x$ the multiset
$\Gamma(x)\uplus\Delta(x)$.

Type 
judgments have the form $\tjudg{\Gamma}{t}{A}$ where $\Gamma$ is a type 
environment. The 
typing rules are in \reffig{mtypesystem}; type derivations are noted $\pi$ 
and we write 
$\pi\;\triangleright\tjudg{\Gamma}{t}{A}$ for a type derivation $\pi$ with the 
judgment $\tjudg{\Gamma}{t}{A}$ as its conclusion.

\begin{figure}[t]
	\[
	\begin{array}{c@{\hspace{1cm}}c@{\hspace{1cm}}c}
	\infer[\textsc{T-Var}]{\tjudg{x:\mset{A}}{x}{A}}{}
	&
	\infer[\textsc{T-}\lambda]{\tjudg{\Gamma}{\lambdax.t}{\arr{\mathcal{A}}{A}}} 
	{\tjudg{\Gamma,x:\mathcal{A}}{t}{A}}
	&
	\infer[\textsc{T-}\lambda_\star]{\tjudg{}{\lambdax.t}{\star}}{}
	\\[8pt]
	\multicolumn{3}{c}{\infer[\textsc{T-@}]{\tjudg{\Gamma\uplus 
				\biguplus_{i\in\mset{1,\ldots,n}} \Delta_i  
			}{tu}{A 
		}}{\tjudg{\Gamma}{t}{\arr{\mset{\linty'_1,\ldots,\linty'_n}}{A}}
			& 
			\mset{\tjudg{\Delta_i}{u}{\linty'_i}}_{i\in\mset{1,\ldots,n}}}}
	\end{array}
	\]
	\caption{The multi type system for Closed \cbn.}
	\label{fig:mtypesystem}
\end{figure}

Intuitively, a linear type $A$ corresponds to a single use of a term, while the cardinality of a multi type assigned to an argument $t$ stands for the number of times this term $t$ will be \emph{copied} during the reduction. More precisely, the cardinality corresponds to the number of times that $t$ is \emph{used} by the KAM, that is, the number of times that $t$ is substituted on the head variable during the KAM run.
Different uses of $t$ during a run are allowed to have different types: this is precisely the reason why we need the multiset operator. As an example, we show the type derivation for the term $(\lax\varx)(\lay\vartwo)$.
\[
\infer[\textsc{T-@}]{\tjudg{}{(\lax\varx)(\lay\vartwo)}{\star}}{
	\infer[\textsc{T-}\lambda]{\tjudg{}{\lax{x\var}}{\arr{\mset{\arr{\mset{\star}}{\star},\star}}{\star}}}{
		\infer[\textsc{T-@}]{\tjudg{x:\mset{\arr{\mset{\star}}{\star},\star}}{x\var}{\star}}{
			\infer[\textsc{T-Var}]{\tjudg{x:\mset{\arr{\mset{\star}}{\star}}}{x}{\arr{\mset{\star}}{\star}}}{}
			& \infer[\textsc{T-Var}]{\tjudg{x:\mset\star}{x}{\star}}{}}} &
	\hspace{-12pt}\infer[\textsc{T-}\lambda]{\tjudg{}{\lay\vartwo}{\arr{\mset{\star}}{\star}}}{
		\infer[\textsc{T-Var}]{\tjudg{y:\star}{y}{\star}}{}} &
	\infer[\textsc{T-}\lambda_\star]{\tjudg{}{\lay\vartwo}{\star}}{}}
\]
The reader can notice that the argument $\lay\vartwo$ is typed twice, and with different types. It is typed once with $\arr{\mset{\star}}{\star}$, when it is used as a function, and once with $\star$, when it is used as a value. Moreover, the finite polymorphism of multi types allows us to type the term $\lax\varx$, which is not typable with simple types.




\paragraph{Characterization of Termination.} Multi types characterize Closed 
CbN termination, that is, they type all and only those $\l$-terms that terminate
with respect to Closed CbN. Differently from what happens with  idempotent intersection types, such a result has an easy proof with multi types. Soundness, that is, the fact that typable terms terminate, is usually the hard part, as it requires to exhibit a termination argument. For idempotent intersection types one needs to use the reducibility method, which is a quite heavy machinery. For multi types, there is a strikingly simpler argument: a quantitative form of subject reduction holds, stating that the size of the type derivation decreases with each weak head $\beta$-step, which then provides the termination measure. A similar argument shall be used in Section \ref{sec:correctness}.

Completeness of the type system, that is, every terminating term is typable, is proved as for idempotent intersection types, by showing that all weak head normal forms are typable and via a subject \emph{expansion} property.

\begin{theorem}[Characterization of weak head normalization]
	A closed term $t$ has weak head normal form if and only if there exists a multi type  derivation
	$\pi\;\triangleright\tjudg{}{t}{\star}$.
\end{theorem}

\paragraph{Multi Types and the KAM\xspace Time Consumption.} Multi types have been 
successfully 
applied in quantitative 
analyses of normalization, starting with \citet{deCarvalho07,deCarvalho18}, who 
used them to give a bound to the length of KAM\xspace runs. 
De Carvalho's technique can be re-phrased and distilled as a decoration of  
type derivations with \emph{weights}, that is, cost annotations, following the 
scheme of \reffig{weightskam}. This weight system just measures the size of the type derivation, since for each rule R, it adds 1 to the weight of the tree rooted in R. Please 
note that the 
weight assignment is blind to types (which is why terms and types are removed from \reffig{weightskam}), and thus relies only on the structure, an in particular the size, of the type derivation.  De Carvalho's result can be formulated as follows.
\begin{theorem}[de Carvalho]\label{thm:decarvalho}
	Let $t$ be a closed $\lambda$-term. Then there exists a complete KAM\xspace run $\rho$ from $t$ of length $w$ if and only if there exists a multi type derivation $\pi\;\triangleright\wtjudg{}{w}{t}{\star}$.
\end{theorem}
The KAM\xspace being deterministic, one has that all derivations 
$\tjudg{}{t}{\star}$ induce the same weights. Moreover, there is a stronger 
correspondence between the rules of the type system, and the transitions of the 
KAM\xspace, in the special case of closed terms typed with $\star$. Every $\textsc{T-@}$ rule corresponds to a $\tomachhole{\seasym}$ transition, every 
$\textsc{T-}\lambda$ rule corresponds to a $\tomachhole{\beta}$ transition\footnote{This way, multi 
	type derivations can be used to count also the number of $\Rew{wh}$-steps a 
	$\l$-term needs to normalize, which is the natural time cost model for Closed \cbn.}, and every $\textsc{T-Var}$ rule 
corresponds to a $\tomachhole{\subsym}$ transition. The only $\textsc{T-}\lambda_\star$ rule in a type 
derivation for $t$ corresponds 
to the final state of the KAM\xspace run on $t$. The correspondence is deep, each 
state of the 
KAM\xspace run for a $\l$-term $t$ corresponds to a type judgment occurrence in the type derivation of $t$, in such a way that the sub-term of the state is exactly the same sub-term typed by the judgment. In other words, the KAM\xspace and multi types \emph{compute} in the \emph{same} way (in the special case of closed terms typed with $\star$), they only differ in how such a computation is presented.

\begin{example}
	We provide the weighted multi type derivation of our running example term $(\lax(\lay(\la\varthreex)(xy))x)\symfont{I}$.
	\[
	\infer[\textsc{T-@}]{\tjudgw{}{7} {(\lax(\lay(\la\varthreex)(xy))x)\symfont{I}}{\star}}{
	\infer[\textsc{T-}\lambda]{\tjudgw{}{6}{\lax(\lay(\la\varthreex)(xy))x} {\arr{\mset{\star}}\star}}{
	\infer[\textsc{T-@}]{\tjudgw{x:\mset\star}{5}{(\lay(\la\varthreex)(xy))x}{\star}}{\infer[\textsc{T-}\lambda]{\tjudgw{x:\mset\star}{4}{\lay(\la\varthreex)(xy)} {\arr[\,]\star}}{
	\infer[\textsc{T-@}]{\tjudgw{x:\mset\star}{3}{(\la\varthreex)(xy)}{\star}}{
	\infer[\textsc{T-}\lambda]{\tjudgw{x:\mset\star}{2}{\la\varthreex}{\arr[\,]\star}}{
	\infer[\textsc{T-Var}]{\tjudgw{x:\mset\star}{1}{x}{\star}}{}}}}}} & 
	\infer[\textsc{T-}\lambda_\star]{\tjudgw{}{0}{\symfont{I}}{\star}}{}}
	\]
	We note that there is a precise correspondence between this type derivation and the KAM\xspace execution of the same term. Indeed, the final weight is 7, as the number of KAM\xspace transitions. Moreover, each occurrence of rule $\textsc{T-}\lambda$ corresponds to a transition $\tomachhole{\beta}$, each occurrence of rule $\textsc{T-@}$ corresponds to a transition $\tomachhole{\seasym}$, and each occurrence of rule $\textsc{T-Var}$ corresponds to a transition $\tomachhole{\subsym}$.
\end{example}

\begin{figure}
	\begin{center}
		\begin{tabular}{c}
			$\begin{array}{c@{\hspace{1.5cm}}c@{\hspace{1.5cm}}c@{\hspace{1.5cm}}c}
			\infer[\textsc{T-Var}]{\wtjudgone{1}}{}
			&
			\infer[\textsc{T-}\lambda]{\wtjudgone{w+1}}{\wtjudgone{w}}
			&
			\infer[\textsc{T-}\lambda_\star]{\wtjudgone{0}}{}
			&
			\infer[\textsc{T-@}]{\wtjudgone{w+\sum 
					v_i+1}}{\wtjudgone{w} & 
				\mset{\wtjudgone{v_i}}_{i\in\mset{1,\ldots,n}}}
			\end{array}$
		\end{tabular}
	\end{center}
	\caption{The weight assignment measuring the size of multi type derivations/KAM execution time.}\label{fig:aaweightKAMtime}
	\label{fig:weightskam}  
\end{figure}

\section{The Space KAM\xspace} Here, we present an optimization of the KAM, that we call Space KAM\xspace, aiming at space \emph{reasonability}. More specifically, two modifications are implemented in order to achieve reasonability, namely \emph{unchaining} and \emph{eager garbage collection}.

\paragraph{Unchaining.} It is a 
folklore 
optimization for abstract 
machines  bringing speed-ups with respect to both time and space, used e.g.\xspace 
by Sands et al. \cite{DBLP:conf/birthday/SandsGM02}, Wand 
\cite{DBLP:journals/lisp/Wand07}, Friedman et al. 
\cite{DBLP:journals/lisp/FriedmanGSW07}, and Sestoft 
\cite{DBLP:journals/jfp/Sestoft97}. Its first 
systematic study is by Accattoli and Sacerdoti Coen in 
\cite{DBLP:journals/iandc/AccattoliC17}, with respect to time. This optimization prevents the creation of chains of \emph{renamings} in environments, that is, of delayed substitutions of variables for variables, of which the simplest shape in the KAM\xspace is:
\begin{center}$\esub{x_0}{(x_1, \esub{x_1}{(x_2, 
			\esub{x_2}{\ldots})})}$\end{center}
where the links of the chain are generated by $\beta$-redexes having a variable 
as argument. On some families of terms, these chains keep growing and growing, 
leading to the quadratic dependency of the number of transitions from $\sizeb\rho$, and to the continuous increase of space consumption. An example of continuosly growing chain of renamings is easily obtained by computing finite prefixes of the KAM execution of the standard looping term $\Omega$.

\paragraph{Eager Garbage Collection.} Beside the malicious chains connected to 
unchaining,  the Naive KAM\xspace is not parsimonious with space also because there is no 
garbage collection (shortened to GC). In transition $\tomachhole{\subsym}$, the current 
environment is discarded, so something is collected, but this is not enough. 
It is thus natural to modify the machine as to maximize GC and space re-usage, that is, as to perform it \emph{eagerly}. 

\begin{figure}[t]
	\include{machines/SpaceKAM}
	\caption{Space KAM\xspace data structures and transitions.}
	\label{fig:spkam}
\end{figure}

\paragraph{Space KAM\xspace Transitions and Data Structures.}
The KAM\xspace optimized with both eager GC and unchaining 
(both optimizations are mandatory for space reasonability)
is here called Space KAM\xspace and it is defined in \reffig{spkam}. The data structures, 
namely closures and (local) environments, are defined as for the KAM\xspace, the changes 
concern the machine transitions only. Unchaining is realized by transition 
$\tomachhole{\seavsym}$, while
eager garbage collection is realized mainly by transition $\tomachhole{\bwsym}$, which 
discards the argument if the variable of the $\beta$ redex does not occur. 
Transitions $\tomachhole{\seanvsym}$ and $\tomachhole{\seavsym}$ also contribute to implement the GC, by restricting the environment to the occurring variables, when the environment is propagated to sub-terms. As a consequence, we obtain the following invariant.

\begin{lemma}[Environment domain invariant]
	\label{l:spkam-invariants}
	Let $s$ be a Space KAM\xspace reachable state. Then $\dome = \fvt$ for every 
	closure $(t,e)$ in $s$.
\end{lemma}
Because of the invariant, which concerns also the closure given by the active term 
and the local environment of the state, the variable transition $\tomachhole{\subsym}$ 
simplifies as follows:
\[\begin{array}{l@{\hspace{.3cm}} 
	l@{\hspace{.3cm}}l|l|l@{\hspace{.3cm}} 
	l@{\hspace{.3cm}}l}
\mathsf{Term}   & 
\mathsf{Env} & \mathsf{Stack}
&&	\mathsf{Term} 
& 
\mathsf{Env}
& \mathsf{Stack} 
\\
\cline{1-7}
x    &
\esubx{(u,e)}
& S
&
\tomachhole{\subsym} 
u  & e & S
\end{array}\]

\paragraph{Implementation and Space Consumption} We consider the Space KAM\xspace implemented in a rather unusual way, in order to obtain a space reasonable machine. Indeed, we avoid any form of sharing of data structures. Transitions $\tomachhole{\seanvsym}$ and $\tomachhole{\seavsym}$ actually copy the environment itself, and not just a pointer to it. Moreover, all the data structures are implemented as unstructured strings, i.e.\xspace not as linked lists or trees (just think about implementing the Space KAM\xspace directly on a multi tape Turing machine, rather than on a RAM). In this way, the machine does not rest on pointers for structuring the stack and the environment data structures, and this is crucial, as such pointers would add an unreasonable space overhead. Pointers do not disappear altogether: pointers to the initial immutable code are used to represent the left component of every closure (that is, the term $u$ in $(u,e)$), which, by the key \emph{sub-term invariant} of the KAM, is always a sub-term of the initial code. The use of these pointers is another crucial ingredient for space reasonability, as it allows to avoid the copy of sub-terms which would make the code grow during execution (that must be avoided to account for logarithmic space).

The avoidance of data structure pointers is also the reasong why garbage 
collection can  be easily implemented eagerly, as it is assumed by the Space KAM\xspace. If 
one instead adopts a more standard form of \emph{shared} environments (which are 
based on using pointers) then garbage collection becomes trickier, because of 
\emph{aliasing}, that is, the fact that shared environments can be referenced more 
than once. Our approach, instead, does not suffer from this difficulty, since 
\emph{nothing} is shared. Such a choice of course degrades the time performance, 
but here we are mainly interested in space behavior. All these implementation 
choices, necessary to obtain the space reasonability of the Space KAM, are 
discussed at length in~\citet{LICS2022}.


\newcommand{\rsize}[1]{||#1||}

\paragraph{Space and Number of Closures of the Space KAM\xspace} Intuitively, the space occupied by a state $s$ of the Space KAM\xspace during a run of initial immutable code $t_0$ is the number $n$ of closures in $s$ multiplied by the logarithm $\log\size{t_0}$ of the size of the initial immutable code $t_{0}$, accounting for the code in every closure (that is, the left component), which is represented as a pointer to the initial code (because of the sub-term invariant of the KAM mentioned above).

For the space reasonability result in \cite{LICS2022}, however, a trickier notion 
of space is used, as the initial code is divided in \emph{two} address spaces and 
so not every pointer takes space $\log\size{t_0}$ (some use less space). We 
abstract away from such a technical aspect, because it is needed to study the 
representation of Turing machines, but on $\l$-terms that do not belong to the 
image of the encoding of Turing machines it is irrelevant. Therefore, we use an 
abstract notion of space, namely \emph{the number of closures in a state}, which 
roughly is the space of the Space KAM\xspace up to $\log\size{t_0}$.

\begin{definition}[Abstract space]
	The abstract space $\sizes$ taken by a Space KAM\xspace state $s$ with initial immutable code $t_0$ is defined on the structure of Space KAM\xspace states as follows\footnote{In the clause about states, we could have written $\size{(t,e,S)} :=  \size{e}+\size{S}+1$, counting also the space for the closure $(t,e)$. Since the difference is just about a constant, we can remove that ``$+1$'' without loss of generality. The removal of the $+1$ shall slightly simplify the extraction of the space usage from multi type derivations in Section \ref{sec:correctness}.}.
\[\begin{array}{ccccccc}
	\textsc{Environments}
	&
	\textsc{Stacks}\\
	\begin{array}{rcl}
	\size{\epsilon} & := &0
	\\
	\size{\esubxc\cdote} & := & \size{c}+\size{e}
	\end{array}
	&
	\begin{array}{rcl}
	\size{\epsilon} & := &0
	\\
	\size{c\cdotS} & := &	\size{c}+\size{S}
	\end{array}
	\\\\
	
	\textsc{Closures} 
	&		
	\textsc{States}\\
	\begin{array}{rcl}
	\size{(t,e)} & := & 1+\sizee 
	\end{array}
	& 
	\begin{array}{rcl}			
	\size{(t,e,S)} &:= & \size{e}+\size{S}
	\end{array}
	\end{array}\]
\end{definition}


The size a Space KAM\xspace run then it is obtained by considering the maximum size of the states reached along that run.

\newcommand{\rlm}[1]{||#1||_{\mathsf{sp}}}

\begin{definition}[Run Abstract Space]
	Let $\rho:\compil{t_0}\mathrm{\Rew{SpKAM\xspace}}^*s$ be a Space KAM\xspace run. Then the (abstract) space consumption of the run $\rho$ is defined as follows:
	\[\lm{\rho}:=\max_{{\state'}\in\rho}\size{{\state'}}\]
\end{definition}


\begin{example}
	We provide the Space KAM\xspace execution of our example term $(\lax(\lay(\la\varthreex)(xy))x)\symfont{I}$.
	\[
	\begin{array}{l|l|ll}
	\mathsf{Term}   & 
	\mathsf{Environment} & \mathsf{Stack}\\
	\cline{1-3}
	(\lax(\lay(\la\varthreex)(xy))x)\symfont{I} & \epsilon & \epsilon & \tomachhole{\seanvsym}\\
	\lax(\lay(\la\varthreex)(xy))x & \epsilon & (\symfont{I},\epsilon) & \tomachhole{\bnwsym}\\
	(\lay(\la\varthreex)(xy))x & \esubx{(\symfont{I},\epsilon)} & \epsilon & \tomachhole{\seavsym}\\
	\lay(\la\varthreex)(xy) & \esubx{(\symfont{I},\epsilon)} & (\symfont{I},\epsilon) & \tomachhole{\bnwsym} \\
	(\la\varthreex)(xy) & \esuby{(\symfont{I},\epsilon)} \cdot \esubx{(\symfont{I},\epsilon)}=:e & \epsilon & \tomachhole{\seanvsym}\\
	\la\varthreex & \esubx{(\symfont{I},\epsilon)} & (xy,e) & \tomachhole{\bwsym}\\
	x & \esubx{(\symfont{I},\epsilon)} & \epsilon & \tomachhole{\subsym}\\
	\symfont{I} & \epsilon & \epsilon
	\end{array}
	\]
	Note that now the environment contains only closures bound to the free variables of the current term. Moreover, closures that will be never used, because the abstracted variable does not occur in the body of the abstraction, as simply deleted, such as $(xy,e)$ in the  $\tomachhole{\bwsym}$ transition. Finally, no chains that rename variables are present anymore. In the previous execution, on the KAM\xspace, there was one such chain, namely $(x,\esubx{(\symfont{I},\epsilon)})$, which now is just $(\symfont{I},\epsilon)$. From the quantitative point of view, note that the maximum space consumed during the execution is 4 pointers: in the third to last state, the closure in the stack contains $e$, which is itself an environment with two closures, as defined at the previous line.
\end{example}







\section{Capturing the Space KAM\xspace Low-Level Time}\label{sec:time}
\paragraph{Low-Level Time.} \citet{LICS2022} show that the Space KAM\xspace run on a closed 
term $t$ cannot be implemented on Turing machines with an overhead in time which 
is polynomial in the number $n$ of weak head reduction steps from $t$ (which is 
the natural cost model for time in Closed \cbn), nor in the number of Space KAM\xspace steps 
(which is linear in $n$). This is because of the lack of sharing of the Space KAM\xspace 
data structures. Indeed, in transitions $\tomachhole{\seanvsym}$ and $\tomachhole{\seanvsym}$ the 
environment, of a priori unbounded size, can be duplicated. Of course, this copy 
operation cannot take a constant amount of time, and---as \citet{LICS2022} 
shows---it can actually lead to an exponential overhead.


It is however possible to adopt another more low-level time measure, the \emph{real} implementation time, that is, the time actually taken by the Space KAM\xspace to run. One transition does not count anymore for one unit of time, but we have to take into account the amount of time needed to manage the involved data structures. Since we do not rest on any sharing mechanism, roughly the time consumed by any transition is proportional to the sizes of the involved states\footnote{Since we are interested in measure time up to a \emph{polynomial} overhead, we are allowed to make some simplifications. For example, in this case, we do not discuss about the size of the input pointers, because it can be absorbed in the polynomial overhead.}. Thus, in analogy to what we have done for space we define the low-level time consumption of the Space KAM\xspace in the following way.

\begin{definition}[Low-Level Run Time]
	Let $\rho:\compil{t_0}\mathrm{\Rew{SpKAM\xspace}}^*s$ be a Space KAM\xspace run. Then the low-level time consumption of the run $\rho$ is defined as follows:
	\[\lmt{\rho}:=\sum_{{\state'}\in\rho}\size{{\state'}}\]
\end{definition}
Although this low-level time measure can be exponential in the number of $\beta$-steps a term needs to normalize, we have the following reasonability result\footnote{Intuitively, reasonability holds because in the simulation of Turing machines (the reasonable reference model), i.e.\xspace in the execution of the encoding of Turing machines into the $\l$-calculus, the exponential gap does not show up.}. 
\begin{theorem}[\cite{LICS2022}, The Space KAM\xspace Is Reasonable for Low-Level Time]
	Closed CbN evaluation $\Rew{wh}$ and the low-level time of the Space KAM $\lmt{\cdot}$ provide a reasonable time cost model for the $\lambda$-calculus.
\end{theorem}


 \paragraph{The New Weighting System.} We now turn to the definition of a weighted type system that is able to capture the Space KAM\xspace low-level time. Actually, the type system is the same of section~\ref{sec:type-system}, what changes is just the weight assignment, that can be found in \reffig{typing-rules-time}. Essentially, all the $\max$ have been turned into sums. More precisely, one can observe that in every rule (except for $\textsc{T-none}$ and $\textsc{T-many}$), the weight $w$ of the conclusion with judgment $\tjudgw{\Gamma}{w}{t}{A}$ is exactly the sum of all the weights of the premises \emph{plus} $\size\Gamma$ and $\sizeA$, i.e.\xspace the size of the Space KAM\xspace state corresponding to the judgment in the conclusion. 

\paragraph{Soundness.} The proof of soundness proceeds exactly as the one in Section~\ref{sec:correctness}. This is why we report only the main ingredients, leaving the technical details to Appendix~\ref{app:time}. Also in this case we have to extend the type system to the machine components (in \reffig{typing-rules-time}), so that subject reduction/soundness is proved on states, rather than terms.

\begin{figure}[t]
	\[
	\begin{array}{c@{\hspace{1cm}}c@{\hspace{1cm}}c}
	\infer[\textsc{T-Var}]{\wtjudg{x:\mset{A}^k}{k+\size{A}}{x}{A}}{}
	&
	
	\infer[\textsc{T-}\lambda_\star]{\wtjudg{\Gamma}{\size\Gamma}{\lambdax.t}{\star}}{
		\dom\Gamma = \fv{\la\vart} & \Gamma \mbox{ is dry}}
	\\[10pt]
	\infer[\textsc{T-}\lambda_{1}]{\wtjudg{\Gamma}{w+\size\Gamma+\sizeA+k}{\lambdax.t}{\arr{\mathcal{A}^{k}}{A}}} 
	{\wtjudg{\Gamma,x:\mathcal{A}^{k}}{w}{t}{A}}
	&
	\infer[\textsc{T-}\lambda_{2}]{\wtjudg{\Gamma}{w+\size\Gamma+\sizeA+k}{\lambdax.t}{\arr{\mset{\,}^{k}}{A}}}
	{\wtjudg{\Gamma}{w}{t}{A} & x\notin\dom\Gamma}
	\\[10pt]
	\infer[\textsc{T-many}]{\wtjudg{\uplus_{i=1}^n\Gamma_i}{\sum_{i}\set{v_{i}}}{t}{\mset{A_1\mydotsA_n}^{1+\size{\uplus_{i=1}^n\Gamma_i}}}}
	{\wtjudg{\Gamma_i}{v_{i}}{t}{A_i} & 1\leq i\leq n & \#_i\Gamma_{i}}
	& \infer[\textsc{T-none}]{\wtjudg{\Gamma}{0}{t}{[\,]^{1+\size\Gamma}}}{\dom\Gamma = \fv{t} & \Gamma  \mbox{ is dry}}
	\\[10pt]
	
	\infer[\textsc{T-@}_{1}]{\wtjudg{\Gamma\uplus 
			\Delta}{w+v+\size{\Gamma\uplus\Delta}+\sizeA}{tu}{A 
	}}{\wtjudg{\Gamma}{w}{t}{\arr{\mathcal{A}^{k}}{A}}
		& 
		\wtjudg{\Delta}{v}{u}{\mathcal{A}^{k}}& \Gamma\# \Delta} 
	&
	







	%





	\infer[\textsc{T-@}_{2}]{\wtjudg{\Gamma\uplus
			x:\mathcal{A}^k  
		}{w+\size\Gamma+k+\sizeA}{tx}{A 
	}}{\wtjudg{\Gamma}{w}{t}{\arr{\mathcal{A}^k}{A}}
		&&\Gamma\#x:\mathcal{A}^k}
	\\\\
	\hline
	\\
	\infer[\textsc{T-env}]{\wtjudg{}{\sum\set{w_x|x\in\dome}}{e}{\Gamma}} 
	{\wtjudg{}{w_x}{e(x)}{\Gamma(x)}&&\forallx\in\dome}
	&
	\infer[\textsc{T-cl}]{\wtjudg{}{w+v}{(t,e)}{\mathcal{A}^{k}}}{ 
		\wtjudg{}{w}{e}{\Gamma} 
		&& 
		\wtjudg{\Gamma}{v}{t}{\mathcal{A}^{k}} }
	\\\\
	\multicolumn{2}{c}{
		\infer[\textsc{T-st}]{\wtjudg{}{w+u+\sum_i v_i}{\spkamstateteS}{\star}}{
			\wtjudg{\Gamma}{w}{t}{\arr{\mathcal{A}_1^{k_{1}}}{\arr{\cdots}{\arr{\mathcal{A}_n^{k_{n}}}{\star} } } } 
			&
			\wtjudg{}{u}{e}{\Gamma}
			&
			\wtjudg{}{v_i}{S_i}{\mathcal{A}_i^{k_{i}}} 
		}
	}
	\end{array}
	\]
	
	\caption{Typing rules for terms (above) and machine components (below).}
	\label{fig:typing-rules-time}
\end{figure}

\paragraph{Time Analysis of Final States.} We need an auxiliary lemma that allows us to prove that the weight system correctly measures the size of final states.

\begin{lemma}[The weight of final states is their low-level time]
	\label{l:weight-of-final-states-is-right-time}
	Let $s$ be a final state and $\pi\;\triangleright \tjudgw{}{w}{s}{\star}$. Then $w = \sizes$.
\end{lemma}
Then we able to state the soundness theorem, this time for the low-level time weighting system. 
\begin{theorem}[Low-Level Time Soundness]
	Let $s$ be a Space KAM\xspace reachable state such that there is a derivation $\pi\;\triangleright\tjudgw{}{w}{s}{\star}$. Then the run $\rho:s\mathrm{\Rew{SpKAM\xspace}}^*s_{f}$ to the final state is such that
	$w=\lmt\rho$\footnote{We have already proved the soundness of the type system w.r.t. termination, which does not depend on the weighting system. This is why termination is not part of the statement.}.	
\end{theorem}
\begin{proof}
	The proof is by induction on $\size\pi$ and case analysis on whether $s$ is final. If $s$ is final then the run $\rho$ in the statement is given by the empty run, containing only $s$. Therefore, we have $\lmt\rho = \sizes$ and the required time bound becomes $w= \sizes$, which is given by \reflemma{weight-of-final-states-is-right-time}. If $s$ is not final then $s\mathrm{\Rew{SpKAM\xspace}}{\state'}$. By examining all the transition rules. We set $A:=\arr{\mathcal{A}_1^{k_{1}}}{\arr{\cdots}{\arr{\mathcal{A}_n^{k_{n}}}{\star}}}$ and $S:=S_1\cdotsS_n$.
	
	We report just one case to illustrate the methodology, the ones can be found in Appendix~\ref{app:time}.
	
	Case $\tomachhole{\subsym}$, i.e.\xspace $s=\spkamstatex
		{\esubx{(u,e)}}S$ and
		${\state'}=\spkamstateueS$. The type derivation $\pi$ typing  $s$ has the following shape:
		\[
		\infer[\textsc{T-st}]{\wtjudg{}{k+\sizeA+u+w'+\sum_i v_i}{\spkamstatex
				{\esubx{(u,e)}}S}{\star}}{
			\infer[\textsc{T-Var}]{\wtjudg{x:\mset{A}^k}{k+\size{A}}{x}{A}}{} 
			&
			\infer[\textsc{T-env}]{\wtjudg{}{u+w'}{\esubx{(u,e)}}{x:\msetA^k}} {
				\infer[\textsc{T-cl}]{
					\wtjudg{}{u+w'}{(u,e)}{\msetA^k}
				}{
					\wtjudg{\Gamma}{w'}{u}{\msetA^k }
					&
					\wtjudg{}{u}{e}{\Gamma} 
				} 
			}
			&
			\wtjudg{}{v_i}{S_i}{\mathcal{A}_i^{k_{i}}} 
		}
		\]
		with $w = k+\sizeA+u+w'+\sum_i v_i$. The target state ${\state'}$ can be typed by the following derivation $\tyd'$:
		\[\tyd':=
		\infer[\textsc{T-st}]{\wtjudg{}{w'+u+\sum_i v_i}{\spkamstateueS}{\star}}{
			\wtjudg{\Gamma}{w'}{u}{A } 
			&
			\wtjudg{}{u}{e}{\Gamma}
			&
			\wtjudg{}{v_i}{S_i}{\mathcal{A}_i^{k_{i}}} 
		}
		\]
		Since the $\textsc{T-Var}$ rule is removed, we have $\size\pi>\size\tyd'$, and so we can apply the \textit{i.h.}\xspace, obtaining a run $\sigma: {\state'} \mathrm{\Rew{SpKAM\xspace}}^{*} s_{f}$ to a final state such that $w'+u+\sum_i v_i = \lmt\sigma$.
		
		For the time bound, note that $\lmt\rho = \sizes+\lmt\sigma=w$.
\end{proof}

As a corollary, we can transfer back the soundness result from typed \emph{states} to typed \emph{terms}.

\begin{corollary}[Low-Level Time Soundness, on Terms]
	Let $t$ be a closed $\lambda$-term. If there exists $\pi\;\triangleright\tjudgw{}{w}{t}{\star}$, then there exists a complete Space KAM\xspace run $\rho$ from $t$ such that $\lmt\rho=w$.
\end{corollary}

Putting together low-level time soundness and the completeness result of the previous section (which does not rests on the weighting system) one has the low-level time  correctness of the time variant of the closure type system.
\begin{theorem}[Low-Level Time Correctness]
	Let $t$ be a closed $\lambda$-term. Then there exists a complete Space KAM\xspace run $\rho$ from $t$ such that $\lmt\rho=w$ if and only if there exists $\pi\;\triangleright\tjudgw{}{w}{t}{\star}$.
\end{theorem}

\begin{example}
	For the sake of completeness, we provide the closure type derivation of our example term $(\lax(\lay(\la\varthreex)(xy))x)\symfont{I}$ decorated with our new weighting system, characterizing low-level time.
	\[
	\infer[\textsc{T-@}_1]{\tjudgw{}{11} {(\lax(\lay(\la\varthreex)(xy))x)\symfont{I}}{\star}}{
		\infer[\textsc{T-}\lambda_1]{\tjudgw{}{11}{\lax(\lay(\la\varthreex)(xy))x} {\arr{\mset\star^1}\star}}{
			\infer[\textsc{T-@}_2]{\tjudgw{x:\mset\star^1}{10}{(\lay(\la\varthreex)(xy))x}{\star}}{\infer[\textsc{T-}\lambda_1]{\tjudgw{x:\mset\star^1}{9}{\lay(\la\varthreex)(xy)} {\arr{[\,]^1}\star}}{
					\infer[\textsc{T-@}_1]{\tjudgw{x:\mset\star^1,y:[\,]^1}{7}{(\la\varthreex)(xy)}{\star}}{
						\infer[\textsc{T-}\lambda_2]{\tjudgw{x:\mset\star^1}{5}{\la\varthreex}{\arr{[\,]^3}\star}}{
							\infer[\textsc{T-Var}]{\tjudgw{x:\mset\star^1}{1}{x}{\star}}{}} & \infer[\textsc{T-none}]{\tjudgw{x:[\,]^1,y:[\,]^1}{0}{xy}{[\,]^3}}{}}}}} & \infer[\textsc{T-many}]{\tjudgw{}{0}{\symfont{I}}{\mset\star^1}}{
			\infer[\textsc{T-}\lambda_\star]{\tjudgw{}{0}{\symfont{I}}{\star}}{}}}
	\]
	The final weight, i.e.\xspace the low-level time of the evaluation on the Space KAM\xspace is 11. One could easily check that the same result holds if one looks directly at the  Space KAM\xspace execution.
\end{example}
\section{The Closure Type System}\label{sec:type-system}
Here we define our variant of multi types, dubbed \emph{closure types}, that we are going to use to measure the space consumption of (typable) terms. The definition of types is standard, but for the fact that multi-sets come labeled with an index $k$. The idea is that multi-sets of types are associated to arguments (according to the call-by-name translation of the $\lambda$-calculus into linear logic), and arguments give rise to closures (hence the name closure types): the index represent the size $\sizec$ of the closure $c$ (i.e.\xspace the number of pointers to implement it) that shall be associated to that argument/multi-set.
\[
	\begin{array}{rrcll}
		\textsc{Linear 
		Types}&A,\linty'&::=&\star\mathrel{\big |}\arr{\mathcal{A}^k}{A} 
		\\[3pt]
		\textsc{Closure 
		Types}&\mathcal{A}^k,\mathcal{B}^k&::=&\mset{A_1,\ldots,A_n}^k \qquad 
		k>0,n\geq 0
	\end{array}
\]

Type judgments, type environments, and type derivations are defined exactly as in the traditional multi type case. Please note that however some subtleties become apparent, regarding how labeled multi sets are handled. The empty multi-set is noted $[\,]^{k}$ and it also comes labeled with $k$. Note that $k$ has to be strictly positive. The sum $\uplus$ of multi-sets requires the two multi-sets to have the same index, that is, we have that $\mathcal{A}^{k}\uplus \mathcal{B}^{k} := (\mathcal{A}\uplus\mathcal{B})^{k}$, where on the right hand side we treat $\mathcal{A}$ and $\mathcal{B}$ as ordinary multi-sets, while $\mathcal{A}^{k}\uplus \mathcal{B}^{h}$ is undefined for $h\neq k$.

\paragraph{Space and Weakenings} The study of space requires an unusual approach 
to weakenings. In a weak evaluation setting, a judgment 
$\tjudg{\Gamma}{t}{A}$ usually implies only that $\dom\Gamma \subseteq \fvt$ 
and not necessarily that $\dom\Gamma = \fvt$, because there can be untyped free 
variables, that is, free variables occurring under abstraction that are not 
touched by weak evaluation and thus not typed. Indeed, given an abstraction 
$\la\vart$ with $\fv{\la\vart} \neq \emptyset$, usually one can type it with 
$\star$, deriving a judgment $\tjudg{}{\la\vart}{\star}$ with an 
\emph{empty} type context. Here this shall not be possible, because in the Space KAM\xspace 
the variables in $\fv{\la\vart}$ play a role in the space usage, as they forbid 
to garbage collect some closures. Therefore, we modify the type system as to 
enforce the property $\dom\Gamma = \fvt$, even if evaluation is weak, and this is 
done via an unusual use of weakenings. In particular, we distinguish between a 
variable $x\notin\dom\Gamma$ and a variable $\Gamma(x)=[\,]^{k_{x}}$ that 
gets assigned an empty multi-set. The intuition is that $x\notin\dom\Gamma$ means 
that $x$ does not appear in the term at all, and it would correspond to $x$ 
being typed with $[\,]^{0}$, which is however not a valid type because the 
index $k_{x}$ must be $>0$. Instead, $\Gamma(x)=[\,]^{k_{x}}$ means that 
$x$ appears but it is not going to be used, and it shall nonetheless have an 
associated closure of size $k_{x}$. We point out that also 
\citet{DBLP:journals/iandc/LengrandLDDB04} have studied intersection types in a 
calculus with explicit substitutions and a garbage collection rule.

We shall need a notion of type context assigning the empty multi-set (with a positive index) to all the variable in its domain.
\begin{definition}[Dry type contexts]
A type context $\Gamma$ is \emph{dry} if for every $x\in\dom\Gamma$, there 
exists $k_{x}$ such that $\Gamma(x)=[\,]^{k_{x}}$.
\end{definition}


\paragraph{Typing Rules.}
In order to define the typing rules we need two further notions.
First, we need a notion of size of types and type contexts.
\[
\begin{array}{c@{\hspace{2cm}}c@{\hspace{2cm}}c}
	\size{\star}:= 0 &
	\size{\arr{\mathcal{A}^k}A}:= k+\size{A}&
	\size{x:\mathcal{A}^k,\Gamma}:= k+\size{\Gamma}
\end{array}
\]
Note that for a type context one sums only the indices over the multi-sets, ignoring the size of linear types inside the multi-sets themselves.

To define the type system, we need a predicate over type environments to ensure that they are summable, because multi-sets sum is restricted to multi-sets having the same index.

\begin{definition}
	 Two type environments $\Gamma$ and $\Delta$ are \emph{summable}, noted $\Gamma\# \Delta$, if when $\Gamma(x) = \mathcal{A}^{k}$ and 
$\Delta(x) = \mathcal{B}^{h}$ then $k =h$, for all 
$x\in\dom\Gamma\cap\dom\Delta$. The notion can be naturally generalized to an 
arbitrary number of type environment $\Gamma_i$ as $\#_i\Gamma_i$.
\end{definition}

\begin{figure}[t]
	\[
	\begin{array}{c@{\hspace{1cm}}c@{\hspace{1cm}}c}
	\infer[\textsc{T-Var}]{\wtjudg{x:\mset{A}^k}{k+\size{A}}{x}{A}}{}
	&
	
	\infer[\textsc{T-}\lambda_\star]{\wtjudg{\Gamma}{\size{\Gamma}}{\lambdax.t}{\star}}{
		\dom\Gamma = \fv{\la\vart} & \Gamma \mbox{ is dry}}
	\\[10pt]
	\infer[\textsc{T-}\lambda_{1}]{\wtjudg{\Gamma}{w}{\lambdax.t}{\arr{\mathcal{A}^{k}}{A}}} 
	{\wtjudg{\Gamma,x:\mathcal{A}^{k}}{w}{t}{A}}
	&
	\infer[\textsc{T-}\lambda_{2}]{\wtjudg{\Gamma}{\max\{w,\size\Gamma+\sizeA+k\}}{\lambdax.t}{\arr{\mset{\,}^{k}}{A}}}
	{\wtjudg{\Gamma}{w}{t}{A} & x\notin\dom\Gamma}
	\\[10pt]
	\infer[\textsc{T-many}]{\wtjudg{\uplus_{i=1}^n\Gamma_i}{\max_{i}\set{v_{i}}}{t}{\mset{A_1\mydotsA_n}^{1+\size{\uplus_{i=1}^n\Gamma_i}}}}
	{\wtjudg{\Gamma_i}{v_{i}}{t}{A_i} & 1\leq i\leq n & \#_i\Gamma_{i}}
	& \infer[\textsc{T-none}]{\wtjudg{\Gamma}{0}{t}{[\,]^{1+\size\Gamma}}}{\dom\Gamma = \fv{t} & \Gamma  \mbox{ is dry}}
	\\[10pt]
	
	\infer[\textsc{T-@}_{1}]{\wtjudg{\Gamma\uplus 
			\Delta}{\max\{w,v\}}{tu}{A 
	}}{\wtjudg{\Gamma}{w}{t}{\arr{\mathcal{A}^{k}}{A}}
		& 
		\wtjudg{\Delta}{v}{u}{\mathcal{A}^{k}}& \Gamma\# \Delta} 
	&
	







	%





	\infer[\textsc{T-@}_{2}]{\wtjudg{\Gamma\uplus
			x:\mathcal{A}^k  
		}{w}{tx}{A 
	}}{\wtjudg{\Gamma}{w}{t}{\arr{\mathcal{A}^k}{A}}
		&&\Gamma\#x:\mathcal{A}^k}
	\end{array}
	\]
	
	\caption{The closure type system.}
	\label{fig:typing-rules}
\end{figure}

The typing rules are in \reffig{typing-rules}. For now, just ignore the weights. As in the case of the multi type system and of the KAM\xspace, we have crafted this system in such a way that given a type 
derivation $\pi$ for a term $t$, there is a one to one correspondence 
between the transitions used by the Space KAM\xspace run on $t$ and the occurrences of 
the typing rules (excluded $\textsc{T-many}$ and $\textsc{T-none}$) of $\pi$, plus the fact that $\textsc{T-}\lambda_\star$ is used to type final states. Namely, $\tomachhole{\seavsym}$ corresponds to $\textsc{T-@}_{2}$, $\tomachhole{\seanvsym}$ to $\textsc{T-@}_{1}$, $\tomachhole{\bnwsym}$  to $\textsc{T-}\lambda_{1}$, $\tomachhole{\bwsym}$  to $\textsc{T-}\lambda_{2}$, and $\tomachhole{\subsym}$ to $\textsc{T-Var}$. The intuition behind the closure types is that there is a correspondence between Space KAM\xspace data 
structures 
and the type theoretic side. The idea is that every closure type $\mathcal{A}^k$ 
corresponds to a closure $c$ such that $\sizec=k$. In particular, given 
a state $s = \spkamstate{t}{e}{S}$ and 
a judgment $\tjudg{\Gamma}{t}{A}$, the 
type environment $\Gamma\defeqx_1:\mathcal{A}^{k_1}\ldotsx_n:\mathcal{A}^{k_n}$ morally 
corresponds to the environment 
$e:=\esub{x_1}{c_1}\ldots\esub{x_n}{c_n}$ 
and moreover $\size{c_i}=k_i$ for each $1\leq i\leq n$. Similarly, 
there is a correspondence between the stack and the type $A$, namely  
$A:=\arr{\mathcal{A}_1^{k_{1}}}{\arr{\cdots}{\arr{\mathcal{A}_m^{k_{m}}}{\star}}}$ 
corresponds to the stack $S:=S_1\ldotsS_m$ and moreover 
$\size{S_i}=k_i$ for each $1\leq i\leq m$. Essentially, this means that we are able to read from the type derivation of a term $t$ the sizes of all the states reached by the Space KAM\xspace evaluating $t$. 

Rules $\textsc{T-many}$ and $\textsc{T-none}$ is where multi-sets are introduced on the right. In order to explain the index on the introduced multi-set, let us first consider $\textsc{T-none}$. The idea is that $t$ shall be paired by the machine with an environment $e$ as to form a closure $c = (t,e)$. By the invariant of the machine (\reflemma{spkam-invariants}), $\dome$ is exactly $\fvt$, that is, $e$ contains a closure for each variable $x$ in $\fvt$. Now, each such closure shall have size $k_{x}$, where $k_{x}$ is the index given to $[\,]$ by the dry context $\Gamma$. Therefore, $1+\size\Gamma$ shall correspond to $1+\sizee$, which is exactly the size of $c$.

For $\textsc{T-many}$, the reasoning is analogous. Let us explain a point about the 
quantity $\size{\uplus_{i=1}^n\Gamma_i}$ in its conclusion. An invariant 
(forthcoming \reflemma{tye-invariant}) shall guarantee that $\dom\Gamma = \fvt$, 
whenever $\tjudg{\Gamma}{t}{A}$. Then in $\textsc{T-many}$, the type contexts 
$\Gamma_{i}$ have all the same domain, and by the summable hypothesis, they all give 
the same index $k$ to the (potentially different) multi-sets $\Gamma_{i}(x)$ for 
a same variable $x$. Thus the various $\size{\Gamma_j}$ all coincide (for 
$j\in\set{1,\ldots,n}$) and also coincide with the quantity 
$\size{\uplus_{i=1}^n\Gamma_i}$ (so one could have as well decorated the conclusion 
of $\textsc{T-many}$ with the index $\size{\Gamma_1}$ rather than 
$\size{\uplus_{i=1}^n\Gamma_i}$, as they coincide).

Some of the rules of the type system seem to introduce some \emph{arbitrary} indices in the conclusions. Namely, rules $\textsc{T-Var}$ and $\textsc{T-}\lambda_{2}$ introduce an arbitrary $k>0$, and rules $\textsc{T-}\lambda_\star$ and $\textsc{T-none}$ refer to a dry $\Gamma$, and dryness only requires the indices to be different from $0$ but otherwise arbitrary. Two lemmas in the next section (\reflemma{env-clos-size} and \reflemma{space-bound-on-current-state}) shall however guarantee that, if the global derivation in which the rules occur types a closed term with $\star$, such arbitrary choices are in fact strongly constrained, to the point that the indices are actually \emph{uniquely} determined. 

We highlight the main differences w.r.t. the traditional multi type system.
\begin{itemize}
	\item \emph{Weakening.} As we have already observed, the approach to weakenings is slightly more liberal than in multi types. It is implicitly part of rules $\textsc{T-}\lambda_\star$, $\textsc{T-}\lambda_{2}$, and $\textsc{T-none}$. In rules $\textsc{T-}\lambda_\star$ and $\textsc{T-none}$, a context $\Gamma$ can be injected in the conclusion, but only if it is dry, and if its domain coincides with the free variables of the typed term. The situation at the level of the Space KAM\xspace for the rule $\textsc{T-}\lambda_\star$ corresponds to final states such as $\spkamstate{\laxy}{\esub\vartwot}{\epsilon}$. A closure is indeed present, hence the index $k>0$, although it will never be used, hence its type being the empty multi-set. In rule $\textsc{T-}\lambda_{2}$, which is not present in the multi type system (because transition $\tomachhole{\bwsym}$ is not a transition of the KAM\xspace), the variable $x$ that does not occur free in $t$ is intuitively typed with $[\,]^0$ in the premise in the rule. In the conclusion, however, a type $\arr{[\,]^0}{A}$ would not be correct, as the index cannot be $0$. Then the rule uses an arbitrary index $k>0$. The intuition is that  the Space KAM\xspace closure corresponding to $[\,]$, before being eliminated by rule $\tomachhole{\bwsym}$, has size strictly greater than zero.
	
	Please notice that all this consideration ensure the invariant for which for any judgment $\tjudg{\Gamma}{t}{A}$ or $\tjudg{\Gamma}{t}{\mathcal{A}^k}$ one has $\dom{\Gamma}=\fvt$.
	\item \emph{Separate multi-sets rules.} In the traditional multi types rules $\textsc{T-none}$ and $\textsc{T-many}$ are incorporated inside rule $\textsc{T-@}$. This was impossible to do in the closure type system because the rule $\textsc{T-none}$ was necessarily different from the rule $\textsc{T-many}$, and not just the special case when there are zero premises. This is because of the way we deal with weakenings: weakening is present just in the rule $\textsc{T-none}$, while there is not in rule $\textsc{T-many}$.
	
	Rules $\textsc{T-none}$ and $\textsc{T-many}$ correspond to the creation of closures. This why the index of the created multi-set is $1+\size\Gamma$. Morally, this corresponds to the closure $(t,e)$, where $t$ is the typed term and $e$ corresponds to $\Gamma$. Hence, we have $\size{(t,e)}=1+\sizee=1+\size\Gamma$.
	\item  \emph{Unchaining.} The type rule $\textsc{T-@}_{2}$ is the type theoretic equivalent of the Space KAM\xspace transition rule $\tomachhole{\seavsym}$, that implements the unchaining optimization. If one forgets the indices, the rule is just a specialization of the rule $\textsc{T-@}_{1}$, from which it can be derived (using also an instance of rule $\textsc{T-Var}$). The derived rule, however, would not have the right indices (because it corresponds to the KAM way of computing that does not unchain), which is why we need an additional rule.
	\item \emph{Coherence.} All the rules which sum type environments have to enforce the coherence relation $\#\Gamma_i$ between the type environments $\Gamma_i$ in the premises.
\end{itemize}

\paragraph{The Weight System.} The intuition behind the weight system is very simple. The weight of the type derivation $\pi$ ending in $\tjudg{}t\star$ should correspond to the space consumed by the complete run $\rho$ of the Space KAM\xspace starting from $t$. We know how to  read the size of a Space KAM\xspace state $s= \spkamstate{t}{e}{S}$ belonging to $\rho$ out of the corresponding to type judgment $\tjudg{\Gamma}{t}{A}$ belonging to $\pi$: simply $\sizes=\size\Gamma+\sizeA$. Then, the space consumed by $\rho$ is the maximum of the sizes of all the type judgments occurring in $\pi$. This is exactly what the weighting system is keeping trace of.

\begin{example}
	We provide the closure type derivation of our example term $(\lax(\lay(\la\varthreex)(xy))x)\symfont{I}$.
	\[
	\infer[\textsc{T-@}_1]{\tjudgw{}{4} {(\lax(\lay(\la\varthreex)(xy))x)\symfont{I}}{\star}}{
		\infer[\textsc{T-}\lambda_1]{\tjudgw{}{4}{\lax(\lay(\la\varthreex)(xy))x} {\arr{\mset\star^1}\star}}{
			\infer[\textsc{T-@}_2]{\tjudgw{x:\mset\star^1}{4}{(\lay(\la\varthreex)(xy))x}{\star}}{\infer[\textsc{T-}\lambda_1]{\tjudgw{x:\mset\star^1}{4}{\lay(\la\varthreex)(xy)} {\arr{[\,]^1}\star}}{
					\infer[\textsc{T-@}_1]{\tjudgw{x:\mset\star^1,y:[\,]^1}{4}{(\la\varthreex)(xy)}{\star}}{
						\infer[\textsc{T-}\lambda_2]{\tjudgw{x:\mset\star^1}{4}{\la\varthreex}{\arr{[\,]^3}\star}}{
							\infer[\textsc{T-Var}]{\tjudgw{x:\mset\star^1}{1}{x}{\star}}{}} & \infer[\textsc{T-none}]{\tjudgw{x:[\,]^1,y:[\,]^1}{0}{xy}{[\,]^3}}{}}}}} & \infer[\textsc{T-many}]{\tjudgw{}{0}{\symfont{I}}{\mset\star^1}}{
								\infer[\textsc{T-}\lambda_\star]{\tjudgw{}{0}{\symfont{I}}{\star}}{}}}
	\]
	Also in this case, we can observe the precise correspondence between this type derivation and the execution of the Space KAM\xspace. Not only rules and transitions are into a one-to-one correspondence, but also stack and environment entries (with their sizes) can be seen, respectively, in types and in type environments. Of course, as a consequence, the final weight is 4, as the space consumption of the Space KAM\xspace execution. 
\end{example}

