diff options
| -rw-r--r-- | sec/lang.ltx | 43 |
1 files changed, 22 insertions, 21 deletions
diff --git a/sec/lang.ltx b/sec/lang.ltx index 689a9bf..a3d2cb7 100644 --- a/sec/lang.ltx +++ b/sec/lang.ltx @@ -18,13 +18,13 @@ \end{prooftree} \quad \begin{prooftree} - \hypo{\rangeover{\jdgmnt{ty}{\Psi}{A_i}}{i}} - \infer1{\jdgmnt{ty}{\Psi}{\prod_i A_i}} + \hypo{\rangeover{\jdgmnt{ty}{\Psi}{A_\ell}}{\ell}} + \infer1{\jdgmnt{ty}{\Psi}{\prod_{\ell \in I} A_\ell}} \end{prooftree} \quad \begin{prooftree} - \hypo{\rangeover{\jdgmnt{ty}{\Psi}{A_i}}{i}} - \infer1{\jdgmnt{ty}{\Psi}{\sum_i A_i}} + \hypo{\rangeover{\jdgmnt{ty}{\Psi}{A_\ell}}{\ell}} + \infer1{\jdgmnt{ty}{\Psi}{\sum_{\ell \in I} A_\ell}} \end{prooftree} \quad \begin{prooftree} @@ -38,8 +38,9 @@ In this section we introduce \lang{}, a simply-typed lambda calculus with \emph{regular types}. \Cref{fig:artist-wf} shows the well-formedness judgement for types, where \(\jdgmnt{ty}{\Psi}{A}\) means -that \(A\) is a type using variables from \(\Psi\). Types satisfy the -following substitution lemma: +that \(A\) is a type using variables from \(\Psi\). We have labelled +\(n\)-ary products and sums, where the set of labels is finite. Types +satisfy the following substitution lemma: \begin{proposition}[Type substitution] For any type \(A\) such that \(\jdgmnt{ty}{\Psi}{A}\) and any type environment \(\alpha\) that assigns each variable \(X \in \Psi\) to a type @@ -63,7 +64,7 @@ claim the type unrepresentable in some models of System~T}. \begin{figure} \[ - \begin{array}{cccc} + \begin{array}{ccc} \begin{prooftree} \hypo{x : A \in \Gamma} \infer1{\judgement{\Gamma}{x}{A}} @@ -79,40 +80,40 @@ claim the type unrepresentable in some models of System~T}. \hypo{\judgement{\Gamma}{t}{A}} \infer2{\judgement{\Gamma}{f~t}{B}} \end{prooftree} - & + \\\\ \begin{prooftree} \hypo{\judgement{\Gamma}{t}{A}} \hypo{\judgement{\Gamma, x : A}{u}{B}} \infer2{\judgement{\Gamma}{\lettm{t}{x}{u}}{B}} \end{prooftree} - \\\\ + & \begin{prooftree} - \hypo{\rangeover{\judgement{\Gamma}{t_i}{A_i}}{i}} - \infer1{\judgement{\Gamma}{\tuple{\rangeover{t_i}{i}}}{\prod_i A_i}} + \hypo{\rangeover{\judgement{\Gamma}{t_\ell}{A_\ell}}{\ell}} + \infer1{\judgement{\Gamma}{\tuple{\rangeover{\ell: t_\ell}{\ell}}}{\prod_{\ell \in I} A_\ell}} \end{prooftree} & \begin{prooftree} - \hypo{\judgement{\Gamma}{t}{\prod_i A_i}} - \infer1{\judgement{\Gamma}{t.i}{A_i}} + \hypo{\judgement{\Gamma}{t}{\prod_{\ell \in I} A_\ell}} + \infer1{\judgement{\Gamma}{t.\hat{\ell}}{A_{\hat{\ell}}}} \end{prooftree} - & + \\\\ \begin{prooftree} - \hypo{\judgement{\Gamma}{t}{A_i}} - \infer1{\judgement{\Gamma}{\tuple{i, t}}{\sum_i A_i}} + \hypo{\judgement{\Gamma}{t}{A_{\hat{\ell}}}} + \infer1{\judgement{\Gamma}{\hat{\ell}~t}{\sum_{\ell \in I} A_\ell}} \end{prooftree} & + \multicolumn{2}{c}{ \begin{prooftree} - \hypo{\judgement{\Gamma}{t}{\sum_i A_i}} - \hypo{\rangeover{\judgement{\Gamma, x_i : A_i}{t_i}{B}}{i}} - \infer2{\judgement{\Gamma}{\casetm{t}{\tuple{i,x_i}}{t_i}{i}}{B}} + \hypo{\judgement{\Gamma}{t}{\sum_{\ell \in I} A_\ell}} + \hypo{\rangeover{\judgement{\Gamma, x_\ell : A_\ell}{t_\ell}{B}}{\ell}} + \infer2{\judgement{\Gamma}{\casetm{t}{\ell~x_\ell}{t_\ell}{\ell}}{B}} \end{prooftree} + } \\\\ - \multicolumn{2}{c}{ \begin{prooftree} \hypo{\judgement{\Gamma}{t}{\sub{A}{X/\mu X. A}}} \infer1{\judgement{\Gamma}{\roll~t}{\mu X. A}} \end{prooftree} - } & \multicolumn{2}{c}{ \begin{prooftree} |