diff options
| -rw-r--r-- | thesis.lagda | 410 |
1 files changed, 252 insertions, 158 deletions
diff --git a/thesis.lagda b/thesis.lagda index fa18087..3dcd9a9 100644 --- a/thesis.lagda +++ b/thesis.lagda @@ -174,6 +174,7 @@ \newcommand{\myprsyn}{\myse{prop}} \newcommand{\myprdec}[1]{\mathopen{\mytyc{$\llbracket$}} #1 \mathopen{\mytyc{$\rrbracket$}}} \newcommand{\myand}{\mathrel{\mytyc{$\wedge$}}} +\newcommand{\mybigand}{\mathrel{\mytyc{$\bigwedge$}}} \newcommand{\myprfora}[3]{\forall #1 {:} #2. #3} \newcommand{\myimpl}{\mathrel{\mytyc{$\Rightarrow$}}} \newcommand{\mybot}{\mytyc{$\bot$}} @@ -2119,142 +2120,6 @@ checking the type, and updating the context with a new typed variable: \subsubsection{User defined types} \label{sec:user-type} -\begin{figure}[p] - \begin{subfigure}[b]{\textwidth} - \vspace{-1cm} - \mydesc{syntax}{ }{ - \footnotesize - $ - \begin{array}{l} - \mynamesyn ::= \cdots \mysynsep \mytyc{D} \mysynsep \mytyc{D}.\mydc{c} \mysynsep \mytyc{D}.\myfun{f} - \end{array} - $ - } - - \mydesc{syntax elaboration:}{\mydeclsyn \myelabf \mytmsyn ::= \cdots}{ - \footnotesize - $ - \begin{array}{r@{\ }l} - & \myadt{\mytyc{D}}{\mytele}{}{\cdots\ |\ \mydc{c}_n : \mytele_n } \\ - \myelabf & - - \begin{array}{r@{\ }c@{\ }l} - \mytmsyn & ::= & \cdots \mysynsep \myapp{\mytyc{D}}{\mytmsyn^{\mytele}} \mysynsep \cdots \mysynsep - \mytyc{D}.\mydc{c}_n \myappsp \mytmsyn^{\mytele_n} \mysynsep \mytyc{D}.\myfun{elim} \myappsp \mytmsyn \\ - \end{array} - \end{array} - $ - } - - \mydesc{context elaboration:}{\myelab{\mydeclsyn}{\myctx}}{ - \footnotesize - - \AxiomC{$ - \begin{array}{c} - \myinf{\mytele \myarr \mytyp}{\mytyp}\hspace{0.8cm} - \mytyc{D} \not\in \myctx \\ - \myinff{\myctx;\ \mytyc{D} : \mytele \myarr \mytyp}{\mytele \mycc \mytele_i \myarr \myapp{\mytyc{D}}{\mytelee}}{\mytyp}\ \ \ (1 \leq i \leq n) \\ - \text{For each $(\myb{x} {:} \mytya)$ in each $\mytele_i$, if $\mytyc{D} \in \mytya$, then $\mytya = \myapp{\mytyc{D}}{\vec{\mytmt}}$.} - \end{array} - $} - \UnaryInfC{$ - \begin{array}{r@{\ }c@{\ }l} - \myctx & \myelabt & \myadt{\mytyc{D}}{\mytele}{}{ \cdots \ |\ \mydc{c}_n : \mytele_n } \\ - & & \vspace{-0.2cm} \\ - & \myelabf & \myctx;\ \mytyc{D} : \mytele \myarr \mytyp;\ \cdots;\ \mytyc{D}.\mydc{c}_n : \mytele \mycc \mytele_n \myarr \myapp{\mytyc{D}}{\mytelee}; \\ - & & - \begin{array}{@{}r@{\ }l l} - \mytyc{D}.\myfun{elim} : & \mytele \myarr (\myb{x} {:} \myapp{\mytyc{D}}{\mytelee}) \myarr & \textbf{target} \\ - & (\myb{P} {:} \myapp{\mytyc{D}}{\mytelee} \myarr \mytyp) \myarr & \textbf{motive} \\ - & \left. - \begin{array}{@{}l} - \myind{3} \vdots \\ - (\mytele_n \mycc \myhyps(\myb{P}, \mytele_n) \myarr \myapp{\myb{P}}{(\myapp{\mytyc{D}.\mydc{c}_n}{\mytelee_n})}) \myarr - \end{array} \right \} - & \textbf{methods} \\ - & \myapp{\myb{P}}{\myb{x}} & - \end{array} - \end{array} - $} - \DisplayProof \\ \vspace{0.2cm}\ \\ - $ - \begin{array}{@{}l l@{\ } l@{} r c l} - \textbf{where} & \myhyps(\myb{P}, & \myemptytele &) & \mymetagoes & \myemptytele \\ - & \myhyps(\myb{P}, & (\myb{r} {:} \myapp{\mytyc{D}}{\vec{\mytmt}}) \mycc \mytele &) & \mymetagoes & (\myb{r'} {:} \myapp{\myb{P}}{\myb{r}}) \mycc \myhyps(\myb{P}, \mytele) \\ - & \myhyps(\myb{P}, & (\myb{x} {:} \mytya) \mycc \mytele & ) & \mymetagoes & \myhyps(\myb{P}, \mytele) - \end{array} - $ - - } - - \mydesc{reduction elaboration:}{\mydeclsyn \myelabf \myctx \vdash \mytmsyn \myred \mytmsyn}{ - \footnotesize - $\myadt{\mytyc{D}}{\mytele}{}{ \cdots \ |\ \mydc{c}_n : \mytele_n } \ \ \myelabf$ - \AxiomC{$\mytyc{D} : \mytele \myarr \mytyp \in \myctx$} - \AxiomC{$\mytyc{D}.\mydc{c}_i : \mytele;\mytele_i \myarr \myapp{\mytyc{D}}{\mytelee} \in \myctx$} - \BinaryInfC{$ - \myctx \vdash \myapp{\myapp{\myapp{\mytyc{D}.\myfun{elim}}{(\myapp{\mytyc{D}.\mydc{c}_i}{\vec{\myse{t}}})}}{\myse{P}}}{\vec{\myse{m}}} \myred \myapp{\myapp{\myse{m}_i}{\vec{\mytmt}}}{\myrecs(\myse{P}, \vec{m}, \mytele_i)} - $} - \DisplayProof \\ \vspace{0.2cm}\ \\ - $ - \begin{array}{@{}l l@{\ } l@{} r c l} - \textbf{where} & \myrecs(\myse{P}, \vec{m}, & \myemptytele &) & \mymetagoes & \myemptytele \\ - & \myrecs(\myse{P}, \vec{m}, & (\myb{r} {:} \myapp{\mytyc{D}}{\vec{A}}); \mytele & ) & \mymetagoes & (\mytyc{D}.\myfun{elim} \myappsp \myb{r} \myappsp \myse{P} \myappsp \vec{m}); \myrecs(\myse{P}, \vec{m}, \mytele) \\ - & \myrecs(\myse{P}, \vec{m}, & (\myb{x} {:} \mytya); \mytele &) & \mymetagoes & \myrecs(\myse{P}, \vec{m}, \mytele) - \end{array} - $ - } - \end{subfigure} - - \begin{subfigure}[b]{\textwidth} - \mydesc{syntax elaboration:}{\myelab{\mydeclsyn}{\mytmsyn ::= \cdots}}{ - \footnotesize - $ - \begin{array}{r@{\ }c@{\ }l} - \myctx & \myelabt & \myreco{\mytyc{D}}{\mytele}{}{ \cdots, \myfun{f}_n : \myse{F}_n } \\ - & \myelabf & - - \begin{array}{r@{\ }c@{\ }l} - \mytmsyn & ::= & \cdots \mysynsep \myapp{\mytyc{D}}{\mytmsyn^{\mytele}} \mysynsep \mytyc{D}.\mydc{constr} \myappsp \mytmsyn^{n} \mysynsep \cdots \mysynsep \mytyc{D}.\myfun{f}_n \myappsp \mytmsyn \\ - \end{array} - \end{array} - $ -} - - -\mydesc{context elaboration:}{\myelab{\mydeclsyn}{\myctx}}{ - \footnotesize - \AxiomC{$ - \begin{array}{c} - \myinf{\mytele \myarr \mytyp}{\mytyp}\hspace{0.8cm} - \mytyc{D} \not\in \myctx \\ - \myinff{\myctx; \mytele; (\myb{f}_j : \myse{F}_j)_{j=1}^{i - 1}}{F_i}{\mytyp} \myind{3} (1 \le i \le n) - \end{array} - $} - \UnaryInfC{$ - \begin{array}{r@{\ }c@{\ }l} - \myctx & \myelabt & \myreco{\mytyc{D}}{\mytele}{}{ \cdots, \myfun{f}_n : \myse{F}_n } \\ - & & \vspace{-0.2cm} \\ - & \myelabf & \myctx;\ \mytyc{D} : \mytele \myarr \mytyp;\ \cdots;\ \mytyc{D}.\myfun{f}_n : \mytele \myarr (\myb{x} {:} \myapp{\mytyc{D}}{\mytelee}) \myarr \mysub{\myse{F}_n}{\myb{f}_i}{\myapp{\myfun{f}_i}{\myb{x}}}_{i = 1}^{n-1}; \\ - & & \mytyc{D}.\mydc{constr} : \mytele \myarr \myse{F}_1 \myarr \cdots \myarr \myse{F}_n \myarr \myapp{\mytyc{D}}{\mytelee}; - \end{array} - $} - \DisplayProof -} - - \mydesc{reduction elaboration:}{\mydeclsyn \myelabf \myctx \vdash \mytmsyn \myred \mytmsyn}{ - \footnotesize - $\myreco{\mytyc{D}}{\mytele}{}{ \cdots, \myfun{f}_n : \myse{F}_n } \ \ \myelabf$ - \AxiomC{$\mytyc{D} \in \myctx$} - \UnaryInfC{$\myctx \vdash \myapp{\mytyc{D}.\myfun{f}_i}{(\mytyc{D}.\mydc{constr} \myappsp \vec{t})} \myred t_i$} - \DisplayProof - } - - \end{subfigure} - \caption{Elaboration for data types and records.} - \label{fig:elab} -\end{figure} - Elaborating user defined types is the real effort. First, let's explain what we can defined, with some examples. @@ -2478,6 +2343,142 @@ what we can defined, with some examples. What we have is equivalent to ITT's dependent products. \end{description} +\begin{figure}[p] + \begin{subfigure}[b]{\textwidth} + \vspace{-1cm} + \mydesc{syntax}{ }{ + \footnotesize + $ + \begin{array}{l} + \mynamesyn ::= \cdots \mysynsep \mytyc{D} \mysynsep \mytyc{D}.\mydc{c} \mysynsep \mytyc{D}.\myfun{f} + \end{array} + $ + } + + \mydesc{syntax elaboration:}{\mydeclsyn \myelabf \mytmsyn ::= \cdots}{ + \footnotesize + $ + \begin{array}{r@{\ }l} + & \myadt{\mytyc{D}}{\mytele}{}{\cdots\ |\ \mydc{c}_n : \mytele_n } \\ + \myelabf & + + \begin{array}{r@{\ }c@{\ }l} + \mytmsyn & ::= & \cdots \mysynsep \myapp{\mytyc{D}}{\mytmsyn^{\mytele}} \mysynsep \cdots \mysynsep + \mytyc{D}.\mydc{c}_n \myappsp \mytmsyn^{\mytele_n} \mysynsep \mytyc{D}.\myfun{elim} \myappsp \mytmsyn \\ + \end{array} + \end{array} + $ + } + + \mydesc{context elaboration:}{\myelab{\mydeclsyn}{\myctx}}{ + \footnotesize + + \AxiomC{$ + \begin{array}{c} + \myinf{\mytele \myarr \mytyp}{\mytyp}\hspace{0.8cm} + \mytyc{D} \not\in \myctx \\ + \myinff{\myctx;\ \mytyc{D} : \mytele \myarr \mytyp}{\mytele \mycc \mytele_i \myarr \myapp{\mytyc{D}}{\mytelee}}{\mytyp}\ \ \ (1 \leq i \leq n) \\ + \text{For each $(\myb{x} {:} \mytya)$ in each $\mytele_i$, if $\mytyc{D} \in \mytya$, then $\mytya = \myapp{\mytyc{D}}{\vec{\mytmt}}$.} + \end{array} + $} + \UnaryInfC{$ + \begin{array}{r@{\ }c@{\ }l} + \myctx & \myelabt & \myadt{\mytyc{D}}{\mytele}{}{ \cdots \ |\ \mydc{c}_n : \mytele_n } \\ + & & \vspace{-0.2cm} \\ + & \myelabf & \myctx;\ \mytyc{D} : \mytele \myarr \mytyp;\ \cdots;\ \mytyc{D}.\mydc{c}_n : \mytele \mycc \mytele_n \myarr \myapp{\mytyc{D}}{\mytelee}; \\ + & & + \begin{array}{@{}r@{\ }l l} + \mytyc{D}.\myfun{elim} : & \mytele \myarr (\myb{x} {:} \myapp{\mytyc{D}}{\mytelee}) \myarr & \textbf{target} \\ + & (\myb{P} {:} \myapp{\mytyc{D}}{\mytelee} \myarr \mytyp) \myarr & \textbf{motive} \\ + & \left. + \begin{array}{@{}l} + \myind{3} \vdots \\ + (\mytele_n \mycc \myhyps(\myb{P}, \mytele_n) \myarr \myapp{\myb{P}}{(\myapp{\mytyc{D}.\mydc{c}_n}{\mytelee_n})}) \myarr + \end{array} \right \} + & \textbf{methods} \\ + & \myapp{\myb{P}}{\myb{x}} & + \end{array} + \end{array} + $} + \DisplayProof \\ \vspace{0.2cm}\ \\ + $ + \begin{array}{@{}l l@{\ } l@{} r c l} + \textbf{where} & \myhyps(\myb{P}, & \myemptytele &) & \mymetagoes & \myemptytele \\ + & \myhyps(\myb{P}, & (\myb{r} {:} \myapp{\mytyc{D}}{\vec{\mytmt}}) \mycc \mytele &) & \mymetagoes & (\myb{r'} {:} \myapp{\myb{P}}{\myb{r}}) \mycc \myhyps(\myb{P}, \mytele) \\ + & \myhyps(\myb{P}, & (\myb{x} {:} \mytya) \mycc \mytele & ) & \mymetagoes & \myhyps(\myb{P}, \mytele) + \end{array} + $ + + } + + \mydesc{reduction elaboration:}{\mydeclsyn \myelabf \myctx \vdash \mytmsyn \myred \mytmsyn}{ + \footnotesize + $\myadt{\mytyc{D}}{\mytele}{}{ \cdots \ |\ \mydc{c}_n : \mytele_n } \ \ \myelabf$ + \AxiomC{$\mytyc{D} : \mytele \myarr \mytyp \in \myctx$} + \AxiomC{$\mytyc{D}.\mydc{c}_i : \mytele;\mytele_i \myarr \myapp{\mytyc{D}}{\mytelee} \in \myctx$} + \BinaryInfC{$ + \myctx \vdash \myapp{\myapp{\myapp{\mytyc{D}.\myfun{elim}}{(\myapp{\mytyc{D}.\mydc{c}_i}{\vec{\myse{t}}})}}{\myse{P}}}{\vec{\myse{m}}} \myred \myapp{\myapp{\myse{m}_i}{\vec{\mytmt}}}{\myrecs(\myse{P}, \vec{m}, \mytele_i)} + $} + \DisplayProof \\ \vspace{0.2cm}\ \\ + $ + \begin{array}{@{}l l@{\ } l@{} r c l} + \textbf{where} & \myrecs(\myse{P}, \vec{m}, & \myemptytele &) & \mymetagoes & \myemptytele \\ + & \myrecs(\myse{P}, \vec{m}, & (\myb{r} {:} \myapp{\mytyc{D}}{\vec{A}}); \mytele & ) & \mymetagoes & (\mytyc{D}.\myfun{elim} \myappsp \myb{r} \myappsp \myse{P} \myappsp \vec{m}); \myrecs(\myse{P}, \vec{m}, \mytele) \\ + & \myrecs(\myse{P}, \vec{m}, & (\myb{x} {:} \mytya); \mytele &) & \mymetagoes & \myrecs(\myse{P}, \vec{m}, \mytele) + \end{array} + $ + } + \end{subfigure} + + \begin{subfigure}[b]{\textwidth} + \mydesc{syntax elaboration:}{\myelab{\mydeclsyn}{\mytmsyn ::= \cdots}}{ + \footnotesize + $ + \begin{array}{r@{\ }c@{\ }l} + \myctx & \myelabt & \myreco{\mytyc{D}}{\mytele}{}{ \cdots, \myfun{f}_n : \myse{F}_n } \\ + & \myelabf & + + \begin{array}{r@{\ }c@{\ }l} + \mytmsyn & ::= & \cdots \mysynsep \myapp{\mytyc{D}}{\mytmsyn^{\mytele}} \mysynsep \mytyc{D}.\mydc{constr} \myappsp \mytmsyn^{n} \mysynsep \cdots \mysynsep \mytyc{D}.\myfun{f}_n \myappsp \mytmsyn \\ + \end{array} + \end{array} + $ +} + + +\mydesc{context elaboration:}{\myelab{\mydeclsyn}{\myctx}}{ + \footnotesize + \AxiomC{$ + \begin{array}{c} + \myinf{\mytele \myarr \mytyp}{\mytyp}\hspace{0.8cm} + \mytyc{D} \not\in \myctx \\ + \myinff{\myctx; \mytele; (\myb{f}_j : \myse{F}_j)_{j=1}^{i - 1}}{F_i}{\mytyp} \myind{3} (1 \le i \le n) + \end{array} + $} + \UnaryInfC{$ + \begin{array}{r@{\ }c@{\ }l} + \myctx & \myelabt & \myreco{\mytyc{D}}{\mytele}{}{ \cdots, \myfun{f}_n : \myse{F}_n } \\ + & & \vspace{-0.2cm} \\ + & \myelabf & \myctx;\ \mytyc{D} : \mytele \myarr \mytyp;\ \cdots;\ \mytyc{D}.\myfun{f}_n : \mytele \myarr (\myb{x} {:} \myapp{\mytyc{D}}{\mytelee}) \myarr \mysub{\myse{F}_n}{\myb{f}_i}{\myapp{\myfun{f}_i}{\myb{x}}}_{i = 1}^{n-1}; \\ + & & \mytyc{D}.\mydc{constr} : \mytele \myarr \myse{F}_1 \myarr \cdots \myarr \myse{F}_n \myarr \myapp{\mytyc{D}}{\mytelee}; + \end{array} + $} + \DisplayProof +} + + \mydesc{reduction elaboration:}{\mydeclsyn \myelabf \myctx \vdash \mytmsyn \myred \mytmsyn}{ + \footnotesize + $\myreco{\mytyc{D}}{\mytele}{}{ \cdots, \myfun{f}_n : \myse{F}_n } \ \ \myelabf$ + \AxiomC{$\mytyc{D} \in \myctx$} + \UnaryInfC{$\myctx \vdash \myapp{\mytyc{D}.\myfun{f}_i}{(\mytyc{D}.\mydc{constr} \myappsp \vec{t})} \myred t_i$} + \DisplayProof + } + + \end{subfigure} + \caption{Elaboration for data types and records.} + \label{fig:elab} +\end{figure} + Following the intuition given by the examples, the mechanised elaboration is presented in figure \ref{fig:elab}, which is essentially a modification of figure 9 of \citep{McBride2004}\footnote{However, our @@ -2527,7 +2528,7 @@ instantiate when due: \DisplayProof } -\subsubsection{Why user defined types?} +\subsubsection{Why user defined types? Why eliminators?} % TODO reference levitated theories, indexed containers @@ -2681,7 +2682,9 @@ least than $n$ elements. Then we can define propositions, and decoding: It is worth to ask if $\myprop$ is needed at all. It is perfectly possible to have the type checker identify propositional types automatically, and in fact that is what The author initially planned to -identify the propositional fragment iinternally \cite{Jacobs1994}. +identify the propositional fragment internally \cite{Jacobs1994}. + +% TODO finish \subsubsection{OTT constructs} @@ -2769,6 +2772,8 @@ equalities. \]} Finally, quotation % TODO quotation + + \end{description} @@ -2784,15 +2789,76 @@ equalities. $ } +\begin{figure}[p] +\mydesc{typing:}{\myctx \vdash \myprsyn \myred \myprsyn}{ + \footnotesize + \begin{tabular}{cc} + \AxiomC{$\myjud{\myse{P}}{\myprdec{\mytya \myeq \mytyb}}$} + \AxiomC{$\myjud{\mytmt}{\mytya}$} + \BinaryInfC{$\myjud{\mycoee{\mytya}{\mytyb}{\myse{P}}{\mytmt}}{\mytyb}$} + \DisplayProof + & + \AxiomC{$\myjud{\myse{P}}{\myprdec{\mytya \myeq \mytyb}}$} + \AxiomC{$\myjud{\mytmt}{\mytya}$} + \BinaryInfC{$\myjud{\mycohh{\mytya}{\mytyb}{\myse{P}}{\mytmt}}{\myprdec{\myjm{\mytmt}{\mytya}{\mycoee{\mytya}{\mytyb}{\myse{P}}{\mytmt}}{\mytyb}}}$} + \DisplayProof + \end{tabular} +} +\mydesc{propositions:}{\myjud{\myprsyn}{\myprop}}{ + \footnotesize + \begin{tabular}{cc} + \AxiomC{\phantom{$\myjud{\myse{P}}{\myprop}$}} + \UnaryInfC{$\myjud{\mytop}{\myprop}$} + \noLine + \UnaryInfC{$\myjud{\mybot}{\myprop}$} + \DisplayProof + & + \AxiomC{$\myjud{\myse{P}}{\myprop}$} + \AxiomC{$\myjud{\myse{Q}}{\myprop}$} + \BinaryInfC{$\myjud{\myse{P} \myand \myse{Q}}{\myprop}$} + \noLine + \UnaryInfC{\phantom{$\myjud{\mybot}{\myprop}$}} + \DisplayProof + \end{tabular} + + \myderivsp + + \begin{tabular}{cc} + \AxiomC{$ + \begin{array}{@{}c} + \phantom{\myjud{\myse{A}}{\mytyp} \hspace{0.8cm} \myjud{\mytmm}{\myse{A}}} \\ + \myjud{\myse{A}}{\mytyp}\hspace{0.8cm} + \myjudd{\myctx; \myb{x} : \mytya}{\myse{P}}{\myprop} + \end{array} + $} + \UnaryInfC{$\myjud{\myprfora{\myb{x}}{\mytya}{\myse{P}}}{\myprop}$} + \DisplayProof + & + \AxiomC{$ + \begin{array}{c} + \myjud{\myse{A}}{\mytyp} \hspace{0.8cm} \myjud{\mytmm}{\myse{A}} \\ + \myjud{\myse{B}}{\mytyp} \hspace{0.8cm} \myjud{\mytmn}{\myse{B}} + \end{array} + $} + \UnaryInfC{$\myjud{\myjm{\mytmm}{\myse{A}}{\mytmn}{\myse{B}}}{\myprop}$} + \DisplayProof + \end{tabular} +} + % TODO equality for decodings \mydesc{equality reduction:}{\myctx \vdash \myprsyn \myred \myprsyn}{ \footnotesize + \AxiomC{} + \UnaryInfC{$\myctx \vdash \myjm{\mytyp}{\mytyp}{\mytyp}{\mytyp} \myred \mytop$} + \DisplayProof + + \myderivsp + \AxiomC{} \UnaryInfC{$ - \begin{array}{r@{\ }l} + \begin{array}{@{}r@{\ }l} \myctx \vdash & \myjm{\myfora{\myb{x_1}}{\mytya_1}{\mytyb_1}}{\mytyp}{\myfora{\myb{x_2}}{\mytya_2}{\mytyb_2}}{\mytyp} \myred \\ - & \myind{2} \mytya_2 \myeq \mytya_1 \myand \\ - & \myind{2} \myprfora{\myb{x_2}}{\mytya_2}{\myprfora{\myb{x_1}}{\mytya_1}{ + & \myind{2} \mytya_2 \myeq \mytya_1 \myand \myprfora{\myb{x_2}}{\mytya_2}{\myprfora{\myb{x_1}}{\mytya_1}{ \myjm{\myb{x_2}}{\mytya_2}{\myb{x_1}}{\mytya_1} \myimpl \mytyb_1 \myeq \mytyb_2 }} \end{array} @@ -2801,53 +2867,81 @@ equalities. \myderivsp - \AxiomC{$\mytyc{D} : \mytele \myarr \mytyp \in \myctx$} + \AxiomC{} \UnaryInfC{$ - \begin{array}{r@{\ }l} + \begin{array}{@{}r@{\ }l} \myctx \vdash & - \myjm{\mytyc{D} \myappsp \vec{A}}{\mytyp}{\mytyc{D} \myappsp \vec{B}}{\mytyp} \myred \\ - & \myind{2} \myjm{\mytya_1}{\myhead(\mytele)}{\mytyb_1}{\myhead(\mytele)} \myand \cdots \myand \\ - & \myind{2} \myjm{\mytya_n}{\myhead(\mytele(A_1 \cdots A_{n-1}))}{\mytyb_n}{\myhead(\mytele(B_1 \cdots B_{n-1}))} + \myjm{\myse{f}_1}{\myfora{\myb{x_1}}{\mytya_1}{\mytyb_1}}{\myse{f}_2}{\myfora{\myb{x_2}}{\mytya_2}{\mytyb_2}} \myred \\ + & \myind{2} \myprfora{\myb{x_1}}{\mytya_1}{\myprfora{\myb{x_2}}{\mytya_2}{ + \myjm{\myb{x_1}}{\mytya_1}{\myb{x_2}}{\mytya_2} \myimpl + \myjm{\myapp{\myse{f}_1}{\myb{x_1}}}{\mytyb_1[\myb{x_1}]}{\myapp{\myse{f}_2}{\myb{x_2}}}{\mytyb_2[\myb{x_2}]} + }} \end{array} $} \DisplayProof + \myderivsp - \AxiomC{} - \UnaryInfC{$\myctx \vdash \myjm{\mytyp}{\mytyp}{\mytyp}{\mytyp} \myred \mytop$} + \AxiomC{$\mytyc{D} : \mytele \myarr \mytyp \in \myctx$} + \UnaryInfC{$ + \begin{array}{r@{\ }l} + \myctx \vdash & + \myjm{\mytyc{D} \myappsp \vec{A}}{\mytyp}{\mytyc{D} \myappsp \vec{B}}{\mytyp} \myred \\ + & \myind{2} \mybigand_{i = 1}^n (\myjm{\mytya_n}{\myhead(\mytele(A_1 \cdots A_{i-1}))}{\mytyb_i}{\myhead(\mytele(B_1 \cdots B_{i-1}))}) + \end{array} + $} \DisplayProof \myderivsp \AxiomC{$ - \begin{array}{c} + \begin{array}{@{}c} \mydataty(\mytyc{D}, \myctx)\hspace{0.8cm} - \mytyc{D}.\mydc{c}_i : \mytele;\mytele' \myarr \mytyc{D} \myappsp \mytelee \in \myctx \\ + \mytyc{D}.\mydc{c} : \mytele;\mytele' \myarr \mytyc{D} \myappsp \mytelee \in \myctx \\ \mytele_A = (\mytele;\mytele')\vec{A}\hspace{0.8cm} \mytele_B = (\mytele;\mytele')\vec{B} \end{array} $} \UnaryInfC{$ - \begin{array}{l} - \myctx \vdash \myjm{\mytyc{D}.\mydc{c}_i \myappsp \vec{\mytmm}}{\mytyc{D} \myappsp \vec{A}}{\mytyc{D}.\mydc{c}_i \myappsp \vec{\mytmn}}{\mytyc{D} \myappsp \vec{B}} \myred \\ - \myind{2} \myjm{\mytmm_1}{\myhead(\mytele_A)}{\mytmn_1}{\myhead(\mytele_B)} \myand \cdots \myand \\ - \myind{2} \myjm{\mytmm_n}{\mytya_n}{\mytmn_n}{\mytyb_n} + \begin{array}{@{}l@{\ }l} + \myctx \vdash & \myjm{\mytyc{D}.\mydc{c} \myappsp \vec{\myse{l}}}{\mytyc{D} \myappsp \vec{A}}{\mytyc{D}.\mydc{c} \myappsp \vec{\myse{r}}}{\mytyc{D} \myappsp \vec{B}} \myred \\ + & \myind{2} \mybigand_{i=1}^n(\myjm{\mytmm_i}{\myhead(\mytele_A (\mytya_i \cdots \mytya_{i-1}))}{\mytmn_i}{\myhead(\mytele_B (\mytyb_i \cdots \mytyb_{i-1}))}) \end{array} $} \DisplayProof \myderivsp - \AxiomC{$\myisreco(\mytyc{D}, \myctx)$} - \UnaryInfC{$\myctx \vdash \myjm{\mytmm}{\mytyc{D} \myappsp \vec{A}}{\mytmn}{\mytyc{D} \myappsp \vec{B}} \myred foo$} + \AxiomC{$\mydataty(\mytyc{D}, \myctx)$} + \UnaryInfC{$ + \myctx \vdash \myjm{\mytyc{D}.\mydc{c} \myappsp \vec{\myse{l}}}{\mytyc{D} \myappsp \vec{A}}{\mytyc{D}.\mydc{c'} \myappsp \vec{\myse{r}}}{\mytyc{D} \myappsp \vec{B}} \myred \mybot + $} + \DisplayProof + + \myderivsp + + \AxiomC{$ + \begin{array}{@{}c} + \myisreco(\mytyc{D}, \myctx)\hspace{0.8cm} + \mytyc{D}.\myfun{f}_i : \mytele; (\myb{x} {:} \myapp{\mytyc{D}}{\mytelee}) \myarr \myse{F}_i \in \myctx\\ + \end{array} + $} + \UnaryInfC{$ + \begin{array}{@{}l@{\ }l} + \myctx \vdash & \myjm{\myse{l}}{\mytyc{D} \myappsp \vec{A}}{\myse{r}}{\mytyc{D} \myappsp \vec{B}} \myred \\ & \myind{2} \mybigand_{i=1}^n(\myjm{\mytyc{D}.\myfun{f}_1 \myappsp \myse{l}}{(\mytele; (\myb{x} {:} \myapp{\mytyc{D}}{\mytelee}) \myarr \myse{F}_i)(\vec{\mytya};\myse{l})}{\mytyc{D}.\myfun{f}_i \myappsp \myse{r}}{(\mytele; (\myb{x} {:} \myapp{\mytyc{D}}{\mytelee}) \myarr \myse{F}_i)(\vec{\mytyb};\myse{r})}) + \end{array} + $} \DisplayProof \myderivsp \AxiomC{} - \UnaryInfC{$\mytya \myeq \mytyb \myred \mybot\ \text{if $\mytya$ and $\mytyb$ are canonical types.}$} + \UnaryInfC{$\myjm{\mytmm}{\mytya}{\mytmn}{\mytyb} \myred \mybot\ \text{if $\mytya$ and $\mytyb$ are canonical types.}$} \DisplayProof } + \caption{Equality reduction for $\mykant$.} + \label{fig:kant-eq-red} +\end{figure} \subsubsection{$\myprop$ and the hierarchy} @@ -2961,7 +3055,7 @@ diagrammatically in figure \ref{fig:kant-process}: \label{fig:kant-process} \end{figure} -\subsection{Parsing and Sugar} +\subsection{Parsing and \texttt{Sugar}} \subsection{Term representation and context} \label{sec:term-repr} |