From 70bf9aae28c33ac05132bd14a754b7134270eff6 Mon Sep 17 00:00:00 2001 From: Eric Zhao <21zhaoe@protonmail.com> Date: Tue, 6 Jun 2023 15:44:34 -0400 Subject: [PATCH 01/24] formalism: Give brief description of typed action calculus --- formalism/typed.tex | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/formalism/typed.tex b/formalism/typed.tex index 92854d3..21738e8 100644 --- a/formalism/typed.tex +++ b/formalism/typed.tex @@ -9,6 +9,10 @@ \section{Typed hazelnut} \label{sec:typed} +We now give a description of a \emph{typed} version of the Hazelnut action calculus that +incorporates the marked lambda calculus to solve the problem of non-local hole fixes. Here, unlike +in the integration of the untyped version and the marked lambda calculus given in +\cref{sec:untyped}, remarking is performed only when necessary instead of after every action. \nomechanization{} From b0084b63183546322f0733927e09afedd961a3af Mon Sep 17 00:00:00 2001 From: Eric Zhao <21zhaoe@protonmail.com> Date: Sun, 8 Oct 2023 19:48:18 -0400 Subject: [PATCH 02/24] formalism: Fix rules for marked zexp cursor erasure --- formalism/typed.tex | 45 ++++++++++++++++++++++++++++++--------------- 1 file changed, 30 insertions(+), 15 deletions(-) diff --git a/formalism/typed.tex b/formalism/typed.tex index 21738e8..da7be50 100644 --- a/formalism/typed.tex +++ b/formalism/typed.tex @@ -233,21 +233,36 @@ \subsubsection{Expression cursor erasure} \newcommand{\cursorErasesToRow}[2]{\ensuremath{\cursorErase{#1} & = & #2}} \[\begin{array}{rcl} \cursorErasesToRow{\ZCursor{\ECMV}}{\ECMV} \\ - \cursorErasesToRow{(\ZLamT{x}{\ZTMV}{\ECMV})}{\ECLam{x}{\cursorErase{\ZTMV}}{\ECMV}} \\ - \cursorErasesToRow{(\ZLamE{x}{\TMV}{\ZMV})}{\ECLam{x}{\TMV}{\cursorErase{\ZMV}}} \\ - \cursorErasesToRow{(\ZApL{\ZMV}{\ECMV})}{\ECAp{\cursorErase{\ZMV}}{\ECMV}} \\ - \cursorErasesToRow{(\ZApR{\ECMV}{\ZMV})}{\ECAp{\ECMV}{\cursorErase{\ZMV}}} \\ - \cursorErasesToRow{(\ZLetL{x}{\ZMV}{\ECMV})}{\ECLet{x}{\cursorErase{\ZMV}}{\ECMV}} \\ - \cursorErasesToRow{(\ZLetR{x}{\ECMV}{\ZMV})}{\ECLet{x}{\ECMV}{\cursorErase{\ZMV}}} \\ - \cursorErasesToRow{(\ZPlusL{\ZMV}{\ECMV})}{\ECPlus{\cursorErase{\ZMV}}{\ECMV}} \\ - \cursorErasesToRow{(\ZPlusR{\ECMV}{\ZMV})}{\ECPlus{\ECMV}{\cursorErase{\ZMV}}} \\ - \cursorErasesToRow{(\ZIfC{\ZMV}{\ECMV_1}{\ECMV_2})}{\ECIf{\cursorErase{\ZMV}}{\ECMV_1}{\ECMV_2}} \\ - \cursorErasesToRow{(\ZIfL{\ECMV_1}{\ZMV}{\ECMV_2})}{\ECIf{\ECMV_1}{\cursorErase{\ZMV}}{\ECMV_2}} \\ - \cursorErasesToRow{(\ZIfL{\ECMV_1}{\ECMV_2}{\ZMV})}{\ECIf{\ECMV_1}{\ECMV_2}{\cursorErase{\ZMV}}} \\ - \cursorErasesToRow{\ZInconType{\ZMV}}{\cursorErase{\ZMV}} \\ - \cursorErasesToRow{\ZInconBrC{\ZMV}{\ECMV_1}{\ECMV_2}}{\ECIf{\cursorErase{\ZMV}}{\ECMV_1}{\ECMV_2}} \\ - \cursorErasesToRow{\ZInconBrL{\ECMV_1}{\ZMV}{\ECMV_2}}{\ECIf{\ECMV_1}{\cursorErase{\ZMV}}{\ECMV_2}} \\ - \cursorErasesToRow{\ZInconBrR{\ECMV_1}{\ECMV_2}{\ZMV}}{\ECIf{\ECMV_1}{\ECMV_2}{\cursorErase{\ZMV}}} \\ + \cursorErasesToRow{(\ZLamT{x}{\ZTMV}{\ECMV})}{\ECLam{x}{(\cursorErase{\ZTMV})}{\ECMV}} \\ + \cursorErasesToRow{(\ZLamE{x}{\TMV}{\ZMV})}{\ECLam{x}{\TMV}{(\cursorErase{\ZMV})}} \\ + \cursorErasesToRow{(\ZApL{\ZMV}{\ECMV})}{\ECAp{(\cursorErase{\ZMV})}{\ECMV}} \\ + \cursorErasesToRow{(\ZApR{\ECMV}{\ZMV})}{\ECAp{\ECMV}{(\cursorErase{\ZMV})}} \\ + \cursorErasesToRow{(\ZLetL{x}{\ZMV}{\ECMV})}{\ECLet{x}{(\cursorErase{\ZMV})}{\ECMV}} \\ + \cursorErasesToRow{(\ZLetR{x}{\ECMV}{\ZMV})}{\ECLet{x}{\ECMV}{(\cursorErase{\ZMV})}} \\ + \cursorErasesToRow{(\ZPlusL{\ZMV}{\ECMV})}{\ECPlus{(\cursorErase{\ZMV})}{\ECMV}} \\ + \cursorErasesToRow{(\ZPlusR{\ECMV}{\ZMV})}{\ECPlus{\ECMV}{(\cursorErase{\ZMV})}} \\ + \cursorErasesToRow{(\ZIfC{\ZMV}{\ECMV_1}{\ECMV_2})}{\ECIf{(\cursorErase{\ZMV})}{\ECMV_1}{\ECMV_2}} \\ + \cursorErasesToRow{(\ZIfL{\ECMV_1}{\ZMV}{\ECMV_2})}{\ECIf{\ECMV_1}{(\cursorErase{\ZMV})}{\ECMV_2}} \\ + \cursorErasesToRow{(\ZIfL{\ECMV_1}{\ECMV_2}{\ZMV})}{\ECIf{\ECMV_1}{\ECMV_2}{(\cursorErase{\ZMV})}} \\ + \cursorErasesToRow{\ZPairL{\ZMV}{\ECMV}}{\ECPair{\cursorErase{\ZMV}}{\ECMV}} \\ + \cursorErasesToRow{\ZPairR{\ECMV}{\ZMV}}{\ECPair{\ECMV}{\cursorErase{\ZMV}}} \\ + \cursorErasesToRow{(\ZProjL{\ZMV})}{\ECProjL{(\cursorErase{\ZMV})}} \\ + \cursorErasesToRow{(\ZProjR{\ZMV})}{\ECProjR{(\cursorErase{\ZMV})}} \\ + \cursorErasesToRow{\ZFree{x}}{\cursorErase{\ECFree{x}}} \\ + \cursorErasesToRow{\ZInconType{\ZMV}}{\ECInconType{\cursorErase{\ZMV}}} \\ + \cursorErasesToRow{\ZLamInconAscT{x}{\ZTMV}{\ECMV}}{\ECLamInconAsc{x}{\cursorErase{\ZTMV}}{\ECMV}} \\ + \cursorErasesToRow{\ZLamInconAscE{x}{\TMV}{\ZMV}}{\ECLamInconAsc{x}{\TMV}{\cursorErase{\ZMV}}} \\ + \cursorErasesToRow{\ZLamAnaNonMatchedArrowT{x}{\ZTMV}{\ECMV}}{\ECLamAnaNonMatchedArrow{x}{\cursorErase{\ZTMV}}{\ECMV}} \\ + \cursorErasesToRow{\ZLamAnaNonMatchedArrowE{x}{\TMV}{\ZMV}}{\ECLamAnaNonMatchedArrow{x}{\TMV}{\cursorErase{\ZMV}}} \\ + \cursorErasesToRow{(\ZApSynNonMatchedArrowL{\ZMV}{\ECMV})}{\ECApSynNonMatchedArrow{\cursorErase{\ZMV}}{\ECMV}} \\ + \cursorErasesToRow{(\ZApSynNonMatchedArrowR{\ECMV}{\ZMV})}{\ECApSynNonMatchedArrow{\ECMV}{(\cursorErase{\ZMV})}} \\ + \cursorErasesToRow{\ZInconBrC{\ZMV}{\ECMV_1}{\ECMV_2}}{\ECInconBr{\cursorErase{\ZMV}}{\ECMV_1}{\ECMV_2}} \\ + \cursorErasesToRow{\ZInconBrL{\ECMV_1}{\ZMV}{\ECMV_2}}{\ECInconBr{\ECMV_1}{\cursorErase{\ZMV}}{\ECMV_2}} \\ + \cursorErasesToRow{\ZInconBrR{\ECMV_1}{\ECMV_2}{\ZMV}}{\ECInconBr{\ECMV_1}{\ECMV_2}{\cursorErase{\ZMV}}} \\ + \cursorErasesToRow{\ZPairAnaNonMatchedProdL{\ZMV}{\ECMV}}{\ECPairAnaNonMatchedProd{\cursorErase{\ZMV}}{\ECMV}} \\ + \cursorErasesToRow{\ZPairAnaNonMatchedProdR{\ECMV}{\ZMV}}{\ECPairAnaNonMatchedProd{\ECMV}{\cursorErase{\ZMV}}} \\ + \cursorErasesToRow{(\ZProjLSynNonMatchedProd{\ZMV})}{\ECProjLSynNonMatchedProd{\cursorErase{\ZMV}}} \\ + \cursorErasesToRow{(\ZProjRSynNonMatchedProd{\ZMV})}{\ECProjRSynNonMatchedProd{\cursorErase{\ZMV}}} \\ \end{array}\] \subsection{Action model} From 4d9dc02e0b2efa8afc6e453676f3576766069773 Mon Sep 17 00:00:00 2001 From: Eric Zhao <21zhaoe@protonmail.com> Date: Sun, 8 Oct 2023 20:38:52 -0400 Subject: [PATCH 03/24] formalism: Use separate metavariable for marked zexps from untyped zexps --- formalism/symbols/typed.tex | 60 ++++ formalism/typed.tex | 618 ++++++++++++++++++------------------ 2 files changed, 369 insertions(+), 309 deletions(-) diff --git a/formalism/symbols/typed.tex b/formalism/symbols/typed.tex index f26b078..8934d3e 100644 --- a/formalism/symbols/typed.tex +++ b/formalism/symbols/typed.tex @@ -1,5 +1,65 @@ % !requires untyped +% +% marked zippered expressions +% +\newcommand{\ZCMName}{{\normalfont\textsf{MZExp}}} +\newcommand{\ZCMSet}{\ensuremath{\hat{E}}} +\newcommand{\ZCMV}{\ensuremath{\underline{\check{e}}}} + +% cursor +\definecolor{cursorhighlight}{RGB}{230,255,230} +\definecolor{cursor}{RGB}{76,170,76} +\newcommand{\ZCCursor}[1]{\ensuremath{\mathcolorbox{cursorhighlight}{\textcolor{cursor}{\bm{\triangleright}}#1\textcolor{cursor}{\bm{\triangleleft}}}}} + +% integers +\newcommand{\ZCPlusL}[2]{\ensuremath{\ECPlus{#1}{#2}}} +\newcommand{\ZCPlusR}[2]{\ensuremath{\ECPlus{#1}{#2}}} + +% lambdas +\newcommand{\ZCLamT}[3]{\ensuremath{\ECLam{#1}{#2}{#3}}} +\newcommand{\ZCLamE}[3]{\ensuremath{\ECLam{#1}{#2}{#3}}} +\newcommand{\ZCApL}[2]{\ensuremath{\ECAp{#1}{#2}}} +\newcommand{\ZCApR}[2]{\ensuremath{\ECAp{#1}{#2}}} + +% booleans +\newcommand{\ZCIfC}[3]{\ensuremath{\ECIf{#1}{#2}{#3}}} +\newcommand{\ZCIfL}[3]{\ensuremath{\ECIf{#1}{#2}{#3}}} +\newcommand{\ZCIfR}[3]{\ensuremath{\ECIf{#1}{#2}{#3}}} + +% let +\newcommand{\ZCLetL}[3]{\ensuremath{\ECLet{#1}{#2}{#3}}} +\newcommand{\ZCLetR}[3]{\ensuremath{\ECLet{#1}{#2}{#3}}} + +% pairs +\newcommand{\ZCPairL}[2]{\ensuremath{\ECPair{#1}{#2}}} +\newcommand{\ZCPairR}[2]{\ensuremath{\ECPair{#1}{#2}}} +\newcommand{\ZCProjL}[1]{\ensuremath{\ECProjL{#1}}} +\newcommand{\ZCProjR}[1]{\ensuremath{\ECProjR{#1}}} + +% errors +\newcommand{\ZCFree}[1]{\ensuremath{\ECFree{#1}}} +\newcommand{\ZCInconType}[1]{\ensuremath{\ECInconType{#1}}} +\newcommand{\ZCInconBrC}[3]{\ensuremath{\ECInconBr{#1}{#2}{#3}}} +\newcommand{\ZCInconBrL}[3]{\ensuremath{\ECInconBr{#1}{#2}{#3}}} +\newcommand{\ZCInconBrR}[3]{\ensuremath{\ECInconBr{#1}{#2}{#3}}} +\newcommand{\ZCInconAsc}[1]{\ensuremath{\ECInconAsc{#1}}} +\newcommand{\ZCSynNonMatchedArrow}[1]{\ensuremath{\ECSynNonMatchedArrow{#1}}} +\newcommand{\ZCSynNonMatchedProd}[1]{\ensuremath{\ECSynNonMatchedProd{#1}}} +\newcommand{\ZCAnaNonMatchedArrow}[1]{\ensuremath{\ECAnaNonMatchedArrow{#1}}} +\newcommand{\ZCAnaNonMatchedProd}[1]{\ensuremath{\ECAnaNonMatchedProd{#1}}} + +\newcommand{\ZCLamInconAscT}[3]{\ensuremath{\ECInconAsc{\ECLam{#1}{#2}{#3}}}} +\newcommand{\ZCLamInconAscE}[3]{\ensuremath{\ECInconAsc{\ECLam{#1}{#2}{#3}}}} +\newcommand{\ZCApSynNonMatchedArrowL}[2]{\ensuremath{\ECAp{\ECSynNonMatchedArrow{#1}}{#2}}} +\newcommand{\ZCApSynNonMatchedArrowR}[2]{\ensuremath{\ECAp{\ECSynNonMatchedArrow{#1}}{#2}}} +\newcommand{\ZCProjLSynNonMatchedProd}[1]{\ensuremath{\ECProjL{\ECSynNonMatchedProd{#1}}}} +\newcommand{\ZCProjRSynNonMatchedProd}[1]{\ensuremath{\ECProjR{\ECSynNonMatchedProd{#1}}}} +\newcommand{\ZCLamAnaNonMatchedArrowT}[3]{\ensuremath{\ECAnaNonMatchedArrow{\ECLam{#1}{#2}{#3}}}} +\newcommand{\ZCLamAnaNonMatchedArrowE}[3]{\ensuremath{\ECAnaNonMatchedArrow{\ECLam{#1}{#2}{#3}}}} +\newcommand{\ZCPairAnaNonMatchedProdL}[2]{\ensuremath{\ECAnaNonMatchedProd{\ECPair{#1}{#2}}}} +\newcommand{\ZCPairAnaNonMatchedProdR}[2]{\ensuremath{\ECAnaNonMatchedProd{\ECPair{#1}{#2}}}} + % zippered expression well-formedness \newcommand{\zWellFormed}[1]{\ensuremath{#1 ~{\normalfont\textsf{WF}}}} diff --git a/formalism/typed.tex b/formalism/typed.tex index da7be50..c29d131 100644 --- a/formalism/typed.tex +++ b/formalism/typed.tex @@ -21,201 +21,201 @@ \subsection{Syntax} Zippered types are the same as in the untyped model. \[\begin{array}{rrcl} - \ZMName & \ZMV & \Coloneqq & \ZCursor{\ECMV} \mid \ZLamT{x}{\ZTMV}{\ECMV} \mid \ZLamE{x}{\TMV}{\ZMV} \mid \ZApL{\ZMV}{\ECMV} \mid \ZApR{\ECMV}{\ZMV} \\ - & & \mid & \ZLetL{x}{\ZMV}{\ECMV} \mid \ZLetR{x}{\ECMV}{\ZMV} \\ - & & \mid & \ZPlusL{\ZMV}{\ECMV} \mid \ZPlusR{\ECMV}{\ZMV} \\ - & & \mid & \ZIfC{\ZMV}{\ECMV}{\ECMV} \mid \ZIfL{\ECMV}{\ZMV}{\ECMV} \mid \ZIfR{\ECMV}{\ECMV}{\ZMV} \\ - & & \mid & \ZPairL{\ZMV}{\EMV} \mid \ZPairR{\EMV}{\ZMV} \mid \ZProjL{\ZMV} \mid \ZProjR{\ZMV} \\ - & & \mid & \ZFree{x} \mid \ZInconType{\ZMV} \\ - & & \mid & \ZLamInconAscT{x}{\ZTMV}{\ECMV} \mid \ZLamInconAscE{x}{\TMV}{\ZMV} - \mid \ZLamAnaNonMatchedArrowT{x}{\ZTMV}{\ECMV} \mid \ZLamAnaNonMatchedArrowE{x}{\TMV}{\ZMV} - \mid \ZApSynNonMatchedArrowL{\ZMV}{\ECMV} \mid \ZApSynNonMatchedArrowR{\ECMV}{\ZMV} \\ - & & \mid & \ZInconBrC{\ZMV}{\ECMV}{\ECMV} \mid \ZInconBrL{\ECMV}{\ZMV}{\ECMV} \mid \ZInconBrR{\ECMV}{\ECMV}{\ZMV} \\ - & & \mid & \ZPairAnaNonMatchedProdL{\ZMV}{\ECMV} \mid \ZPairAnaNonMatchedProdR{\ECMV}{\ZMV} - \mid \ZProjLSynNonMatchedProd{\ZMV} \mid \ZProjRSynNonMatchedProd{\ZMV} + \ZCMName & \ZCMV & \Coloneqq & \ZCCursor{\ECMV} \mid \ZCLamT{x}{\ZTMV}{\ECMV} \mid \ZCLamE{x}{\TMV}{\ZCMV} \mid \ZCApL{\ZCMV}{\ECMV} \mid \ZCApR{\ECMV}{\ZCMV} \\ + & & \mid & \ZCLetL{x}{\ZCMV}{\ECMV} \mid \ZCLetR{x}{\ECMV}{\ZCMV} \\ + & & \mid & \ZCPlusL{\ZCMV}{\ECMV} \mid \ZCPlusR{\ECMV}{\ZCMV} \\ + & & \mid & \ZCIfC{\ZCMV}{\ECMV}{\ECMV} \mid \ZCIfL{\ECMV}{\ZCMV}{\ECMV} \mid \ZCIfR{\ECMV}{\ECMV}{\ZCMV} \\ + & & \mid & \ZCPairL{\ZCMV}{\EMV} \mid \ZCPairR{\EMV}{\ZCMV} \mid \ZCProjL{\ZCMV} \mid \ZCProjR{\ZCMV} \\ + & & \mid & \ZCFree{x} \mid \ZCInconType{\ZCMV} \\ + & & \mid & \ZCLamInconAscT{x}{\ZTMV}{\ECMV} \mid \ZCLamInconAscE{x}{\TMV}{\ZCMV} + \mid \ZCLamAnaNonMatchedArrowT{x}{\ZTMV}{\ECMV} \mid \ZCLamAnaNonMatchedArrowE{x}{\TMV}{\ZCMV} + \mid \ZCApSynNonMatchedArrowL{\ZCMV}{\ECMV} \mid \ZCApSynNonMatchedArrowR{\ECMV}{\ZCMV} \\ + & & \mid & \ZCInconBrC{\ZCMV}{\ECMV}{\ECMV} \mid \ZCInconBrL{\ECMV}{\ZCMV}{\ECMV} \mid \ZCInconBrR{\ECMV}{\ECMV}{\ZCMV} \\ + & & \mid & \ZCPairAnaNonMatchedProdL{\ZCMV}{\ECMV} \mid \ZCPairAnaNonMatchedProdR{\ECMV}{\ZCMV} + \mid \ZCProjLSynNonMatchedProd{\ZCMV} \mid \ZCProjRSynNonMatchedProd{\ZCMV} \end{array}\] \subsubsection{Well-formedness} \label{sec:typed-well-formedness} -\judgbox{\ensuremath{\zWellFormed{\ZMV}}} $\ZMV$ is well-formed +\judgbox{\ensuremath{\zWellFormed{\ZCMV}}} $\ZCMV$ is well-formed % \begin{mathpar} \inferrule[WFCursor]{ }{ - \zWellFormed{\ZCursor{\ECMV}} + \zWellFormed{\ZCCursor{\ECMV}} } \inferrule[WFLam1]{ }{ - \zWellFormed{\ZLamT{x}{\ZTMV}{\ECMV}} + \zWellFormed{\ZCLamT{x}{\ZTMV}{\ECMV}} } \inferrule[WFLam2]{ - \zWellFormed{\ZMV} + \zWellFormed{\ZCMV} }{ - \zWellFormed{\ZLamE{x}{\TMV}{\ZMV}} + \zWellFormed{\ZCLamE{x}{\TMV}{\ZCMV}} } \inferrule[WFAp1]{ - \zWellFormed{\ZMV} + \zWellFormed{\ZCMV} }{ - \zWellFormed{\ZApL{\ZMV}{\ECMV}} + \zWellFormed{\ZCApL{\ZCMV}{\ECMV}} } \inferrule[WFAp2]{ - \zWellFormed{\ZMV} + \zWellFormed{\ZCMV} }{ - \zWellFormed{\ZApR{\ECMV}{\ZMV}} + \zWellFormed{\ZCApR{\ECMV}{\ZCMV}} } \inferrule[WFLet1]{ - \zWellFormed{\ZMV} + \zWellFormed{\ZCMV} }{ - \zWellFormed{\ZLetL{x}{\ZMV}{\ECMV}} + \zWellFormed{\ZCLetL{x}{\ZCMV}{\ECMV}} } \inferrule[WFLet2]{ - \zWellFormed{\ZMV} + \zWellFormed{\ZCMV} }{ - \zWellFormed{\ZLetR{x}{\ECMV}{\ZMV}} + \zWellFormed{\ZCLetR{x}{\ECMV}{\ZCMV}} } \inferrule[WFPlus1]{ - \zWellFormed{\ZMV} + \zWellFormed{\ZCMV} }{ - \zWellFormed{\ZPlusL{\ZMV}{\ECMV}} + \zWellFormed{\ZCPlusL{\ZCMV}{\ECMV}} } \inferrule[WFPlus2]{ - \zWellFormed{\ZMV} + \zWellFormed{\ZCMV} }{ - \zWellFormed{\ZPlusR{\ECMV}{\ZMV}} + \zWellFormed{\ZCPlusR{\ECMV}{\ZCMV}} } \inferrule[WFIf1]{ - \zWellFormed{\ZMV} + \zWellFormed{\ZCMV} }{ - \zWellFormed{\ZIfC{\ZMV}{\ECMV_1}{\ECMV_2}} + \zWellFormed{\ZCIfC{\ZCMV}{\ECMV_1}{\ECMV_2}} } \inferrule[WFIf2]{ - \zWellFormed{\ZMV} + \zWellFormed{\ZCMV} }{ - \zWellFormed{\ZIfL{\ECMV_1}{\ZMV}{\ECMV_2}} + \zWellFormed{\ZCIfL{\ECMV_1}{\ZCMV}{\ECMV_2}} } \inferrule[WFIf3]{ - \zWellFormed{\ZMV} + \zWellFormed{\ZCMV} }{ - \zWellFormed{\ZIfR{\ECMV_1}{\ECMV_2}{\ZMV}} + \zWellFormed{\ZCIfR{\ECMV_1}{\ECMV_2}{\ZCMV}} } \inferrule[WFPair1]{ - \zWellFormed{\ZMV} + \zWellFormed{\ZCMV} }{ - \zWellFormed{\ZPairL{\ZMV}{\ECMV}} + \zWellFormed{\ZCPairL{\ZCMV}{\ECMV}} } \inferrule[WFPair2]{ - \zWellFormed{\ZMV} + \zWellFormed{\ZCMV} }{ - \zWellFormed{\ZPairR{\ECMV}{\ZMV}} + \zWellFormed{\ZCPairR{\ECMV}{\ZCMV}} } \inferrule[WFProjL1]{ - \zWellFormed{\ZMV} + \zWellFormed{\ZCMV} }{ - \zWellFormed{\ZProjL{\ZMV}} + \zWellFormed{\ZCProjL{\ZCMV}} } \inferrule[WFProjR1]{ - \zWellFormed{\ZMV} + \zWellFormed{\ZCMV} }{ - \zWellFormed{\ZProjR{\ZMV}} + \zWellFormed{\ZCProjR{\ZCMV}} } \inferrule[WFFree]{ }{ - \zWellFormed{\ZFree{x}} + \zWellFormed{\ZCFree{x}} } \inferrule[WFInconsistentTypes]{ - \notEqual{\ZMV}{\ZCursor{\ECMV}} \\ - \zWellFormed{\ZMV} + \notEqual{\ZCMV}{\ZCCursor{\ECMV}} \\ + \zWellFormed{\ZCMV} }{ - \zWellFormed{\ZInconType{\ZMV}} + \zWellFormed{\ZCInconType{\ZCMV}} } \inferrule[WFLam3]{ }{ - \zWellFormed{\ZLamInconAscT{x}{\ZTMV}{\ECMV}} + \zWellFormed{\ZCLamInconAscT{x}{\ZTMV}{\ECMV}} } \inferrule[WFLam4]{ - \zWellFormed{\ZMV} + \zWellFormed{\ZCMV} }{ - \zWellFormed{\ZLamInconAscE{x}{\TMV}{\ZMV}} + \zWellFormed{\ZCLamInconAscE{x}{\TMV}{\ZCMV}} } \inferrule[WFLam5]{ }{ - \zWellFormed{\ZLamAnaNonMatchedArrowT{x}{\ZTMV}{\ECMV}} + \zWellFormed{\ZCLamAnaNonMatchedArrowT{x}{\ZTMV}{\ECMV}} } \inferrule[WFLam6]{ - \zWellFormed{\ZMV} + \zWellFormed{\ZCMV} }{ - \zWellFormed{\ZLamAnaNonMatchedArrowE{x}{\TMV}{\ZMV}} + \zWellFormed{\ZCLamAnaNonMatchedArrowE{x}{\TMV}{\ZCMV}} } \inferrule[WFAp3]{ - \zWellFormed{\ZMV} + \zWellFormed{\ZCMV} }{ - \zWellFormed{\ZApSynNonMatchedArrowL{\ZMV}{\ECMV}} + \zWellFormed{\ZCApSynNonMatchedArrowL{\ZCMV}{\ECMV}} } \inferrule[WFAp4]{ - \zWellFormed{\ZMV} + \zWellFormed{\ZCMV} }{ - \zWellFormed{\ZApSynNonMatchedArrowR{\ECMV}{\ZMV}} + \zWellFormed{\ZCApSynNonMatchedArrowR{\ECMV}{\ZCMV}} } \inferrule[WFInconsistentBranches1]{ - \zWellFormed{\ZMV} + \zWellFormed{\ZCMV} }{ - \zWellFormed{\ZInconBrC{\ZMV}{\ECMV_1}{\ECMV_2}} + \zWellFormed{\ZCInconBrC{\ZCMV}{\ECMV_1}{\ECMV_2}} } \inferrule[WFInconsistentBranches2]{ - \zWellFormed{\ZMV} + \zWellFormed{\ZCMV} }{ - \zWellFormed{\ZInconBrL{\ECMV_1}{\ZMV}{\ECMV_2}} + \zWellFormed{\ZCInconBrL{\ECMV_1}{\ZCMV}{\ECMV_2}} } \inferrule[WFInconsistentBranches3]{ - \zWellFormed{\ZMV} + \zWellFormed{\ZCMV} }{ - \zWellFormed{\ZInconBrR{\ECMV_1}{\ECMV_2}{\ZMV}} + \zWellFormed{\ZCInconBrR{\ECMV_1}{\ECMV_2}{\ZCMV}} } \inferrule[WFPair3]{ - \zWellFormed{\ZMV} + \zWellFormed{\ZCMV} }{ - \zWellFormed{\ZPairAnaNonMatchedProdL{\ZMV}{\ECMV}} + \zWellFormed{\ZCPairAnaNonMatchedProdL{\ZCMV}{\ECMV}} } \inferrule[WFPair4]{ - \zWellFormed{\ZMV} + \zWellFormed{\ZCMV} }{ - \zWellFormed{\ZPairAnaNonMatchedProdR{\ECMV}{\ZMV}} + \zWellFormed{\ZCPairAnaNonMatchedProdR{\ECMV}{\ZCMV}} } \inferrule[WFProjL2]{ - \zWellFormed{\ZMV} + \zWellFormed{\ZCMV} }{ - \zWellFormed{\ZProjLSynNonMatchedProd{\ZMV}} + \zWellFormed{\ZCProjLSynNonMatchedProd{\ZCMV}} } \inferrule[WFProjR2]{ - \zWellFormed{\ZMV} + \zWellFormed{\ZCMV} }{ - \zWellFormed{\ZProjRSynNonMatchedProd{\ZMV}} + \zWellFormed{\ZCProjRSynNonMatchedProd{\ZCMV}} } \end{mathpar} @@ -228,41 +228,41 @@ \subsubsection{Type cursor erasure} \subsubsection{Expression cursor erasure} \label{sec:typed-expression-cursor-erasure} -\judgbox{\ensuremath{\cursorErase{\ZMV}}} is a metafunction defined as follows: +\judgbox{\ensuremath{\cursorErase{\ZCMV}}} is a metafunction defined as follows: % \newcommand{\cursorErasesToRow}[2]{\ensuremath{\cursorErase{#1} & = & #2}} \[\begin{array}{rcl} - \cursorErasesToRow{\ZCursor{\ECMV}}{\ECMV} \\ - \cursorErasesToRow{(\ZLamT{x}{\ZTMV}{\ECMV})}{\ECLam{x}{(\cursorErase{\ZTMV})}{\ECMV}} \\ - \cursorErasesToRow{(\ZLamE{x}{\TMV}{\ZMV})}{\ECLam{x}{\TMV}{(\cursorErase{\ZMV})}} \\ - \cursorErasesToRow{(\ZApL{\ZMV}{\ECMV})}{\ECAp{(\cursorErase{\ZMV})}{\ECMV}} \\ - \cursorErasesToRow{(\ZApR{\ECMV}{\ZMV})}{\ECAp{\ECMV}{(\cursorErase{\ZMV})}} \\ - \cursorErasesToRow{(\ZLetL{x}{\ZMV}{\ECMV})}{\ECLet{x}{(\cursorErase{\ZMV})}{\ECMV}} \\ - \cursorErasesToRow{(\ZLetR{x}{\ECMV}{\ZMV})}{\ECLet{x}{\ECMV}{(\cursorErase{\ZMV})}} \\ - \cursorErasesToRow{(\ZPlusL{\ZMV}{\ECMV})}{\ECPlus{(\cursorErase{\ZMV})}{\ECMV}} \\ - \cursorErasesToRow{(\ZPlusR{\ECMV}{\ZMV})}{\ECPlus{\ECMV}{(\cursorErase{\ZMV})}} \\ - \cursorErasesToRow{(\ZIfC{\ZMV}{\ECMV_1}{\ECMV_2})}{\ECIf{(\cursorErase{\ZMV})}{\ECMV_1}{\ECMV_2}} \\ - \cursorErasesToRow{(\ZIfL{\ECMV_1}{\ZMV}{\ECMV_2})}{\ECIf{\ECMV_1}{(\cursorErase{\ZMV})}{\ECMV_2}} \\ - \cursorErasesToRow{(\ZIfL{\ECMV_1}{\ECMV_2}{\ZMV})}{\ECIf{\ECMV_1}{\ECMV_2}{(\cursorErase{\ZMV})}} \\ - \cursorErasesToRow{\ZPairL{\ZMV}{\ECMV}}{\ECPair{\cursorErase{\ZMV}}{\ECMV}} \\ - \cursorErasesToRow{\ZPairR{\ECMV}{\ZMV}}{\ECPair{\ECMV}{\cursorErase{\ZMV}}} \\ - \cursorErasesToRow{(\ZProjL{\ZMV})}{\ECProjL{(\cursorErase{\ZMV})}} \\ - \cursorErasesToRow{(\ZProjR{\ZMV})}{\ECProjR{(\cursorErase{\ZMV})}} \\ - \cursorErasesToRow{\ZFree{x}}{\cursorErase{\ECFree{x}}} \\ - \cursorErasesToRow{\ZInconType{\ZMV}}{\ECInconType{\cursorErase{\ZMV}}} \\ - \cursorErasesToRow{\ZLamInconAscT{x}{\ZTMV}{\ECMV}}{\ECLamInconAsc{x}{\cursorErase{\ZTMV}}{\ECMV}} \\ - \cursorErasesToRow{\ZLamInconAscE{x}{\TMV}{\ZMV}}{\ECLamInconAsc{x}{\TMV}{\cursorErase{\ZMV}}} \\ - \cursorErasesToRow{\ZLamAnaNonMatchedArrowT{x}{\ZTMV}{\ECMV}}{\ECLamAnaNonMatchedArrow{x}{\cursorErase{\ZTMV}}{\ECMV}} \\ - \cursorErasesToRow{\ZLamAnaNonMatchedArrowE{x}{\TMV}{\ZMV}}{\ECLamAnaNonMatchedArrow{x}{\TMV}{\cursorErase{\ZMV}}} \\ - \cursorErasesToRow{(\ZApSynNonMatchedArrowL{\ZMV}{\ECMV})}{\ECApSynNonMatchedArrow{\cursorErase{\ZMV}}{\ECMV}} \\ - \cursorErasesToRow{(\ZApSynNonMatchedArrowR{\ECMV}{\ZMV})}{\ECApSynNonMatchedArrow{\ECMV}{(\cursorErase{\ZMV})}} \\ - \cursorErasesToRow{\ZInconBrC{\ZMV}{\ECMV_1}{\ECMV_2}}{\ECInconBr{\cursorErase{\ZMV}}{\ECMV_1}{\ECMV_2}} \\ - \cursorErasesToRow{\ZInconBrL{\ECMV_1}{\ZMV}{\ECMV_2}}{\ECInconBr{\ECMV_1}{\cursorErase{\ZMV}}{\ECMV_2}} \\ - \cursorErasesToRow{\ZInconBrR{\ECMV_1}{\ECMV_2}{\ZMV}}{\ECInconBr{\ECMV_1}{\ECMV_2}{\cursorErase{\ZMV}}} \\ - \cursorErasesToRow{\ZPairAnaNonMatchedProdL{\ZMV}{\ECMV}}{\ECPairAnaNonMatchedProd{\cursorErase{\ZMV}}{\ECMV}} \\ - \cursorErasesToRow{\ZPairAnaNonMatchedProdR{\ECMV}{\ZMV}}{\ECPairAnaNonMatchedProd{\ECMV}{\cursorErase{\ZMV}}} \\ - \cursorErasesToRow{(\ZProjLSynNonMatchedProd{\ZMV})}{\ECProjLSynNonMatchedProd{\cursorErase{\ZMV}}} \\ - \cursorErasesToRow{(\ZProjRSynNonMatchedProd{\ZMV})}{\ECProjRSynNonMatchedProd{\cursorErase{\ZMV}}} \\ + \cursorErasesToRow{\ZCCursor{\ECMV}}{\ECMV} \\ + \cursorErasesToRow{(\ZCLamT{x}{\ZTMV}{\ECMV})}{\ECLam{x}{(\cursorErase{\ZTMV})}{\ECMV}} \\ + \cursorErasesToRow{(\ZCLamE{x}{\TMV}{\ZCMV})}{\ECLam{x}{\TMV}{(\cursorErase{\ZCMV})}} \\ + \cursorErasesToRow{(\ZCApL{\ZCMV}{\ECMV})}{\ECAp{(\cursorErase{\ZCMV})}{\ECMV}} \\ + \cursorErasesToRow{(\ZCApR{\ECMV}{\ZCMV})}{\ECAp{\ECMV}{(\cursorErase{\ZCMV})}} \\ + \cursorErasesToRow{(\ZCLetL{x}{\ZCMV}{\ECMV})}{\ECLet{x}{(\cursorErase{\ZCMV})}{\ECMV}} \\ + \cursorErasesToRow{(\ZCLetR{x}{\ECMV}{\ZCMV})}{\ECLet{x}{\ECMV}{(\cursorErase{\ZCMV})}} \\ + \cursorErasesToRow{(\ZCPlusL{\ZCMV}{\ECMV})}{\ECPlus{(\cursorErase{\ZCMV})}{\ECMV}} \\ + \cursorErasesToRow{(\ZCPlusR{\ECMV}{\ZCMV})}{\ECPlus{\ECMV}{(\cursorErase{\ZCMV})}} \\ + \cursorErasesToRow{(\ZCIfC{\ZCMV}{\ECMV_1}{\ECMV_2})}{\ECIf{(\cursorErase{\ZCMV})}{\ECMV_1}{\ECMV_2}} \\ + \cursorErasesToRow{(\ZCIfL{\ECMV_1}{\ZCMV}{\ECMV_2})}{\ECIf{\ECMV_1}{(\cursorErase{\ZCMV})}{\ECMV_2}} \\ + \cursorErasesToRow{(\ZCIfL{\ECMV_1}{\ECMV_2}{\ZCMV})}{\ECIf{\ECMV_1}{\ECMV_2}{(\cursorErase{\ZCMV})}} \\ + \cursorErasesToRow{\ZCPairL{\ZCMV}{\ECMV}}{\ECPair{\cursorErase{\ZCMV}}{\ECMV}} \\ + \cursorErasesToRow{\ZCPairR{\ECMV}{\ZCMV}}{\ECPair{\ECMV}{\cursorErase{\ZCMV}}} \\ + \cursorErasesToRow{(\ZCProjL{\ZCMV})}{\ECProjL{(\cursorErase{\ZCMV})}} \\ + \cursorErasesToRow{(\ZCProjR{\ZCMV})}{\ECProjR{(\cursorErase{\ZCMV})}} \\ + \cursorErasesToRow{\ZCFree{x}}{\cursorErase{\ECFree{x}}} \\ + \cursorErasesToRow{\ZCInconType{\ZCMV}}{\ECInconType{\cursorErase{\ZCMV}}} \\ + \cursorErasesToRow{\ZCLamInconAscT{x}{\ZTMV}{\ECMV}}{\ECLamInconAsc{x}{\cursorErase{\ZTMV}}{\ECMV}} \\ + \cursorErasesToRow{\ZCLamInconAscE{x}{\TMV}{\ZCMV}}{\ECLamInconAsc{x}{\TMV}{\cursorErase{\ZCMV}}} \\ + \cursorErasesToRow{\ZCLamAnaNonMatchedArrowT{x}{\ZTMV}{\ECMV}}{\ECLamAnaNonMatchedArrow{x}{\cursorErase{\ZTMV}}{\ECMV}} \\ + \cursorErasesToRow{\ZCLamAnaNonMatchedArrowE{x}{\TMV}{\ZCMV}}{\ECLamAnaNonMatchedArrow{x}{\TMV}{\cursorErase{\ZCMV}}} \\ + \cursorErasesToRow{(\ZCApSynNonMatchedArrowL{\ZCMV}{\ECMV})}{\ECApSynNonMatchedArrow{\cursorErase{\ZCMV}}{\ECMV}} \\ + \cursorErasesToRow{(\ZCApSynNonMatchedArrowR{\ECMV}{\ZCMV})}{\ECApSynNonMatchedArrow{\ECMV}{(\cursorErase{\ZCMV})}} \\ + \cursorErasesToRow{\ZCInconBrC{\ZCMV}{\ECMV_1}{\ECMV_2}}{\ECInconBr{\cursorErase{\ZCMV}}{\ECMV_1}{\ECMV_2}} \\ + \cursorErasesToRow{\ZCInconBrL{\ECMV_1}{\ZCMV}{\ECMV_2}}{\ECInconBr{\ECMV_1}{\cursorErase{\ZCMV}}{\ECMV_2}} \\ + \cursorErasesToRow{\ZCInconBrR{\ECMV_1}{\ECMV_2}{\ZCMV}}{\ECInconBr{\ECMV_1}{\ECMV_2}{\cursorErase{\ZCMV}}} \\ + \cursorErasesToRow{\ZCPairAnaNonMatchedProdL{\ZCMV}{\ECMV}}{\ECPairAnaNonMatchedProd{\cursorErase{\ZCMV}}{\ECMV}} \\ + \cursorErasesToRow{\ZCPairAnaNonMatchedProdR{\ECMV}{\ZCMV}}{\ECPairAnaNonMatchedProd{\ECMV}{\cursorErase{\ZCMV}}} \\ + \cursorErasesToRow{(\ZCProjLSynNonMatchedProd{\ZCMV})}{\ECProjLSynNonMatchedProd{\cursorErase{\ZCMV}}} \\ + \cursorErasesToRow{(\ZCProjRSynNonMatchedProd{\ZCMV})}{\ECProjRSynNonMatchedProd{\cursorErase{\ZCMV}}} \\ \end{array}\] \subsection{Action model} @@ -279,144 +279,144 @@ \subsubsection{Type actions} \subsubsection{Expression movement} \label{sec:typed-expression-movement} -\judgbox{\ensuremath{\AUEMove{\ZMV}{\ZMV'}{\MMV}}} +\judgbox{\ensuremath{\AUEMove{\ZCMV}{\ZCMV'}{\MMV}}} % \begin{mathparpagebreakable} \inferrule[AEMLamChild1]{ }{ - \ASEMChild{\ECLam{x}{\TMV}{\ECMV}}{\ZLamT{x}{\ZTCursor{\TMV}}{\ECMV}}{1} + \ASEMChild{\ECLam{x}{\TMV}{\ECMV}}{\ZCLamT{x}{\ZTCursor{\TMV}}{\ECMV}}{1} } \inferrule[AEMLamChild2]{ }{ - \ASEMChild{\ECLam{x}{\TMV}{\ECMV}}{\ZLamE{x}{\TMV}{\ZCursor{\ECMV}}}{2} + \ASEMChild{\ECLam{x}{\TMV}{\ECMV}}{\ZCLamE{x}{\TMV}{\ZCCursor{\ECMV}}}{2} } \inferrule[AEMLamParent1]{ }{ - \ASEMParent{\ZLamT{x}{\ZTCursor{\TMV}}{\ECMV}}{\ECLam{x}{\TMV}{\ECMV}} + \ASEMParent{\ZCLamT{x}{\ZTCursor{\TMV}}{\ECMV}}{\ECLam{x}{\TMV}{\ECMV}} } \inferrule[AEMLamParent2]{ }{ - \ASEMParent{\ZLamE{x}{\TMV}{\ZCursor{\ECMV}}}{\ECLam{x}{\TMV}{\ECMV}} + \ASEMParent{\ZCLamE{x}{\TMV}{\ZCCursor{\ECMV}}}{\ECLam{x}{\TMV}{\ECMV}} } \inferrule[AEMApChild1]{ }{ - \ASEMChild{\ECAp{\ECMV_1}{\ECMV_2}}{\ZApL{\ZCursor{\ECMV_1}}{\ECMV_2}}{1} + \ASEMChild{\ECAp{\ECMV_1}{\ECMV_2}}{\ZCApL{\ZCCursor{\ECMV_1}}{\ECMV_2}}{1} } \inferrule[AEMApChild2]{ }{ - \ASEMChild{\ECAp{\ECMV_1}{\ECMV_2}}{\ZApR{\ECMV_1}{\ZCursor{\ECMV_2}}}{2} + \ASEMChild{\ECAp{\ECMV_1}{\ECMV_2}}{\ZCApR{\ECMV_1}{\ZCCursor{\ECMV_2}}}{2} } \inferrule[AEMApParent1]{ }{ - \ASEMParent{\ZApL{\ZCursor{\ECMV_1}}{\ECMV_2}}{\ECAp{\ECMV_1}{\ECMV_2}} + \ASEMParent{\ZCApL{\ZCCursor{\ECMV_1}}{\ECMV_2}}{\ECAp{\ECMV_1}{\ECMV_2}} } \inferrule[AEMApParent2]{ }{ - \ASEMParent{\ZApR{\ECMV_1}{\ZCursor{\ECMV_2}}}{\ECAp{\ECMV_1}{\ECMV_2}} + \ASEMParent{\ZCApR{\ECMV_1}{\ZCCursor{\ECMV_2}}}{\ECAp{\ECMV_1}{\ECMV_2}} } \inferrule[AEMLetChild1]{ }{ - \ASEMChild{\ECLet{x}{\ECMV_1}{\ECMV_2}}{\ZLetL{x}{\ZCursor{\ECMV_1}}{\ECMV_2}}{1} + \ASEMChild{\ECLet{x}{\ECMV_1}{\ECMV_2}}{\ZCLetL{x}{\ZCCursor{\ECMV_1}}{\ECMV_2}}{1} } \inferrule[AEMLetChild2]{ }{ - \ASEMChild{\ECLet{x}{\ECMV_1}{\ECMV_2}}{\ZLetR{x}{\ECMV_1}{\ZCursor{\ECMV_2}}}{2} + \ASEMChild{\ECLet{x}{\ECMV_1}{\ECMV_2}}{\ZCLetR{x}{\ECMV_1}{\ZCCursor{\ECMV_2}}}{2} } \inferrule[AEMLetParent1]{ }{ - \ASEMParent{\ZLetL{x}{\ZCursor{\ECMV_1}}{\ECMV_2}}{\ECLet{x}{\ECMV_1}{\ECMV_2}} + \ASEMParent{\ZCLetL{x}{\ZCCursor{\ECMV_1}}{\ECMV_2}}{\ECLet{x}{\ECMV_1}{\ECMV_2}} } \inferrule[AEMLetParent2]{ }{ - \ASEMParent{\ZLetR{x}{\ECMV_1}{\ZCursor{\ECMV_2}}}{\ECLet{x}{\ECMV_1}{\ECMV_2}} + \ASEMParent{\ZCLetR{x}{\ECMV_1}{\ZCCursor{\ECMV_2}}}{\ECLet{x}{\ECMV_1}{\ECMV_2}} } \inferrule[AEMPlusChild1]{ }{ - \ASEMChild{\ECPlus{\ECMV_1}{\ECMV_2}}{\ZPlusL{\ZCursor{\ECMV_1}}{\ECMV_2}}{1} + \ASEMChild{\ECPlus{\ECMV_1}{\ECMV_2}}{\ZCPlusL{\ZCCursor{\ECMV_1}}{\ECMV_2}}{1} } \inferrule[AEMPlusChild2]{ }{ - \ASEMChild{\ECPlus{\ECMV_1}{\ECMV_2}}{\ZPlusR{\ECMV_1}{\ZCursor{\ECMV_2}}}{2} + \ASEMChild{\ECPlus{\ECMV_1}{\ECMV_2}}{\ZCPlusR{\ECMV_1}{\ZCCursor{\ECMV_2}}}{2} } \inferrule[AEMPlusParent1]{ }{ - \ASEMParent{\ZPlusL{\ZCursor{\ECMV_1}}{\ECMV_2}}{\ECPlus{\ECMV_1}{\ECMV_2}} + \ASEMParent{\ZCPlusL{\ZCCursor{\ECMV_1}}{\ECMV_2}}{\ECPlus{\ECMV_1}{\ECMV_2}} } \inferrule[AEMPlusParent2]{ }{ - \ASEMParent{\ZPlusR{\ECMV_1}{\ZCursor{\ECMV_2}}}{\ECPlus{\ECMV_1}{\ECMV_2}} + \ASEMParent{\ZCPlusR{\ECMV_1}{\ZCCursor{\ECMV_2}}}{\ECPlus{\ECMV_1}{\ECMV_2}} } \inferrule[AEMIfChild1]{ }{ - \ASEMChild{\ECIf{\ECMV_1}{\ECMV_2}{\ECMV_3}}{\ZIfC{\ZCursor{\ECMV_1}}{\ECMV_2}{\ECMV_3}}{1} + \ASEMChild{\ECIf{\ECMV_1}{\ECMV_2}{\ECMV_3}}{\ZCIfC{\ZCCursor{\ECMV_1}}{\ECMV_2}{\ECMV_3}}{1} } \inferrule[AEMIfChild2]{ }{ - \ASEMChild{\ECIf{\ECMV_1}{\ECMV_2}{\ECMV_3}}{\ZIfL{\ECMV_1}{\ZCursor{\ECMV_2}}{\ECMV_3}}{2} + \ASEMChild{\ECIf{\ECMV_1}{\ECMV_2}{\ECMV_3}}{\ZCIfL{\ECMV_1}{\ZCCursor{\ECMV_2}}{\ECMV_3}}{2} } \inferrule[AEMIfChild3]{ }{ - \ASEMChild{\ECIf{\ECMV_1}{\ECMV_2}{\ECMV_3}}{\ZIfR{\ECMV_1}{\ECMV_2}{\ZCursor{\ECMV_3}}}{3} + \ASEMChild{\ECIf{\ECMV_1}{\ECMV_2}{\ECMV_3}}{\ZCIfR{\ECMV_1}{\ECMV_2}{\ZCCursor{\ECMV_3}}}{3} } \inferrule[AEMIfParent1]{ }{ - \ASEMParent{\ZIfC{\ZCursor{\ECMV_1}}{\ECMV_2}{\ECMV_3}}{\ECIf{\ECMV_1}{\ECMV_2}{\ECMV_3}} + \ASEMParent{\ZCIfC{\ZCCursor{\ECMV_1}}{\ECMV_2}{\ECMV_3}}{\ECIf{\ECMV_1}{\ECMV_2}{\ECMV_3}} } \inferrule[AEMIfParent2]{ }{ - \ASEMParent{\ZIfL{\ECMV_1}{\ZCursor{\ECMV_2}}{\ECMV_3}}{\ECIf{\ECMV_1}{\ECMV_2}{\ECMV_3}} + \ASEMParent{\ZCIfL{\ECMV_1}{\ZCCursor{\ECMV_2}}{\ECMV_3}}{\ECIf{\ECMV_1}{\ECMV_2}{\ECMV_3}} } \inferrule[AEMIfParent3]{ }{ - \ASEMParent{\ZIfR{\ECMV_1}{\ECMV_2}{\ZCursor{\ECMV_3}}}{\ECIf{\ECMV_1}{\ECMV_2}{\ECMV_3}} + \ASEMParent{\ZCIfR{\ECMV_1}{\ECMV_2}{\ZCCursor{\ECMV_3}}}{\ECIf{\ECMV_1}{\ECMV_2}{\ECMV_3}} } \inferrule[AEMInconsistentTypesChild]{ - \ASEMChild{\ZMV}{\ZMV'}{\MChildNMV} + \ASEMChild{\ZCMV}{\ZCMV'}{\MChildNMV} }{ - \ASEMChild{\ZInconType{\ZMV}}{\ZInconType{\ZMV'}}{\MChildNMV} + \ASEMChild{\ZCInconType{\ZCMV}}{\ZCInconType{\ZCMV'}}{\MChildNMV} } \inferrule[AEMInconsistentTypesParent]{ - \ASEMParent{\ZMV}{\ZMV'} + \ASEMParent{\ZCMV}{\ZCMV'} }{ - \ASEMParent{\ZInconType{\ZMV}}{\ZInconType{\ZMV'}} + \ASEMParent{\ZCInconType{\ZCMV}}{\ZCInconType{\ZCMV'}} } \inferrule[AEMInconsistentBranchesChild1]{ }{ - \ASEMChild{\ECInconBr{\ECMV_1}{\ECMV_2}{\ECMV_3}}{\ZInconBrC{\ZCursor{\ECMV_1}}{\ECMV_2}{\ECMV_3}}{1} + \ASEMChild{\ECInconBr{\ECMV_1}{\ECMV_2}{\ECMV_3}}{\ZCInconBrC{\ZCCursor{\ECMV_1}}{\ECMV_2}{\ECMV_3}}{1} } \inferrule[AEMInconsistentBranchesChild2]{ }{ - \ASEMChild{\ECInconBr{\ECMV_1}{\ECMV_2}{\ECMV_3}}{\ZInconBrL{\ECMV_1}{\ZCursor{\ECMV_2}}{\ECMV_3}}{2} + \ASEMChild{\ECInconBr{\ECMV_1}{\ECMV_2}{\ECMV_3}}{\ZCInconBrL{\ECMV_1}{\ZCCursor{\ECMV_2}}{\ECMV_3}}{2} } \inferrule[AEMInconsistentBranchesChild3]{ }{ - \ASEMChild{\ECInconBr{\ECMV_1}{\ECMV_2}{\ECMV_3}}{\ZInconBrR{\ECMV_1}{\ECMV_2}{\ZCursor{\ECMV_3}}}{3} + \ASEMChild{\ECInconBr{\ECMV_1}{\ECMV_2}{\ECMV_3}}{\ZCInconBrR{\ECMV_1}{\ECMV_2}{\ZCCursor{\ECMV_3}}}{3} } \inferrule[AEMInconsistentBranchesParent1]{ }{ - \ASEMParent{\ZInconBrC{\ZCursor{\ECMV_1}}{\ECMV_2}{\ECMV_3}}{\ECInconBr{\ECMV_1}{\ECMV_2}{\ECMV_3}} + \ASEMParent{\ZCInconBrC{\ZCCursor{\ECMV_1}}{\ECMV_2}{\ECMV_3}}{\ECInconBr{\ECMV_1}{\ECMV_2}{\ECMV_3}} } \inferrule[AEMInconsistentBranchesParent2]{ }{ - \ASEMParent{\ZInconBrC{\ECMV_1}{\ZCursor{\ECMV_2}}{\ECMV_3}}{\ECInconBr{\ECMV_1}{\ECMV_2}{\ECMV_3}} + \ASEMParent{\ZCInconBrC{\ECMV_1}{\ZCCursor{\ECMV_2}}{\ECMV_3}}{\ECInconBr{\ECMV_1}{\ECMV_2}{\ECMV_3}} } \inferrule[AEMInconsistentBranchesParent3]{ }{ - \ASEMParent{\ZInconBrC{\ECMV_1}{\ECMV_2}{\ZCursor{\ECMV_3}}}{\ECInconBr{\ECMV_1}{\ECMV_2}{\ECMV_3}} + \ASEMParent{\ZCInconBrC{\ECMV_1}{\ECMV_2}{\ZCCursor{\ECMV_3}}}{\ECInconBr{\ECMV_1}{\ECMV_2}{\ECMV_3}} } \end{mathparpagebreakable} \subsubsection{Synthetic expression actions} \label{sec:typed-synthetic-expression-actions} -\judgbox{\ensuremath{\ASAction{\ctx}{\ZMV}{\TMV}{\ZMV'}{\TMV'}{\AMV}}} +\judgbox{\ensuremath{\ASAction{\ctx}{\ZCMV}{\TMV}{\ZCMV'}{\TMV'}{\AMV}}} \paragraph{Movement} \begin{mathpar} \inferrule[ASEMove]{ - \ASEMove{\ZMV}{\ZMV'}{\MMV} + \ASEMove{\ZCMV}{\ZCMV'}{\MMV} }{ - \ASMove{\ctx}{\ZMV}{\TMV}{\ZMV'}{\TMV}{\MMV} + \ASMove{\ctx}{\ZCMV}{\TMV}{\ZCMV'}{\TMV}{\MMV} } \end{mathpar} @@ -432,93 +432,93 @@ \subsubsection{Synthetic expression actions} \inferrule[ASEConVar]{ \inCtx{\ctx}{x}{\TMV} }{ - \ASCon{\ctx}{\ZCursor{\ECEHole}}{\TUnknown}{\ZCursor{x}}{\TMV}{\SVar{x}} + \ASCon{\ctx}{\ZCCursor{\ECEHole}}{\TUnknown}{\ZCCursor{x}}{\TMV}{\SVar{x}} } \inferrule[ASEConFree]{ \notInCtx{\ctx}{x} }{ - \ASCon{\ctx}{\ZCursor{\ECEHole}}{\TUnknown}{\ZCursor{\ZFree{x}}}{\TUnknown}{\SVar{x}} + \ASCon{\ctx}{\ZCCursor{\ECEHole}}{\TUnknown}{\ZCCursor{\ZCFree{x}}}{\TUnknown}{\SVar{x}} } \inferrule[ASEConLam]{ \ctxSynFixedInto{\extendCtx{\ctx}{x}{\TUnknown}}{\erase{\ECMV}}{\ECMV'}{\TMV'} }{ - \ASCon{\ctx}{\ZCursor{\ECMV}}{\TMV}{\ZLamT{x}{\ZTCursor{\TUnknown}}{\ECMV'}}{\TArrow{\TUnknown}{\TMV'}}{\SLam{x}} + \ASCon{\ctx}{\ZCCursor{\ECMV}}{\TMV}{\ZCLamT{x}{\ZTCursor{\TUnknown}}{\ECMV'}}{\TArrow{\TUnknown}{\TMV'}}{\SLam{x}} } \inferrule[ASEConApL1]{ \matchedArrow{\TMV}{\TMV_1}{\TMV_2} }{ - \ASCon{\ctx}{\ZCursor{\ECMV}}{\TMV}{\ZApL{\ECInconType{\ECMV}}{\ZCursor{\ECEHole}}}{\TMV_2}{\SApL} + \ASCon{\ctx}{\ZCCursor{\ECMV}}{\TMV}{\ZCApL{\ECInconType{\ECMV}}{\ZCCursor{\ECEHole}}}{\TMV_2}{\SApL} } \inferrule[ASEConApL2]{ \notMatchedArrow{\TMV} }{ - \ASCon{\ctx}{\ZCursor{\ECMV}}{\TMV}{\ZApL{\ECInconType{\ECMV}}{\ZCursor{\ECEHole}}}{\TUnknown}{\SApL} + \ASCon{\ctx}{\ZCCursor{\ECMV}}{\TMV}{\ZCApL{\ECInconType{\ECMV}}{\ZCCursor{\ECEHole}}}{\TUnknown}{\SApL} } \inferrule[ASEConApR]{ }{ - \ASCon{\ctx}{\ZCursor{\ECMV}}{\TMV}{\ZApR{\ZCursor{\ECEHole}}{\ECMV}}{\TUnknown}{\SApR} + \ASCon{\ctx}{\ZCCursor{\ECMV}}{\TMV}{\ZCApR{\ZCCursor{\ECEHole}}{\ECMV}}{\TUnknown}{\SApR} } \inferrule[ASEConLet1]{ }{ - \ASCon{\ctx}{\ZCursor{\ECMV}}{\TMV}{\ZLetL{x}{\ECMV}{\ZCursor{\ECEHole}}}{\TUnknown}{\SLetL{x}} + \ASCon{\ctx}{\ZCCursor{\ECMV}}{\TMV}{\ZCLetL{x}{\ECMV}{\ZCCursor{\ECEHole}}}{\TUnknown}{\SLetL{x}} } \inferrule[ASEConLet2]{ \ctxSynFixedInto{\extendCtx{\ctx}{x}{\TUnknown}}{\erase{\ECMV}}{\ECMV'}{\TMV'} }{ - \ASCon{\ctx}{\ZCursor{\ECMV}}{\TMV}{\ZLetR{x}{\ZCursor{\ECEHole}}{\ECMV'}}{\TMV'}{\SLetL{x}} + \ASCon{\ctx}{\ZCCursor{\ECMV}}{\TMV}{\ZCLetR{x}{\ZCCursor{\ECEHole}}{\ECMV'}}{\TMV'}{\SLetL{x}} } \inferrule[ASEConNum]{ }{ - \ASCon{\ctx}{\ZCursor{\ECEHole}}{\TUnknown}{\ZCursor{\ENumMV}}{\TNum}{\SLit{\ENumMV}} + \ASCon{\ctx}{\ZCCursor{\ECEHole}}{\TUnknown}{\ZCCursor{\ENumMV}}{\TNum}{\SLit{\ENumMV}} } \inferrule[ASEConPlusL1]{ \consistent{\TMV}{\TNum} }{ - \ASCon{\ctx}{\ZCursor{\ECMV}}{\TMV}{\ZPlusR{\ECMV}{\ZCursor{\ECEHole}}}{\TNum}{\SPlusL} + \ASCon{\ctx}{\ZCCursor{\ECMV}}{\TMV}{\ZCPlusR{\ECMV}{\ZCCursor{\ECEHole}}}{\TNum}{\SPlusL} } \inferrule[ASEConPlusL2]{ \inconsistent{\TMV}{\TNum} }{ - \ASCon{\ctx}{\ZCursor{\ECMV}}{\TMV}{\ZPlusR{\ECInconType{\ECMV}}{\ZCursor{\ECEHole}}}{\TNum}{\SPlusL} + \ASCon{\ctx}{\ZCCursor{\ECMV}}{\TMV}{\ZCPlusR{\ECInconType{\ECMV}}{\ZCCursor{\ECEHole}}}{\TNum}{\SPlusL} } \\ \inferrule[ASEConPlusR1]{ \consistent{\TMV}{\TNum} }{ - \ASCon{\ctx}{\ZCursor{\ECMV}}{\TMV}{\ZPlusL{\ZCursor{\ECEHole}}{\ECMV}}{\TNum}{\SPlusR} + \ASCon{\ctx}{\ZCCursor{\ECMV}}{\TMV}{\ZCPlusL{\ZCCursor{\ECEHole}}{\ECMV}}{\TNum}{\SPlusR} } \inferrule[ASEConPlusR2]{ \inconsistent{\TMV}{\TNum} }{ - \ASCon{\ctx}{\ZCursor{\ECMV}}{\TMV}{\ZPlusL{\ZCursor{\ECEHole}}{\ECInconType{\ECMV}}}{\TNum}{\SPlusR} + \ASCon{\ctx}{\ZCCursor{\ECMV}}{\TMV}{\ZCPlusL{\ZCCursor{\ECEHole}}{\ECInconType{\ECMV}}}{\TNum}{\SPlusR} } \inferrule[ASEConIfC1]{ \consistent{\TMV}{\TBool} }{ - \ASCon{\ctx}{\ZCursor{\ECMV}}{\TMV}{\ZIfL{\ECMV}{\ZCursor{\ECEHole}}{\ECEHole}}{\TUnknown}{\SIfC} + \ASCon{\ctx}{\ZCCursor{\ECMV}}{\TMV}{\ZCIfL{\ECMV}{\ZCCursor{\ECEHole}}{\ECEHole}}{\TUnknown}{\SIfC} } \inferrule[ASEConIfC2]{ \inconsistent{\TMV}{\TBool} }{ - \ASCon{\ctx}{\ZCursor{\ECMV}}{\TMV}{\ZIfL{\ECInconType{\ECMV}}{\ZCursor{\ECEHole}}{\ECEHole}}{\TUnknown}{\SIfC} + \ASCon{\ctx}{\ZCCursor{\ECMV}}{\TMV}{\ZCIfL{\ECInconType{\ECMV}}{\ZCCursor{\ECEHole}}{\ECEHole}}{\TUnknown}{\SIfC} } \inferrule[ASEConIfL]{ }{ - \ASCon{\ctx}{\ZCursor{\ECMV}}{\TMV}{\ZIfC{\ZCursor{\ECEHole}}{\ECMV}{\ECEHole}}{\TMV}{\SIfL} + \ASCon{\ctx}{\ZCCursor{\ECMV}}{\TMV}{\ZCIfC{\ZCCursor{\ECEHole}}{\ECMV}{\ECEHole}}{\TMV}{\SIfL} } \inferrule[ASEConIfR]{ }{ - \ASCon{\ctx}{\ZCursor{\ECMV}}{\TMV}{\ZIfC{\ZCursor{\ECEHole}}{\ECEHole}{\ECMV}}{\TMV}{\SIfR} + \ASCon{\ctx}{\ZCCursor{\ECMV}}{\TMV}{\ZCIfC{\ZCCursor{\ECEHole}}{\ECEHole}{\ECMV}}{\TMV}{\SIfR} } \end{mathparpagebreakable} @@ -528,7 +528,7 @@ \subsubsection{Synthetic expression actions} \AUTAction{\ZTMV_1}{\ZTMV_1'}{\AMV} \\ \equal{\cursorErase{\ZTMV_1}}{\cursorErase{\ZTMV_1'}} }{ - \ASEAction{\ctx}{\ZLamT{x}{\ZTMV_1}{\ECMV}}{\TArrow{\cursorErase{\ZTMV_1}}{\TMV_2}}{\ZLamT{x}{\ZTMV_1'}{\ECMV}}{\TArrow{\cursorErase{\ZTMV_1}}{\TMV_2}}{\AMV} + \ASEAction{\ctx}{\ZCLamT{x}{\ZTMV_1}{\ECMV}}{\TArrow{\cursorErase{\ZTMV_1}}{\TMV_2}}{\ZCLamT{x}{\ZTMV_1'}{\ECMV}}{\TArrow{\cursorErase{\ZTMV_1}}{\TMV_2}}{\AMV} } \inferrule[ASEZipLamT2]{ @@ -536,242 +536,242 @@ \subsubsection{Synthetic expression actions} \notEqual{\cursorErase{\ZTMV_1}}{\cursorErase{\ZTMV_1'}} \\ \ctxSynFixedInto{\extendCtx{\ctx}{x}{\cursorErase{\ZTMV_1'}}}{\erase{\ECMV}}{\ECMV'}{\TMV_2'} }{ - \ASEAction{\ctx}{\ZLamT{x}{\ZTMV_1}{\ECMV}}{\TArrow{\cursorErase{\ZTMV_1}}{\TMV_2}}{\ZLamT{x}{\ZTMV_1'}{\ECMV'}}{\TArrow{\cursorErase{\ZTMV_1'}}{\TMV_2'}}{\AMV} + \ASEAction{\ctx}{\ZCLamT{x}{\ZTMV_1}{\ECMV}}{\TArrow{\cursorErase{\ZTMV_1}}{\TMV_2}}{\ZCLamT{x}{\ZTMV_1'}{\ECMV'}}{\TArrow{\cursorErase{\ZTMV_1'}}{\TMV_2'}}{\AMV} } \inferrule[ASEZipLamE]{ - \ASEAction{\extendCtx{\ctx}{x}{\TMV_1}}{\ZMV}{\TMV_2}{\ZMV'}{\TMV_2'}{\AMV} + \ASEAction{\extendCtx{\ctx}{x}{\TMV_1}}{\ZCMV}{\TMV_2}{\ZCMV'}{\TMV_2'}{\AMV} }{ - \ASEAction{\ctx}{\ZLamE{x}{\TMV_1}{\ZMV}}{\TArrow{\TMV_1}{\TMV_2}}{\ZLamE{x}{\TMV_1}{\ZMV'}}{\TArrow{\ZTMV_1}{\TMV_2'}}{\AMV} + \ASEAction{\ctx}{\ZCLamE{x}{\TMV_1}{\ZCMV}}{\TArrow{\TMV_1}{\TMV_2}}{\ZCLamE{x}{\TMV_1}{\ZCMV'}}{\TArrow{\ZTMV_1}{\TMV_2'}}{\AMV} } \inferrule[ASEZipApL1]{ - \ctxSynTypeM{\ctx}{\cursorErase{\ZMV_1}}{\TMV_1} \\ - \ASEAction{\ctx}{\ZMV_1}{\TMV_1}{\ZMV_1'}{\TMV_1'}{\AMV} \\\\ + \ctxSynTypeM{\ctx}{\cursorErase{\ZCMV_1}}{\TMV_1} \\ + \ASEAction{\ctx}{\ZCMV_1}{\TMV_1}{\ZCMV_1'}{\TMV_1'}{\AMV} \\\\ \matchedArrow{\TMV_1'}{\TMV_2}{\TMV_3} \\ \ctxAnaType{\ctx}{\ECMV_2}{\TMV_2} }{ - \ASEAction{\ctx}{\ZApL{\ZMV_1}{\ECMV_2}}{\TMV}{\ZApL{\ZMV_1'}{\ECMV_2}}{\TMV_3}{\AMV} + \ASEAction{\ctx}{\ZCApL{\ZCMV_1}{\ECMV_2}}{\TMV}{\ZCApL{\ZCMV_1'}{\ECMV_2}}{\TMV_3}{\AMV} } \inferrule[ASEZipApL2]{ - \ctxSynTypeM{\ctx}{\cursorErase{\ZMV_1}}{\TMV_1} \\ - \ASEAction{\ctx}{\ZMV_1}{\TMV_1}{\ZMV_1'}{\TMV_1'}{\AMV} \\\\ + \ctxSynTypeM{\ctx}{\cursorErase{\ZCMV_1}}{\TMV_1} \\ + \ASEAction{\ctx}{\ZCMV_1}{\TMV_1}{\ZCMV_1'}{\TMV_1'}{\AMV} \\\\ \matchedArrow{\TMV_1'}{\TMV_2}{\TMV_3} \\ \ctxNotAnaType{\ctx}{\ECMV_2}{\TMV_2} }{ - \ASEAction{\ctx}{\ZApL{\ZMV_1}{\ECMV_2}}{\TMV}{\ZApL{\ZMV_1'}{\ECInconType{\ECMV_2}}}{\TMV_3}{\AMV} + \ASEAction{\ctx}{\ZCApL{\ZCMV_1}{\ECMV_2}}{\TMV}{\ZCApL{\ZCMV_1'}{\ECInconType{\ECMV_2}}}{\TMV_3}{\AMV} } \inferrule[ASEZipApL3]{ - \ctxSynTypeM{\ctx}{\cursorErase{\ZMV_1}}{\TMV_1} \\ - \ASEAction{\ctx}{\ZMV}{\TMV_1}{\ZMV'}{\TMV_1'}{\AMV} \\\\ + \ctxSynTypeM{\ctx}{\cursorErase{\ZCMV_1}}{\TMV_1} \\ + \ASEAction{\ctx}{\ZCMV}{\TMV_1}{\ZCMV'}{\TMV_1'}{\AMV} \\\\ \notMatchedArrow{\TMV_1'} }{ - \ASEAction{\ctx}{\ZApL{\ZMV_1}{\ECMV_2}}{\TMV}{\ZApL{\ECInconType{\ZMV_1'}}{\ECMV_2}}{\TUnknown}{\AMV} + \ASEAction{\ctx}{\ZCApL{\ZCMV_1}{\ECMV_2}}{\TMV}{\ZCApL{\ECInconType{\ZCMV_1'}}{\ECMV_2}}{\TUnknown}{\AMV} } \inferrule[ASEZipApL4]{ - \ctxSynTypeM{\ctx}{\cursorErase{\ZMV_1}}{\TMV_1} \\ - \ASEAction{\ctx}{\ZMV_1}{\TMV_1}{\ZMV_1'}{\TMV_1'}{\AMV} \\\\ + \ctxSynTypeM{\ctx}{\cursorErase{\ZCMV_1}}{\TMV_1} \\ + \ASEAction{\ctx}{\ZCMV_1}{\TMV_1}{\ZCMV_1'}{\TMV_1'}{\AMV} \\\\ \matchedArrow{\TMV_1'}{\TMV_2}{\TMV_3} \\ \ctxAnaType{\ctx}{\ECMV_2}{\TMV_2} }{ - \ASEAction{\ctx}{\ZApL{\ECInconType{\ZMV_1}}{\ECMV_2}}{\TUnknown}{\ZApL{\ZMV_1'}{\ECMV_2}}{\TMV_3}{\AMV} + \ASEAction{\ctx}{\ZCApL{\ECInconType{\ZCMV_1}}{\ECMV_2}}{\TUnknown}{\ZCApL{\ZCMV_1'}{\ECMV_2}}{\TMV_3}{\AMV} } \inferrule[ASEZipApL5]{ - \ctxSynTypeM{\ctx}{\cursorErase{\ZMV_1}}{\TMV_1} \\ - \ASEAction{\ctx}{\ZMV_1}{\TMV_1}{\ZMV_1'}{\TMV_1'}{\AMV} \\\\ + \ctxSynTypeM{\ctx}{\cursorErase{\ZCMV_1}}{\TMV_1} \\ + \ASEAction{\ctx}{\ZCMV_1}{\TMV_1}{\ZCMV_1'}{\TMV_1'}{\AMV} \\\\ \matchedArrow{\TMV_1'}{\TMV_2}{\TMV_3} \\ \ctxNotAnaType{\ctx}{\ECMV_2}{\TMV_2} }{ - \ASEAction{\ctx}{\ZApL{\ECInconType{\ZMV_1}}{\ECMV_2}}{\TUnknown}{\ZApL{\ZMV_1'}{\ECInconType{\ECMV_2}}}{\TMV_3}{\AMV} + \ASEAction{\ctx}{\ZCApL{\ECInconType{\ZCMV_1}}{\ECMV_2}}{\TUnknown}{\ZCApL{\ZCMV_1'}{\ECInconType{\ECMV_2}}}{\TMV_3}{\AMV} } \inferrule[ASEZipApL6]{ - \ctxSynTypeM{\ctx}{\cursorErase{\ZMV_1}}{\TMV_1} \\ - \ASEAction{\ctx}{\ZMV_1}{\TMV_1}{\ZMV_1'}{\TMV_1'}{\AMV} \\\\ + \ctxSynTypeM{\ctx}{\cursorErase{\ZCMV_1}}{\TMV_1} \\ + \ASEAction{\ctx}{\ZCMV_1}{\TMV_1}{\ZCMV_1'}{\TMV_1'}{\AMV} \\\\ \notMatchedArrow{\TMV_1'} }{ - \ASEAction{\ctx}{\ZApL{\ECInconType{\ZMV_1}}{\ECMV_2}}{\TUnknown}{\ZApL{\ECInconType{\ZMV_1'}}{\ECMV_2}}{\TUnknown}{\AMV} + \ASEAction{\ctx}{\ZCApL{\ECInconType{\ZCMV_1}}{\ECMV_2}}{\TUnknown}{\ZCApL{\ECInconType{\ZCMV_1'}}{\ECMV_2}}{\TUnknown}{\AMV} } \inferrule[ASEZipApR]{ \ctxSynTypeM{\ctx}{\ECMV_1}{\TMV_1} \\ \matchedArrow{\TMV_1}{\TMV_2}{\TMV_3} \\ - \AAEAction{\ctx}{\ZMV_2}{\ZMV_2'}{\TMV_2}{\AMV} + \AAEAction{\ctx}{\ZCMV_2}{\ZCMV_2'}{\TMV_2}{\AMV} }{ - \ASEAction{\ctx}{\ZApR{\ECMV_1}{\ZMV_2}}{\TMV}{\ZApR{\ECMV_1}{\ZMV_2'}}{\TMV_3}{\AMV} + \ASEAction{\ctx}{\ZCApR{\ECMV_1}{\ZCMV_2}}{\TMV}{\ZCApR{\ECMV_1}{\ZCMV_2'}}{\TMV_3}{\AMV} } \inferrule[ASEZipLetL1]{ - \ctxSynTypeM{\ctx}{\cursorErase{\ZMV_1}}{\TMV_1} \\ - \ASEAction{\ctx}{\ZMV_1}{\TMV_1}{\ZMV_1'}{\TMV_1'}{\AMV} \\ + \ctxSynTypeM{\ctx}{\cursorErase{\ZCMV_1}}{\TMV_1} \\ + \ASEAction{\ctx}{\ZCMV_1}{\TMV_1}{\ZCMV_1'}{\TMV_1'}{\AMV} \\ \consistent{\TMV_1}{\TMV_1'} }{ - \ASEAction{\ctx}{\ZLetL{x}{\ZMV_1}{\ECMV_2}}{\TMV_2}{\ZLetL{x}{\ZMV_1'}{\ECMV_2}}{\TMV_2}{\AMV} + \ASEAction{\ctx}{\ZCLetL{x}{\ZCMV_1}{\ECMV_2}}{\TMV_2}{\ZCLetL{x}{\ZCMV_1'}{\ECMV_2}}{\TMV_2}{\AMV} } \inferrule[ASEZipLetL2]{ - \ctxSynTypeM{\ctx}{\cursorErase{\ZMV_1}}{\TMV_1} \\ - \ASEAction{\ctx}{\ZMV_1}{\TMV_1}{\ZMV_1'}{\TMV_1'}{\AMV} \\\\ + \ctxSynTypeM{\ctx}{\cursorErase{\ZCMV_1}}{\TMV_1} \\ + \ASEAction{\ctx}{\ZCMV_1}{\TMV_1}{\ZCMV_1'}{\TMV_1'}{\AMV} \\\\ \inconsistent{\TMV_1}{\TMV_1'} \\ \ctxSynFixedInto{\extendCtx{\ctx}{x}{\TMV_1'}}{\erase{\ECMV_2}}{\ECMV_2'}{\TMV_2'} }{ - \ASEAction{\ctx}{\ZLetL{x}{\ZMV_1}{\ECMV_2}}{\TMV_2}{\ZLetL{x}{\ZMV_1'}{\ECMV_2'}}{\TMV_2'}{\AMV} + \ASEAction{\ctx}{\ZCLetL{x}{\ZCMV_1}{\ECMV_2}}{\TMV_2}{\ZCLetL{x}{\ZCMV_1'}{\ECMV_2'}}{\TMV_2'}{\AMV} } \inferrule[ASEZipLetR]{ \ctxSynTypeM{\ctx}{\ECMV_1}{\TMV_1} \\ - \ctxSynTypeM{\extendCtx{\ctx}{x}{\TMV_1}}{\cursorErase{\ZMV_2}}{\TMV_2} \\\\ - \ASEAction{\extendCtx{\ctx}{x}{\TMV_1}}{\ZMV_2}{\TMV_2}{\ZMV_2'}{\TMV_2'}{\AMV} + \ctxSynTypeM{\extendCtx{\ctx}{x}{\TMV_1}}{\cursorErase{\ZCMV_2}}{\TMV_2} \\\\ + \ASEAction{\extendCtx{\ctx}{x}{\TMV_1}}{\ZCMV_2}{\TMV_2}{\ZCMV_2'}{\TMV_2'}{\AMV} }{ - \ASEAction{\ctx}{\ZLetR{x}{\ECMV_1}{\ZMV_2}}{\TMV_2}{\ZLetR{x}{\ECMV_1}{\ZMV_2'}}{\TMV_2'}{\AMV} + \ASEAction{\ctx}{\ZCLetR{x}{\ECMV_1}{\ZCMV_2}}{\TMV_2}{\ZCLetR{x}{\ECMV_1}{\ZCMV_2'}}{\TMV_2'}{\AMV} } \inferrule[ASEZipPlusL]{ - \AAEAction{\ctx}{\ZMV}{\ZMV'}{\TNum}{\AMV} + \AAEAction{\ctx}{\ZCMV}{\ZCMV'}{\TNum}{\AMV} }{ - \ASEAction{\ctx}{\ZPlusL{\ZMV}{\ECMV}}{\TNum}{\ZPlusL{\ZMV'}{\ECMV}}{\TNum}{\AMV} + \ASEAction{\ctx}{\ZCPlusL{\ZCMV}{\ECMV}}{\TNum}{\ZCPlusL{\ZCMV'}{\ECMV}}{\TNum}{\AMV} } \inferrule[ASEZipPlusR]{ - \AAEAction{\ctx}{\ZMV}{\ZMV'}{\TNum}{\AMV} + \AAEAction{\ctx}{\ZCMV}{\ZCMV'}{\TNum}{\AMV} }{ - \ASEAction{\ctx}{\ZPlusR{\ECMV}{\ZMV}}{\TNum}{\ZPlusR{\ECMV}{\ZMV'}}{\TNum}{\AMV} + \ASEAction{\ctx}{\ZCPlusR{\ECMV}{\ZCMV}}{\TNum}{\ZCPlusR{\ECMV}{\ZCMV'}}{\TNum}{\AMV} } \inferrule[ASEZipIfC]{ - \AAEAction{\ctx}{\ZMV}{\ZMV'}{\TBool}{\AMV} + \AAEAction{\ctx}{\ZCMV}{\ZCMV'}{\TBool}{\AMV} }{ - \ASEAction{\ctx}{\ZIfC{\ZMV}{\ECMV_1}{\ECMV_2}}{\TMV}{\ZIfC{\ZMV'}{\ECMV_1}{\ECMV_2}}{\TMV}{\AMV} + \ASEAction{\ctx}{\ZCIfC{\ZCMV}{\ECMV_1}{\ECMV_2}}{\TMV}{\ZCIfC{\ZCMV'}{\ECMV_1}{\ECMV_2}}{\TMV}{\AMV} } \inferrule[ASEZipIfL1]{ - \ctxSynTypeM{\ctx}{\cursorErase{\ZMV}}{\TMV_1} \\ + \ctxSynTypeM{\ctx}{\cursorErase{\ZCMV}}{\TMV_1} \\ \ctxSynTypeM{\ctx}{\ECMV_2}{\TMV_2} \\\\ - \ASEAction{\ctx}{\ZMV}{\TMV_1}{\ZMV'}{\TMV_1'}{\AMV} \\ + \ASEAction{\ctx}{\ZCMV}{\TMV_1}{\ZCMV'}{\TMV_1'}{\AMV} \\ \consistent{\TMV_1'}{\TMV_2} }{ - \ASEAction{\ctx}{\ZIfL{\ECMV_1}{\ZMV}{\ECMV_2}}{\TMV}{\ZIfL{\ECMV_1}{\ZMV'}{\ECMV_2}}{\TMeet{\TMV_1'}{\TMV_2}}{\AMV} + \ASEAction{\ctx}{\ZCIfL{\ECMV_1}{\ZCMV}{\ECMV_2}}{\TMV}{\ZCIfL{\ECMV_1}{\ZCMV'}{\ECMV_2}}{\TMeet{\TMV_1'}{\TMV_2}}{\AMV} } \inferrule[ASEZipIfL2]{ - \ctxSynTypeM{\ctx}{\cursorErase{\ZMV}}{\TMV_1} \\ + \ctxSynTypeM{\ctx}{\cursorErase{\ZCMV}}{\TMV_1} \\ \ctxSynTypeM{\ctx}{\ECMV_2}{\TMV_2} \\\\ - \ASEAction{\ctx}{\ZMV}{\TMV_1}{\ZMV'}{\TMV_1'}{\AMV} \\ + \ASEAction{\ctx}{\ZCMV}{\TMV_1}{\ZCMV'}{\TMV_1'}{\AMV} \\ \inconsistent{\TMV_1'}{\TMV_2} }{ - \ASEAction{\ctx}{\ZIfL{\ECMV_1}{\ZMV}{\ECMV_2}}{\TMV}{\ZInconBrL{\ECMV_1}{\ZMV'}{\ECMV_2}}{\TUnknown}{\AMV} + \ASEAction{\ctx}{\ZCIfL{\ECMV_1}{\ZCMV}{\ECMV_2}}{\TMV}{\ZCInconBrL{\ECMV_1}{\ZCMV'}{\ECMV_2}}{\TUnknown}{\AMV} } \inferrule[ASEZipIfR1]{ \ctxSynTypeM{\ctx}{\ECMV_2}{\TMV_1} \\ - \ctxSynTypeM{\ctx}{\cursorErase{\ZMV}}{\TMV_2} \\\\ - \ASEAction{\ctx}{\ZMV}{\TMV_2}{\ZMV'}{\TMV_2'}{\AMV} \\ + \ctxSynTypeM{\ctx}{\cursorErase{\ZCMV}}{\TMV_2} \\\\ + \ASEAction{\ctx}{\ZCMV}{\TMV_2}{\ZCMV'}{\TMV_2'}{\AMV} \\ \consistent{\TMV_1}{\TMV_2'} }{ - \ASEAction{\ctx}{\ZIfR{\ECMV_1}{\ECMV_2}{\ZMV}}{\TMV}{\ZIfR{\ECMV_1}{\ECMV_2}{\ZMV'}}{\TMeet{\TMV_1}{\TMV_2'}}{\AMV} + \ASEAction{\ctx}{\ZCIfR{\ECMV_1}{\ECMV_2}{\ZCMV}}{\TMV}{\ZCIfR{\ECMV_1}{\ECMV_2}{\ZCMV'}}{\TMeet{\TMV_1}{\TMV_2'}}{\AMV} } \inferrule[ASEZipIfR2]{ \ctxSynTypeM{\ctx}{\ECMV_1}{\TMV_1} \\ - \ctxSynTypeM{\ctx}{\cursorErase{\ZMV}}{\TMV_2} \\\\ - \ASEAction{\ctx}{\ZMV}{\TMV_2}{\ZMV'}{\TMV_2'}{\AMV} \\ + \ctxSynTypeM{\ctx}{\cursorErase{\ZCMV}}{\TMV_2} \\\\ + \ASEAction{\ctx}{\ZCMV}{\TMV_2}{\ZCMV'}{\TMV_2'}{\AMV} \\ \inconsistent{\TMV_1}{\TMV_2'} }{ - \ASEAction{\ctx}{\ZIfR{\ECMV_1}{\ECMV_2}{\ZMV}}{\TMV}{\ZInconBrR{\ECMV_1}{\ECMV_2}{\ZMV'}}{\TUnknown}{\AMV} + \ASEAction{\ctx}{\ZCIfR{\ECMV_1}{\ECMV_2}{\ZCMV}}{\TMV}{\ZCInconBrR{\ECMV_1}{\ECMV_2}{\ZCMV'}}{\TUnknown}{\AMV} } \inferrule[ASEZipInconsistentBranchesC]{ - \AAEAction{\ctx}{\ZMV}{\ZMV'}{\TBool}{\AMV} + \AAEAction{\ctx}{\ZCMV}{\ZCMV'}{\TBool}{\AMV} }{ - \ASEAction{\ctx}{\ZInconBrC{\ZMV}{\ECMV_1}{\ECMV_2}}{\TMV}{\ZInconBrC{\ZMV'}{\ECMV_1}{\ECMV_2}}{\TMV}{\AMV} + \ASEAction{\ctx}{\ZCInconBrC{\ZCMV}{\ECMV_1}{\ECMV_2}}{\TMV}{\ZCInconBrC{\ZCMV'}{\ECMV_1}{\ECMV_2}}{\TMV}{\AMV} } \inferrule[ASEZipInconsistentBranchesL1]{ - \ASEAction{\ctx}{\ZMV}{\TMV_1}{\ZMV'}{\TMV_1'}{\AMV} \\ + \ASEAction{\ctx}{\ZCMV}{\TMV_1}{\ZCMV'}{\TMV_1'}{\AMV} \\ \ctxSynTypeM{\ctx}{\ECMV_2}{\TMV_2} \\ \consistent{\TMV_1'}{\TMV_2} }{ - \ASEAction{\ctx}{\ZInconBrL{\ECMV_1}{\ZMV}{\ECMV_2}}{\TMV}{\ZIfL{\ECMV_1}{\ZMV'}{\ECMV_2}}{\TMeet{\TMV_1'}{\TMV_2}}{\AMV} + \ASEAction{\ctx}{\ZCInconBrL{\ECMV_1}{\ZCMV}{\ECMV_2}}{\TMV}{\ZCIfL{\ECMV_1}{\ZCMV'}{\ECMV_2}}{\TMeet{\TMV_1'}{\TMV_2}}{\AMV} } \inferrule[ASEZipInconsistentBranchesL2]{ - \ASEAction{\ctx}{\ZMV}{\TMV_1}{\ZMV'}{\TMV_1'}{\AMV} \\ + \ASEAction{\ctx}{\ZCMV}{\TMV_1}{\ZCMV'}{\TMV_1'}{\AMV} \\ \ctxSynTypeM{\ctx}{\ECMV_2}{\TMV_2} \\ \inconsistent{\TMV_1'}{\TMV_2} }{ - \ASEAction{\ctx}{\ZInconBrL{\ECMV_1}{\ZMV}{\ECMV_2}}{\TMV}{\ZInconBrL{\ECMV_1}{\ZMV'}{\ECMV_2}}{\TUnknown}{\AMV} + \ASEAction{\ctx}{\ZCInconBrL{\ECMV_1}{\ZCMV}{\ECMV_2}}{\TMV}{\ZCInconBrL{\ECMV_1}{\ZCMV'}{\ECMV_2}}{\TUnknown}{\AMV} } \inferrule[ASEZipInconsistentBranchesR1]{ \ctxSynTypeM{\ctx}{\ECMV_1}{\TMV_1} \\ - \ASEAction{\ctx}{\ZMV}{\TMV_2}{\ZMV'}{\TMV_2'}{\AMV} \\ + \ASEAction{\ctx}{\ZCMV}{\TMV_2}{\ZCMV'}{\TMV_2'}{\AMV} \\ \consistent{\TMV_1}{\TMV_2'} }{ - \ASEAction{\ctx}{\ZInconBrR{\ECMV_1}{\ECMV_2}{\ZMV}}{\TMV}{\ZIfL{\ECMV_1}{\ECMV_2}{\ZMV'}}{\TMeet{\TMV_1}{\TMV_2'}}{\AMV} + \ASEAction{\ctx}{\ZCInconBrR{\ECMV_1}{\ECMV_2}{\ZCMV}}{\TMV}{\ZCIfL{\ECMV_1}{\ECMV_2}{\ZCMV'}}{\TMeet{\TMV_1}{\TMV_2'}}{\AMV} } \inferrule[ASEZipInconsistentBranchesR2]{ \ctxSynTypeM{\ctx}{\ECMV_2}{\TMV_1} \\ - \ASEAction{\ctx}{\ZMV}{\TMV_2}{\ZMV'}{\TMV_2'}{\AMV} \\ + \ASEAction{\ctx}{\ZCMV}{\TMV_2}{\ZCMV'}{\TMV_2'}{\AMV} \\ \inconsistent{\TMV_1}{\TMV_2'} }{ - \ASEAction{\ctx}{\ZInconBrR{\ECMV_1}{\ECMV_2}{\ZMV}}{\TMV}{\ZInconBrR{\ECMV_1}{\ECMV_2}{\ZMV'}}{\TUnknown}{\AMV} + \ASEAction{\ctx}{\ZCInconBrR{\ECMV_1}{\ECMV_2}{\ZCMV}}{\TMV}{\ZCInconBrR{\ECMV_1}{\ECMV_2}{\ZCMV'}}{\TUnknown}{\AMV} } \end{mathparpagebreakable} \subsubsection{Analytic expression actions} \label{sec:typed-analytic-expression-actions} -\judgbox{\ensuremath{\AAAction{\ctx}{\ZMV}{\ZMV'}{\TMV'}{\AMV}}} +\judgbox{\ensuremath{\AAAction{\ctx}{\ZCMV}{\ZCMV'}{\TMV'}{\AMV}}} \paragraph{Subsumption} \begin{mathpar} \inferrule[AAESubsume1]{ - \ctxSynTypeM{\ctx}{\cursorErase{\ZMV}}{\TMV'} \\ - \ASAction{\ctx}{\ZMV}{\TMV'}{\ZMV'}{\TMV''}{\AMV} \\\\ + \ctxSynTypeM{\ctx}{\cursorErase{\ZCMV}}{\TMV'} \\ + \ASAction{\ctx}{\ZCMV}{\TMV'}{\ZCMV'}{\TMV''}{\AMV} \\\\ \consistent{\TMV}{\TMV''} \\ - \subsumable{\cursorErase{\ZMV}} + \subsumable{\cursorErase{\ZCMV}} }{ - \AAAction{\ctx}{\ZMV}{\ZMV'}{\TMV}{\AMV} + \AAAction{\ctx}{\ZCMV}{\ZCMV'}{\TMV}{\AMV} } \inferrule[AAESubsume2]{ - \ctxSynTypeM{\ctx}{\cursorErase{\ZMV}}{\TMV'} \\ - \ASAction{\ctx}{\ZMV}{\TMV'}{\ZMV'}{\TMV''}{\AMV} \\\\ + \ctxSynTypeM{\ctx}{\cursorErase{\ZCMV}}{\TMV'} \\ + \ASAction{\ctx}{\ZCMV}{\TMV'}{\ZCMV'}{\TMV''}{\AMV} \\\\ \inconsistent{\TMV}{\TMV''} \\ - \subsumable{\cursorErase{\ZMV}} + \subsumable{\cursorErase{\ZCMV}} }{ - \AAAction{\ctx}{\ZMV}{\ZInconType{\ZMV'}}{\TMV}{\AMV} + \AAAction{\ctx}{\ZCMV}{\ZCInconType{\ZCMV'}}{\TMV}{\AMV} } \inferrule[AAEInconsistentTypes1]{ - \ctxSynTypeM{\ctx}{\cursorErase{\ZMV}}{\TMV'} \\ - \ASAction{\ctx}{\ZMV}{\TMV'}{\ZMV'}{\TMV''}{\AMV} \\\\ + \ctxSynTypeM{\ctx}{\cursorErase{\ZCMV}}{\TMV'} \\ + \ASAction{\ctx}{\ZCMV}{\TMV'}{\ZCMV'}{\TMV''}{\AMV} \\\\ \inconsistent{\TMV}{\TMV''} \\ - \subsumable{\cursorErase{\ZMV}} + \subsumable{\cursorErase{\ZCMV}} }{ - \AAAction{\ctx}{\ZInconType{\ZMV}}{\ZInconType{\ZMV'}}{\TMV}{\AMV} + \AAAction{\ctx}{\ZCInconType{\ZCMV}}{\ZCInconType{\ZCMV'}}{\TMV}{\AMV} } \inferrule[AAEInconsistentTypes2]{ - \ctxSynTypeM{\ctx}{\cursorErase{\ZMV}}{\TMV'} \\ - \ASAction{\ctx}{\ZMV}{\TMV'}{\ZMV'}{\TMV''}{\AMV} \\\\ + \ctxSynTypeM{\ctx}{\cursorErase{\ZCMV}}{\TMV'} \\ + \ASAction{\ctx}{\ZCMV}{\TMV'}{\ZCMV'}{\TMV''}{\AMV} \\\\ \consistent{\TMV}{\TMV''} \\ - \subsumable{\cursorErase{\ZMV}} + \subsumable{\cursorErase{\ZCMV}} }{ - \AAAction{\ctx}{\ZInconType{\ZMV}}{\ZMV'}{\TMV}{\AMV} + \AAAction{\ctx}{\ZCInconType{\ZCMV}}{\ZCMV'}{\TMV}{\AMV} } \end{mathpar} \paragraph{Movement} \begin{mathpar} \inferrule[AAEMove]{ - \ASEMove{\ZMV}{\ZMV'}{\MMV} + \ASEMove{\ZCMV}{\ZCMV'}{\MMV} }{ - \AAMove{\ctx}{\ZMV}{\ZMV'}{\TMV}{\MMV} + \AAMove{\ctx}{\ZCMV}{\ZCMV'}{\TMV}{\MMV} } \end{mathpar} @@ -788,33 +788,33 @@ \subsubsection{Analytic expression actions} \matchedArrow{\TMV}{\TMV_1}{\TMV_2} \\ \ctxAnaFixedInto{\extendCtx{\ctx}{x}{\TMV_1}}{\ECMV}{\ECMV'}{\TMV_2} }{ - \AACon{\ctx}{\ZCursor{\ECMV}}{\ZLamT{x}{\ZTCursor{\TMV_1}}{\ECMV'}}{\TMV}{\SLam{x}} + \AACon{\ctx}{\ZCCursor{\ECMV}}{\ZCLamT{x}{\ZTCursor{\TMV_1}}{\ECMV'}}{\TMV}{\SLam{x}} } \inferrule[AAEConLam2]{ \notMatchedArrow{\TMV} \\ \ctxAnaFixedInto{\extendCtx{\ctx}{x}{\TUnknown}}{\ECMV}{\ECMV'}{\TUnknown} }{ - \AACon{\ctx}{\ZCursor{\ECMV}}{\ZInconType{\ZLamT{x}{\ZTCursor{\TUnknown}}{\ECMV'}}}{\TMV}{\SLam{x}} + \AACon{\ctx}{\ZCCursor{\ECMV}}{\ZCInconType{\ZCLamT{x}{\ZTCursor{\TUnknown}}{\ECMV'}}}{\TMV}{\SLam{x}} } \inferrule[AAEConLetL]{ }{ - \AACon{\ctx}{\ZCursor{\ECMV}}{\ZLetL{x}{\ECMV}{\ZCursor{\ECEHole}}}{\TMV}{\SLetL{x}} + \AACon{\ctx}{\ZCCursor{\ECMV}}{\ZCLetL{x}{\ECMV}{\ZCCursor{\ECEHole}}}{\TMV}{\SLetL{x}} } \inferrule[AAEConLetR]{ \ctxAnaFixedInto{\extendCtx{\ctx}{x}{\TUnknown}}{\erase{\ECMV}}{\ECMV'}{\TMV} }{ - \AACon{\ctx}{\ZCursor{\ECMV}}{\ZLetR{x}{\ZCursor{\ECEHole}}{\ECMV'}}{\TMV}{\SLetR{x}} + \AACon{\ctx}{\ZCCursor{\ECMV}}{\ZCLetR{x}{\ZCCursor{\ECEHole}}{\ECMV'}}{\TMV}{\SLetR{x}} } \inferrule[AAEConIfL]{ }{ - \AACon{\ctx}{\ZCursor{\ECMV}}{\ZIfC{\ZCursor{\ECEHole}}{\ECMV}{\ECEHole}}{\TMV}{\SIfL} + \AACon{\ctx}{\ZCCursor{\ECMV}}{\ZCIfC{\ZCCursor{\ECEHole}}{\ECMV}{\ECEHole}}{\TMV}{\SIfL} } \inferrule[AAEConIfR]{ }{ - \AACon{\ctx}{\ZCursor{\ECMV}}{\ZIfC{\ZCursor{\ECEHole}}{\ECEHole}{\ECMV}}{\TMV}{\SIfR} + \AACon{\ctx}{\ZCCursor{\ECMV}}{\ZCIfC{\ZCCursor{\ECEHole}}{\ECEHole}{\ECMV}}{\TMV}{\SIfR} } \end{mathparpagebreakable} @@ -824,7 +824,7 @@ \subsubsection{Analytic expression actions} \AUTAction{\ZTMV}{\ZTMV'}{\AMV} \\ \consistent{\cursorErase{\ZTMV}}{\cursorErase{\ZTMV'}} }{ - \AAAction{\ctx}{\ZLamT{x}{\ZTMV}{\ECMV}}{\ZLamT{x}{\ZTMV'}{\ECMV}}{\TMV}{\AMV} + \AAAction{\ctx}{\ZCLamT{x}{\ZTMV}{\ECMV}}{\ZCLamT{x}{\ZTMV'}{\ECMV}}{\TMV}{\AMV} } \inferrule[AAEZipLamT2]{ @@ -834,7 +834,7 @@ \subsubsection{Analytic expression actions} \consistent{\cursorErase{\ZTMV'}}{\TMV_1} \\ \ctxAnaFixedInto{\extendCtx{\ctx}{x}{\cursorErase{\ZTMV'}}}{\erase{\ECMV}}{\ECMV'}{\TMV_2} }{ - \AAAction{\ctx}{\ZLamT{x}{\ZTMV}{\ECMV}}{\ZLamT{x}{\ZTMV'}{\ECMV'}}{\TMV}{\AMV} + \AAAction{\ctx}{\ZCLamT{x}{\ZTMV}{\ECMV}}{\ZCLamT{x}{\ZTMV'}{\ECMV'}}{\TMV}{\AMV} } \inferrule[AAEZipLamT3]{ @@ -844,55 +844,55 @@ \subsubsection{Analytic expression actions} \inconsistent{\cursorErase{\ZTMV'}}{\TMV_1} \\ \ctxAnaFixedInto{\extendCtx{\ctx}{x}{\TMV_1}}{\erase{\ECMV}}{\ECMV'}{\TMV_2} }{ - \AAAction{\ctx}{\ZLamT{x}{\ZTMV}{\ECMV}}{\ZInconType{\ZLamT{x}{\ZTMV'}{\ECMV'}}}{\TMV}{\AMV} + \AAAction{\ctx}{\ZCLamT{x}{\ZTMV}{\ECMV}}{\ZCInconType{\ZCLamT{x}{\ZTMV'}{\ECMV'}}}{\TMV}{\AMV} } \inferrule[AAEZipLamE]{ \matchedArrow{\TMV}{\TMV_1}{\TMV_2} \\ - \AAAction{\extendCtx{\ctx}{x}{\TMV_3}}{\ZMV}{\ZMV'}{\TMV_2}{\AMV} + \AAAction{\extendCtx{\ctx}{x}{\TMV_3}}{\ZCMV}{\ZCMV'}{\TMV_2}{\AMV} }{ - \AAAction{\ctx}{\ZLamE{x}{\TMV_3}{\ZMV}}{\ZLamE{x}{\TMV_3}{\ZMV'}}{\TMV}{\AMV} + \AAAction{\ctx}{\ZCLamE{x}{\TMV_3}{\ZCMV}}{\ZCLamE{x}{\TMV_3}{\ZCMV'}}{\TMV}{\AMV} } \inferrule[AAEZipLetL1]{ - \ctxSynTypeM{\ctx}{\cursorErase{\ZMV}}{\TMV_1} \\ - \ASEAction{\ctx}{\ZMV}{\TMV_1}{\ZMV'}{\TMV_1'}{\AMV} \\ + \ctxSynTypeM{\ctx}{\cursorErase{\ZCMV}}{\TMV_1} \\ + \ASEAction{\ctx}{\ZCMV}{\TMV_1}{\ZCMV'}{\TMV_1'}{\AMV} \\ \consistent{\TMV_1}{\TMV_1'} }{ - \AAAction{\ctx}{\ZLetL{x}{\ZMV}{\ECMV}}{\ZLetL{x}{\ZMV'}{\ECMV}}{\TMV}{\AMV} + \AAAction{\ctx}{\ZCLetL{x}{\ZCMV}{\ECMV}}{\ZCLetL{x}{\ZCMV'}{\ECMV}}{\TMV}{\AMV} } \inferrule[AAEZipLetL2]{ - \ctxSynTypeM{\ctx}{\cursorErase{\ZMV}}{\TMV_1} \\ - \ASEAction{\ctx}{\ZMV}{\TMV_1}{\ZMV'}{\TMV_1'}{\AMV} \\\\ + \ctxSynTypeM{\ctx}{\cursorErase{\ZCMV}}{\TMV_1} \\ + \ASEAction{\ctx}{\ZCMV}{\TMV_1}{\ZCMV'}{\TMV_1'}{\AMV} \\\\ \ctxAnaFixedInto{\extendCtx{\ctx}{x}{\TMV_1'}}{\erase{\ECMV}}{\ECMV'}{\TMV} }{ - \AAAction{\ctx}{\ZLetL{x}{\ZMV}{\ECMV}}{\ZLetL{x}{\ZMV'}{\ECMV'}}{\TMV}{\AMV} + \AAAction{\ctx}{\ZCLetL{x}{\ZCMV}{\ECMV}}{\ZCLetL{x}{\ZCMV'}{\ECMV'}}{\TMV}{\AMV} } \inferrule[AAEZipLetR]{ \ctxSynTypeM{\ctx}{\ECMV}{\TMV'} \\ - \AAAction{\extendCtx{\ctx}{x}{\TMV'}}{\ZMV}{\ZMV'}{\TMV}{\AMV} + \AAAction{\extendCtx{\ctx}{x}{\TMV'}}{\ZCMV}{\ZCMV'}{\TMV}{\AMV} }{ - \AAAction{\ctx}{\ZLetR{x}{\ECMV}{\ZMV}}{\ZLetL{x}{\ECMV}{\ZMV'}}{\TMV}{\AMV} + \AAAction{\ctx}{\ZCLetR{x}{\ECMV}{\ZCMV}}{\ZCLetL{x}{\ECMV}{\ZCMV'}}{\TMV}{\AMV} } \inferrule[AAEZipIfC]{ - \AAAction{\ctx}{\ZMV}{\ZMV'}{\TBool}{\AMV} + \AAAction{\ctx}{\ZCMV}{\ZCMV'}{\TBool}{\AMV} }{ - \AAAction{\ctx}{\ZIfC{\ZMV}{\ECMV_1}{\ECMV_2}}{\ZIfC{\ZMV'}{\ECMV_1}{\ECMV_2}}{\TMV}{\AMV} + \AAAction{\ctx}{\ZCIfC{\ZCMV}{\ECMV_1}{\ECMV_2}}{\ZCIfC{\ZCMV'}{\ECMV_1}{\ECMV_2}}{\TMV}{\AMV} } \inferrule[AAEZipIfL]{ - \AAAction{\ctx}{\ZMV}{\ZMV'}{\TMV}{\AMV} + \AAAction{\ctx}{\ZCMV}{\ZCMV'}{\TMV}{\AMV} }{ - \AAAction{\ctx}{\ZIfL{\ECMV_1}{\ZMV}{\ECMV_2}}{\ZIfL{\ECMV_1}{\ZMV'}{\ECMV_2}}{\TMV}{\AMV} + \AAAction{\ctx}{\ZCIfL{\ECMV_1}{\ZCMV}{\ECMV_2}}{\ZCIfL{\ECMV_1}{\ZCMV'}{\ECMV_2}}{\TMV}{\AMV} } \inferrule[AAEZipIfR]{ - \AAAction{\ctx}{\ZMV}{\ZMV'}{\TMV}{\AMV} + \AAAction{\ctx}{\ZCMV}{\ZCMV'}{\TMV}{\AMV} }{ - \AAAction{\ctx}{\ZIfR{\ECMV_1}{\ECMV_2}{\ZMV}}{\ZIfR{\ECMV_1}{\ECMV_2}{\ZMV'}}{\TMV}{\AMV} + \AAAction{\ctx}{\ZCIfR{\ECMV_1}{\ECMV_2}{\ZCMV}}{\ZCIfR{\ECMV_1}{\ECMV_2}{\ZCMV'}}{\TMV}{\AMV} } \end{mathparpagebreakable} @@ -900,33 +900,33 @@ \subsubsection{Iterated actions} \label{sec:typed-iterated-actions} The iterated type action and movements judgments are the same as in the untyped model. \\ -\judgbox{\ensuremath{\ASEActionIter{\ctx}{\ZMV}{\TMV}{\ZMV'}{\TMV'}{\AIMV}}} +\judgbox{\ensuremath{\ASEActionIter{\ctx}{\ZCMV}{\TMV}{\ZCMV'}{\TMV'}{\AIMV}}} % \begin{mathpar} \inferrule[ASEIRefl]{ }{ - \ASEActionIter{\ctx}{\ZMV}{\TMV}{\ZMV}{\TMV}{\AINil} + \ASEActionIter{\ctx}{\ZCMV}{\TMV}{\ZCMV}{\TMV}{\AINil} } \inferrule[ASEIExp]{ - \ASEAction{\ctx}{\ZMV}{\TMV}{\ZMV'}{\TMV'}{\AMV} \\ - \ASEActionIter{\ctx}{\ZMV'}{\TMV'}{\ZMV''}{\TMV''}{\AIMV} + \ASEAction{\ctx}{\ZCMV}{\TMV}{\ZCMV'}{\TMV'}{\AMV} \\ + \ASEActionIter{\ctx}{\ZCMV'}{\TMV'}{\ZCMV''}{\TMV''}{\AIMV} }{ - \ASEActionIter{\ctx}{\ZMV}{\TMV}{\ZMV''}{\TMV''}{\AICons{\AMV}{\AIMV}} + \ASEActionIter{\ctx}{\ZCMV}{\TMV}{\ZCMV''}{\TMV''}{\AICons{\AMV}{\AIMV}} } \end{mathpar} -\judgbox{\ensuremath{\AAEActionIter{\ctx}{\ZMV}{\ZMV'}{\TMV}{\AIMV}}} +\judgbox{\ensuremath{\AAEActionIter{\ctx}{\ZCMV}{\ZCMV'}{\TMV}{\AIMV}}} % \begin{mathpar} \inferrule[AAEIRefl]{ }{ - \AAEActionIter{\ctx}{\ZMV}{\ZMV}{\TMV}{\AINil} + \AAEActionIter{\ctx}{\ZCMV}{\ZCMV}{\TMV}{\AINil} } \inferrule[AAEIExp]{ - \AAEAction{\ctx}{\ZMV}{\ZMV'}{\TMV'}{\AMV} \\ - \AAEActionIter{\ctx}{\ZMV'}{\ZMV''}{\TMV''}{\AIMV} + \AAEAction{\ctx}{\ZCMV}{\ZCMV'}{\TMV'}{\AMV} \\ + \AAEActionIter{\ctx}{\ZCMV'}{\ZCMV''}{\TMV''}{\AIMV} }{ - \AAEActionIter{\ctx}{\ZMV}{\ZMV''}{\TMV''}{\AICons{\AMV}{\AIMV}} + \AAEActionIter{\ctx}{\ZCMV}{\ZCMV''}{\TMV''}{\AICons{\AMV}{\AIMV}} } \end{mathpar} @@ -934,13 +934,13 @@ \subsection{Metatheorems} \label{sec:typed-metatheorems} \begin{theorem}[name=Sensibility] \ \begin{enumerate} - \item If $\zWellFormed{\ZMV}$ and $\ctxSynTypeM{\ctx}{\cursorErase{\ZMV}}{\TMV}$ and - $\ASEAction{\ctx}{\ZMV}{\TMV}{\ZMV'}{\TMV'}{\AMV}$, then $\zWellFormed{\ZMV'}$ and - $\ctxSynTypeM{\ctx}{\cursorErase{\ZMV'}}{\TMV'}$. + \item If $\zWellFormed{\ZCMV}$ and $\ctxSynTypeM{\ctx}{\cursorErase{\ZCMV}}{\TMV}$ and + $\ASEAction{\ctx}{\ZCMV}{\TMV}{\ZCMV'}{\TMV'}{\AMV}$, then $\zWellFormed{\ZCMV'}$ and + $\ctxSynTypeM{\ctx}{\cursorErase{\ZCMV'}}{\TMV'}$. - \item If $\zWellFormed{\ZMV}$ and $\ctxAnaType{\ctx}{\cursorErase{\ZMV}}{\TMV}$ and - $\AAEAction{\ctx}{\ZMV}{\ZMV'}{\TMV}{\AMV}$, then $\zWellFormed{\ZMV'}$ and - $\ctxAnaType{\ctx}{\cursorErase{\ZMV'}}{\TMV}$. + \item If $\zWellFormed{\ZCMV}$ and $\ctxAnaType{\ctx}{\cursorErase{\ZCMV}}{\TMV}$ and + $\AAEAction{\ctx}{\ZCMV}{\ZCMV'}{\TMV}{\AMV}$, then $\zWellFormed{\ZCMV'}$ and + $\ctxAnaType{\ctx}{\cursorErase{\ZCMV'}}{\TMV}$. \end{enumerate} \end{theorem} @@ -949,13 +949,13 @@ \subsection{Metatheorems} \item If $\AUTAction{\ZTMV}{\ZTMV'}{\AMove{\MMV}}$, then $\cursorErase{\ZTMV} = \cursorErase{\ZTMV'}$. - \item If $\zWellFormed{\ZMV}$ and $\ctxSynTypeM{\ctx}{\cursorErase{\ZMV}}{\TMV}$ and - $\ASEAction{\ctx}{\ZMV}{\TMV}{\ZMV'}{\TMV'}{\AMove{\MMV}}$, then $\zWellFormed{\ZMV'}$ and - $\cursorErase{\ZMV} = \cursorErase{\ZMV'}$ and $\equal{\TMV}{\TMV'}$. + \item If $\zWellFormed{\ZCMV}$ and $\ctxSynTypeM{\ctx}{\cursorErase{\ZCMV}}{\TMV}$ and + $\ASEAction{\ctx}{\ZCMV}{\TMV}{\ZCMV'}{\TMV'}{\AMove{\MMV}}$, then $\zWellFormed{\ZCMV'}$ and + $\cursorErase{\ZCMV} = \cursorErase{\ZCMV'}$ and $\equal{\TMV}{\TMV'}$. - \item If $\zWellFormed{\ZMV}$ and $\ctxAnaType{\ctx}{\cursorErase{\ZMV}}{\TMV}$ and - $\AAEAction{\ctx}{\ZMV}{\ZMV'}{\TMV}{\AMove{\MMV}}$, then $\zWellFormed{\ZMV'}$ and - $\cursorErase{\ZMV} = \cursorErase{\ZMV'}$. + \item If $\zWellFormed{\ZCMV}$ and $\ctxAnaType{\ctx}{\cursorErase{\ZCMV}}{\TMV}$ and + $\AAEAction{\ctx}{\ZCMV}{\ZCMV'}{\TMV}{\AMove{\MMV}}$, then $\zWellFormed{\ZCMV'}$ and + $\cursorErase{\ZCMV} = \cursorErase{\ZCMV'}$. \end{enumerate} \end{theorem} @@ -964,15 +964,15 @@ \subsection{Metatheorems} \item If $\cursorErase{\ZTMV} = \cursorErase{\ZTMV'}$, then there exists $\AIMV$ such that $\movements{\AIMV}$ and $\AUTActionIter{\ZTMV}{\ZTMV'}{\AIMV}$. - \item If $\zWellFormed{\ZMV}$ and $\zWellFormed{\ZMV'}$ and - $\ctxSynTypeM{\ctx}{\cursorErase{\ZMV}}{\TMV}$ and $\cursorErase{\ZMV} = \cursorErase{\ZMV'}$, + \item If $\zWellFormed{\ZCMV}$ and $\zWellFormed{\ZCMV'}$ and + $\ctxSynTypeM{\ctx}{\cursorErase{\ZCMV}}{\TMV}$ and $\cursorErase{\ZCMV} = \cursorErase{\ZCMV'}$, then there exists $\AIMV$ such that $\movements{\AIMV}$ and - $\ASEActionIter{\ctx}{\ZMV}{\TMV}{\ZMV'}{\TMV}{\AIMV}$. + $\ASEActionIter{\ctx}{\ZCMV}{\TMV}{\ZCMV'}{\TMV}{\AIMV}$. - \item If $\zWellFormed{\ZMV}$ and $\zWellFormed{\ZMV'}$ and - $\ctxAnaType{\ctx}{\cursorErase{\ZMV}}{\TMV}$ and $\cursorErase{\ZMV} = \cursorErase{\ZMV'}$, + \item If $\zWellFormed{\ZCMV}$ and $\zWellFormed{\ZCMV'}$ and + $\ctxAnaType{\ctx}{\cursorErase{\ZCMV}}{\TMV}$ and $\cursorErase{\ZCMV} = \cursorErase{\ZCMV'}$, then there exists $\AIMV$ such that $\movements{\AIMV}$ and - $\AAEActionIter{\ctx}{\ZMV}{\ZMV'}{\TMV}{\AIMV}$. + $\AAEActionIter{\ctx}{\ZCMV}{\ZCMV'}{\TMV}{\AIMV}$. \end{enumerate} \end{theorem} @@ -981,13 +981,13 @@ \subsection{Metatheorems} \item If $\cursorErase{\ZTMV} = \TMV$, then there exists $\AIMV$ such that $\movements{\AIMV}$ and $\AUTActionIter{\ZTMV}{\ZTCursor{\TMV}}{\AIMV}$. - \item If $\zWellFormed{\ZMV}$ and $\ctxSynTypeM{\ctx}{\cursorErase{\ZMV}}{\TMV}$ and - $\cursorErase{\ZMV} = \ECMV$, then there exists $\AIMV$ such that $\movements{\AIMV}$ and - $\ASEActionIter{\ctx}{\ZMV}{\TMV}{\ZTCursor{\ECMV}}{\TMV}{\AIMV}$. + \item If $\zWellFormed{\ZCMV}$ and $\ctxSynTypeM{\ctx}{\cursorErase{\ZCMV}}{\TMV}$ and + $\cursorErase{\ZCMV} = \ECMV$, then there exists $\AIMV$ such that $\movements{\AIMV}$ and + $\ASEActionIter{\ctx}{\ZCMV}{\TMV}{\ZCCursor{\ECMV}}{\TMV}{\AIMV}$. - \item If $\zWellFormed{\ZMV}$ and $\ctxAnaType{\ctx}{\cursorErase{\ZMV}}{\TMV}$ and - $\cursorErase{\ZMV} = \ECMV$, then there exists $\AIMV$ such that $\movements{\AIMV}$ and - $\AAEActionIter{\ctx}{\ZMV}{\ZTCursor{\ECMV}}{\TMV}{\AIMV}$. + \item If $\zWellFormed{\ZCMV}$ and $\ctxAnaType{\ctx}{\cursorErase{\ZCMV}}{\TMV}$ and + $\cursorErase{\ZCMV} = \ECMV$, then there exists $\AIMV$ such that $\movements{\AIMV}$ and + $\AAEActionIter{\ctx}{\ZCMV}{\ZCCursor{\ECMV}}{\TMV}{\AIMV}$. \end{enumerate} \end{lemma} @@ -996,13 +996,13 @@ \subsection{Metatheorems} \item If $\cursorErase{\ZTMV} = \TMV$, then there exists $\AIMV$ such that $\movements{\AIMV}$ and $\AUTActionIter{\ZTCursor{\TMV}}{\ZTMV}{\AIMV}$. - \item If $\zWellFormed{\ZMV}$ and $\ctxSynTypeM{\ctx}{\cursorErase{\ZMV}}{\TMV}$ and - $\cursorErase{\ZMV} = \ECMV$, then there exists $\AIMV$ such that $\movements{\AIMV}$ and - $\ASEActionIter{\ctx}{\ZTCursor{\ECMV}}{\TMV}{\ZMV}{\TMV}{\AIMV}$. + \item If $\zWellFormed{\ZCMV}$ and $\ctxSynTypeM{\ctx}{\cursorErase{\ZCMV}}{\TMV}$ and + $\cursorErase{\ZCMV} = \ECMV$, then there exists $\AIMV$ such that $\movements{\AIMV}$ and + $\ASEActionIter{\ctx}{\ZCCursor{\ECMV}}{\TMV}{\ZCMV}{\TMV}{\AIMV}$. - \item If $\zWellFormed{\ZMV}$ and $\ctxAnaType{\ctx}{\cursorErase{\ZMV}}{\TMV}$ and - $\cursorErase{\ZMV} = \ECMV$, then there exists $\AIMV$ such that $\movements{\AIMV}$ and - $\AAEActionIter{\ctx}{\ZTCursor{\ECMV}}{\ZMV}{\TMV}{\AIMV}$. + \item If $\zWellFormed{\ZCMV}$ and $\ctxAnaType{\ctx}{\cursorErase{\ZCMV}}{\TMV}$ and + $\cursorErase{\ZCMV} = \ECMV$, then there exists $\AIMV$ such that $\movements{\AIMV}$ and + $\AAEActionIter{\ctx}{\ZCCursor{\ECMV}}{\ZCMV}{\TMV}{\AIMV}$. \end{enumerate} \end{lemma} @@ -1012,10 +1012,10 @@ \subsection{Metatheorems} $\AUTActionIter{\ZTCursor{\TUnknown}}{\ZTCursor{\TMV}}{\AIMV}$. \item If $\ctxSynTypeM{\ctx}{\ECMV}{\TMV}$, then there exists $\AIMV$ such that - $\ASEActionIter{\ctx}{\ZCursor{\EEHole}}{\TUnknown}{\ZCursor{\ECMV}}{\TMV}{\AIMV}$. + $\ASEActionIter{\ctx}{\ZCCursor{\EEHole}}{\TUnknown}{\ZCCursor{\ECMV}}{\TMV}{\AIMV}$. \item If $\ctxAnaType{\ctx}{\ECMV}{\TMV}$, then there exists $\AIMV$ such that - $\AAEActionIter{\ctx}{\ZCursor{\EEHole}}{\ZCursor{\ECMV}}{\TMV}{\AIMV}$. + $\AAEActionIter{\ctx}{\ZCCursor{\EEHole}}{\ZCCursor{\ECMV}}{\TMV}{\AIMV}$. \end{enumerate} \end{theorem} @@ -1024,14 +1024,14 @@ \subsection{Metatheorems} \item If $\AUTActionIter{\ZTMV}{\ZTMV'}{\AMV}$ and $\AUTActionIter{\ZTMV}{\ZTMV''}{\AMV}$, then $\ZTMV' = \ZTMV''$. - \item If $\zWellFormed{\ZMV}$ and $\ctxSynTypeM{\ctx}{\cursorErase{\ZMV}}{\TMV}$ and - $\ASEActionIter{\ctx}{\ZMV}{\TMV}{\ZMV'}{\TMV'}{\AMV}$ and - $\ASEActionIter{\ctx}{\ZMV}{\TMV}{\ZMV''}{\TMV''}{\AMV}$, then $\ZMV' = \ZMV''$ and + \item If $\zWellFormed{\ZCMV}$ and $\ctxSynTypeM{\ctx}{\cursorErase{\ZCMV}}{\TMV}$ and + $\ASEActionIter{\ctx}{\ZCMV}{\TMV}{\ZCMV'}{\TMV'}{\AMV}$ and + $\ASEActionIter{\ctx}{\ZCMV}{\TMV}{\ZCMV''}{\TMV''}{\AMV}$, then $\ZCMV' = \ZCMV''$ and $\equal{\TMV'}{\TMV''}$. - \item If $\zWellFormed{\ZMV}$ and $\ctxAnaType{\ctx}{\cursorErase{\ZMV}}{\TMV}$ and - $\AAEActionIter{\ctx}{\ZMV}{\ZMV'}{\TMV}{\AMV}$ and - $\AAEActionIter{\ctx}{\ZMV}{\ZMV''}{\TMV}{\AMV}$, then $\ZMV' = \ZMV''$. + \item If $\zWellFormed{\ZCMV}$ and $\ctxAnaType{\ctx}{\cursorErase{\ZCMV}}{\TMV}$ and + $\AAEActionIter{\ctx}{\ZCMV}{\ZCMV'}{\TMV}{\AMV}$ and + $\AAEActionIter{\ctx}{\ZCMV}{\ZCMV''}{\TMV}{\AMV}$, then $\ZCMV' = \ZCMV''$. \end{enumerate} \end{theorem} From 69fb9c26d0d61557ff1146e02d83ffab75c2aa8f Mon Sep 17 00:00:00 2001 From: Eric Zhao <21zhaoe@protonmail.com> Date: Mon, 9 Oct 2023 00:23:53 -0400 Subject: [PATCH 04/24] formalism: Add missing marked zexp movement rules --- formalism/typed.tex | 112 ++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 112 insertions(+) diff --git a/formalism/typed.tex b/formalism/typed.tex index c29d131..a59d4aa 100644 --- a/formalism/typed.tex +++ b/formalism/typed.tex @@ -370,6 +370,38 @@ \subsubsection{Expression movement} \ASEMParent{\ZCIfR{\ECMV_1}{\ECMV_2}{\ZCCursor{\ECMV_3}}}{\ECIf{\ECMV_1}{\ECMV_2}{\ECMV_3}} } + \inferrule[AEMPairChild1]{ }{ + \ASEMChild{\ECPair{\ECMV_1}{\ECMV_2}}{\ZCPairL{\ZCCursor{\ECMV_1}}{\ECMV_2}}{1} + } + + \inferrule[AEMPairChild2]{ }{ + \ASEMChild{\ECPair{\ECMV_1}{\ECMV_2}}{\ZCPairR{\ECMV_1}{\ZCCursor{\ECMV_2}}}{2} + } + + \inferrule[AEMPairParent1]{ }{ + \ASEMParent{\ZCPairL{\ZCCursor{\ECMV_1}}{\ECMV_2}}{\ECPair{\ECMV_1}{\ECMV_2}} + } + + \inferrule[AEMPairParent2]{ }{ + \ASEMParent{\ZCPairR{\ECMV_1}{\ZCCursor{\ECMV_2}}}{\ECPair{\ECMV_1}{\ECMV_2}} + } + + \inferrule[AEMProjLChild1]{ }{ + \ASEMChild{\ECProjL{\ECMV}}{\ZCProjL{\ZCCursor{\ECMV}}}{1} + } + + \inferrule[AEMProjLParent1]{ }{ + \ASEMParent{\ZCProjL{\ZCCursor{\ECMV}}}{\ECProjL{\ECMV}} + } + + \inferrule[AEMProjRChild1]{ }{ + \ASEMChild{\ECProjR{\ECMV}}{\ZCProjR{\ZCCursor{\ECMV}}}{1} + } + + \inferrule[AEMProjRParent1]{ }{ + \ASEMParent{\ZCProjR{\ZCCursor{\ECMV}}}{\ECProjR{\ECMV}} + } + \inferrule[AEMInconsistentTypesChild]{ \ASEMChild{\ZCMV}{\ZCMV'}{\MChildNMV} }{ @@ -382,6 +414,54 @@ \subsubsection{Expression movement} \ASEMParent{\ZCInconType{\ZCMV}}{\ZCInconType{\ZCMV'}} } + \inferrule[AEMLamChild3]{ }{ + \ASEMChild{\ECLamInconAsc{x}{\TMV}{\ECMV}}{\ZCLamInconAscT{x}{\ZTCursor{\TMV}}{\ECMV}}{1} + } + + \inferrule[AEMLamChild4]{ }{ + \ASEMChild{\ECLamInconAsc{x}{\TMV}{\ECMV}}{\ZCLamInconAscE{x}{\TMV}{\ZCCursor{\ECMV}}}{2} + } + + \inferrule[AEMLamParent3]{ }{ + \ASEMParent{\ZCLamInconAscT{x}{\ZTCursor{\TMV}}{\ECMV}}{\ECLamInconAsc{x}{\TMV}{\ECMV}} + } + + \inferrule[AEMLamParent4]{ }{ + \ASEMParent{\ZCLamInconAscE{x}{\TMV}{\ZCCursor{\ECMV}}}{\ECLamInconAsc{x}{\TMV}{\ECMV}} + } + + \inferrule[AEMLamChild5]{ }{ + \ASEMChild{\ECLamAnaNonMatchedArrow{x}{\TMV}{\ECMV}}{\ZCLamAnaNonMatchedArrowT{x}{\ZTCursor{\TMV}}{\ECMV}}{1} + } + + \inferrule[AEMLamChild6]{ }{ + \ASEMChild{\ECLamAnaNonMatchedArrow{x}{\TMV}{\ECMV}}{\ZCLamAnaNonMatchedArrowE{x}{\TMV}{\ZCCursor{\ECMV}}}{2} + } + + \inferrule[AEMLamParent5]{ }{ + \ASEMParent{\ZCLamAnaNonMatchedArrowT{x}{\ZTCursor{\TMV}}{\ECMV}}{\ECLamAnaNonMatchedArrow{x}{\TMV}{\ECMV}} + } + + \inferrule[AEMLamParent6]{ }{ + \ASEMParent{\ZCLamAnaNonMatchedArrowE{x}{\TMV}{\ZCCursor{\ECMV}}}{\ECLamAnaNonMatchedArrow{x}{\TMV}{\ECMV}} + } + + \inferrule[AEMApChild3]{ }{ + \ASEMChild{\ECApSynNonMatchedArrow{\ECMV_1}{\ECMV_2}}{\ZCApSynNonMatchedArrowL{\ZCCursor{\ECMV_1}}{\ECMV_2}}{1} + } + + \inferrule[AEMApChild4]{ }{ + \ASEMChild{\ECApSynNonMatchedArrow{\ECMV_1}{\ECMV_2}}{\ZCApSynNonMatchedArrowR{\ECMV_1}{\ZCCursor{\ECMV_2}}}{2} + } + + \inferrule[AEMApParent3]{ }{ + \ASEMParent{\ZCApSynNonMatchedArrowL{\ZCCursor{\ECMV_1}}{\ECMV_2}}{\ECApSynNonMatchedArrow{\ECMV_1}{\ECMV_2}} + } + + \inferrule[AEMApParent4]{ }{ + \ASEMParent{\ZCApSynNonMatchedArrowR{\ECMV_1}{\ZCCursor{\ECMV_2}}}{\ECApSynNonMatchedArrow{\ECMV_1}{\ECMV_2}} + } + \inferrule[AEMInconsistentBranchesChild1]{ }{ \ASEMChild{\ECInconBr{\ECMV_1}{\ECMV_2}{\ECMV_3}}{\ZCInconBrC{\ZCCursor{\ECMV_1}}{\ECMV_2}{\ECMV_3}}{1} } @@ -405,6 +485,38 @@ \subsubsection{Expression movement} \inferrule[AEMInconsistentBranchesParent3]{ }{ \ASEMParent{\ZCInconBrC{\ECMV_1}{\ECMV_2}{\ZCCursor{\ECMV_3}}}{\ECInconBr{\ECMV_1}{\ECMV_2}{\ECMV_3}} } + + \inferrule[AEMPairChild3]{ }{ + \ASEMChild{\ECPairAnaNonMatchedProd{\ECMV_1}{\ECMV_2}}{\ZCPairAnaNonMatchedProdL{\ZCCursor{\ECMV_1}}{\ECMV_2}}{1} + } + + \inferrule[AEMPairChild4]{ }{ + \ASEMChild{\ECPairAnaNonMatchedProd{\ECMV_1}{\ECMV_2}}{\ZCPairAnaNonMatchedProdR{\ECMV_1}{\ZCCursor{\ECMV_2}}}{2} + } + + \inferrule[AEMPairParent3]{ }{ + \ASEMParent{\ZCPairAnaNonMatchedProdL{\ZCCursor{\ECMV_1}}{\ECMV_2}}{\ECPairAnaNonMatchedProd{\ECMV_1}{\ECMV_2}} + } + + \inferrule[AEMPairParent4]{ }{ + \ASEMParent{\ZCPairAnaNonMatchedProdR{\ECMV_1}{\ZCCursor{\ECMV_2}}}{\ECPairAnaNonMatchedProd{\ECMV_1}{\ECMV_2}} + } + + \inferrule[AEMProjLChild2]{ }{ + \ASEMChild{\ECProjLSynNonMatchedProd{\ECMV}}{\ZCProjLSynNonMatchedProd{\ZCCursor{\ECMV}}}{1} + } + + \inferrule[AEMProjLParent2]{ }{ + \ASEMParent{\ZCProjLSynNonMatchedProd{\ZCCursor{\ECMV}}}{\ECProjLSynNonMatchedProd{\ECMV}} + } + + \inferrule[AEMProjRChild2]{ }{ + \ASEMChild{\ECProjRSynNonMatchedProd{\ECMV}}{\ZCProjRSynNonMatchedProd{\ZCCursor{\ECMV}}}{1} + } + + \inferrule[AEMProjRParent2]{ }{ + \ASEMParent{\ZCProjRSynNonMatchedProd{\ZCCursor{\ECMV}}}{\ECProjRSynNonMatchedProd{\ECMV}} + } \end{mathparpagebreakable} \subsubsection{Synthetic expression actions} From 17922d0b45b21bf4a9dad1cb9fbeb7a2c5a8345d Mon Sep 17 00:00:00 2001 From: Eric Zhao <21zhaoe@protonmail.com> Date: Mon, 9 Oct 2023 00:24:16 -0400 Subject: [PATCH 05/24] formalism: Name marked zexps MZExp --- formalism/symbols/typed.tex | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/formalism/symbols/typed.tex b/formalism/symbols/typed.tex index 8934d3e..4893be8 100644 --- a/formalism/symbols/typed.tex +++ b/formalism/symbols/typed.tex @@ -3,7 +3,7 @@ % % marked zippered expressions % -\newcommand{\ZCMName}{{\normalfont\textsf{MZExp}}} +\newcommand{\ZCMName}{{\normalfont\textsf{ZMExp}}} \newcommand{\ZCMSet}{\ensuremath{\hat{E}}} \newcommand{\ZCMV}{\ensuremath{\underline{\check{e}}}} From b616af5b80f2a113b1aea22e0ca1150deca2aaf8 Mon Sep 17 00:00:00 2001 From: Eric Zhao <21zhaoe@protonmail.com> Date: Mon, 9 Oct 2023 00:40:19 -0400 Subject: [PATCH 06/24] formalism: Reorder fixed marked zexp rules to match order in preceding sections --- formalism/typed.tex | 334 ++++++++++++++++++++++---------------------- 1 file changed, 167 insertions(+), 167 deletions(-) diff --git a/formalism/typed.tex b/formalism/typed.tex index a59d4aa..25ddc82 100644 --- a/formalism/typed.tex +++ b/formalism/typed.tex @@ -44,6 +44,10 @@ \subsubsection{Well-formedness} \zWellFormed{\ZCCursor{\ECMV}} } + \inferrule[WFFree]{ }{ + \zWellFormed{\ZCFree{x}} + } + \inferrule[WFLam1]{ }{ \zWellFormed{\ZCLamT{x}{\ZTMV}{\ECMV}} } @@ -54,162 +58,151 @@ \subsubsection{Well-formedness} \zWellFormed{\ZCLamE{x}{\TMV}{\ZCMV}} } - \inferrule[WFAp1]{ - \zWellFormed{\ZCMV} + \inferrule[WFLam3]{ }{ - \zWellFormed{\ZCApL{\ZCMV}{\ECMV}} + \zWellFormed{\ZCLamAnaNonMatchedArrowT{x}{\ZTMV}{\ECMV}} } - \inferrule[WFAp2]{ + \inferrule[WFLam4]{ \zWellFormed{\ZCMV} }{ - \zWellFormed{\ZCApR{\ECMV}{\ZCMV}} + \zWellFormed{\ZCLamAnaNonMatchedArrowE{x}{\TMV}{\ZCMV}} } - \inferrule[WFLet1]{ - \zWellFormed{\ZCMV} - }{ - \zWellFormed{\ZCLetL{x}{\ZCMV}{\ECMV}} + \inferrule[WFLam5]{ }{ + \zWellFormed{\ZCLamInconAscT{x}{\ZTMV}{\ECMV}} } - \inferrule[WFLet2]{ + \inferrule[WFLam6]{ \zWellFormed{\ZCMV} }{ - \zWellFormed{\ZCLetR{x}{\ECMV}{\ZCMV}} + \zWellFormed{\ZCLamInconAscE{x}{\TMV}{\ZCMV}} } - \inferrule[WFPlus1]{ + \inferrule[WFAp1]{ \zWellFormed{\ZCMV} }{ - \zWellFormed{\ZCPlusL{\ZCMV}{\ECMV}} + \zWellFormed{\ZCApL{\ZCMV}{\ECMV}} } - \inferrule[WFPlus2]{ + \inferrule[WFAp2]{ \zWellFormed{\ZCMV} }{ - \zWellFormed{\ZCPlusR{\ECMV}{\ZCMV}} + \zWellFormed{\ZCApR{\ECMV}{\ZCMV}} } - \inferrule[WFIf1]{ + \inferrule[WFAp3]{ \zWellFormed{\ZCMV} }{ - \zWellFormed{\ZCIfC{\ZCMV}{\ECMV_1}{\ECMV_2}} + \zWellFormed{\ZCApSynNonMatchedArrowL{\ZCMV}{\ECMV}} } - \inferrule[WFIf2]{ + \inferrule[WFAp4]{ \zWellFormed{\ZCMV} }{ - \zWellFormed{\ZCIfL{\ECMV_1}{\ZCMV}{\ECMV_2}} + \zWellFormed{\ZCApSynNonMatchedArrowR{\ECMV}{\ZCMV}} } - \inferrule[WFIf3]{ + \inferrule[WFLet1]{ \zWellFormed{\ZCMV} }{ - \zWellFormed{\ZCIfR{\ECMV_1}{\ECMV_2}{\ZCMV}} + \zWellFormed{\ZCLetL{x}{\ZCMV}{\ECMV}} } - \inferrule[WFPair1]{ + \inferrule[WFLet2]{ \zWellFormed{\ZCMV} }{ - \zWellFormed{\ZCPairL{\ZCMV}{\ECMV}} + \zWellFormed{\ZCLetR{x}{\ECMV}{\ZCMV}} } - \inferrule[WFPair2]{ + \inferrule[WFPlus1]{ \zWellFormed{\ZCMV} }{ - \zWellFormed{\ZCPairR{\ECMV}{\ZCMV}} + \zWellFormed{\ZCPlusL{\ZCMV}{\ECMV}} } - \inferrule[WFProjL1]{ + \inferrule[WFPlus2]{ \zWellFormed{\ZCMV} }{ - \zWellFormed{\ZCProjL{\ZCMV}} + \zWellFormed{\ZCPlusR{\ECMV}{\ZCMV}} } - \inferrule[WFProjR1]{ + \inferrule[WFIf1]{ \zWellFormed{\ZCMV} }{ - \zWellFormed{\ZCProjR{\ZCMV}} - } - - \inferrule[WFFree]{ }{ - \zWellFormed{\ZCFree{x}} + \zWellFormed{\ZCIfC{\ZCMV}{\ECMV_1}{\ECMV_2}} } - \inferrule[WFInconsistentTypes]{ - \notEqual{\ZCMV}{\ZCCursor{\ECMV}} \\ + \inferrule[WFIf2]{ \zWellFormed{\ZCMV} }{ - \zWellFormed{\ZCInconType{\ZCMV}} - } - - \inferrule[WFLam3]{ }{ - \zWellFormed{\ZCLamInconAscT{x}{\ZTMV}{\ECMV}} + \zWellFormed{\ZCIfL{\ECMV_1}{\ZCMV}{\ECMV_2}} } - \inferrule[WFLam4]{ + \inferrule[WFIf3]{ \zWellFormed{\ZCMV} }{ - \zWellFormed{\ZCLamInconAscE{x}{\TMV}{\ZCMV}} + \zWellFormed{\ZCIfR{\ECMV_1}{\ECMV_2}{\ZCMV}} } - \inferrule[WFLam5]{ + \inferrule[WFInconsistentBranches1]{ + \zWellFormed{\ZCMV} }{ - \zWellFormed{\ZCLamAnaNonMatchedArrowT{x}{\ZTMV}{\ECMV}} + \zWellFormed{\ZCInconBrC{\ZCMV}{\ECMV_1}{\ECMV_2}} } - \inferrule[WFLam6]{ + \inferrule[WFInconsistentBranches2]{ \zWellFormed{\ZCMV} }{ - \zWellFormed{\ZCLamAnaNonMatchedArrowE{x}{\TMV}{\ZCMV}} + \zWellFormed{\ZCInconBrL{\ECMV_1}{\ZCMV}{\ECMV_2}} } - \inferrule[WFAp3]{ + \inferrule[WFInconsistentBranches3]{ \zWellFormed{\ZCMV} }{ - \zWellFormed{\ZCApSynNonMatchedArrowL{\ZCMV}{\ECMV}} + \zWellFormed{\ZCInconBrR{\ECMV_1}{\ECMV_2}{\ZCMV}} } - \inferrule[WFAp4]{ + \inferrule[WFPair1]{ \zWellFormed{\ZCMV} }{ - \zWellFormed{\ZCApSynNonMatchedArrowR{\ECMV}{\ZCMV}} + \zWellFormed{\ZCPairL{\ZCMV}{\ECMV}} } - \inferrule[WFInconsistentBranches1]{ + \inferrule[WFPair2]{ \zWellFormed{\ZCMV} }{ - \zWellFormed{\ZCInconBrC{\ZCMV}{\ECMV_1}{\ECMV_2}} + \zWellFormed{\ZCPairR{\ECMV}{\ZCMV}} } - \inferrule[WFInconsistentBranches2]{ + \inferrule[WFPair3]{ \zWellFormed{\ZCMV} }{ - \zWellFormed{\ZCInconBrL{\ECMV_1}{\ZCMV}{\ECMV_2}} + \zWellFormed{\ZCPairAnaNonMatchedProdL{\ZCMV}{\ECMV}} } - \inferrule[WFInconsistentBranches3]{ + \inferrule[WFPair4]{ \zWellFormed{\ZCMV} }{ - \zWellFormed{\ZCInconBrR{\ECMV_1}{\ECMV_2}{\ZCMV}} + \zWellFormed{\ZCPairAnaNonMatchedProdR{\ECMV}{\ZCMV}} } - \inferrule[WFPair3]{ + \inferrule[WFProjL1]{ \zWellFormed{\ZCMV} }{ - \zWellFormed{\ZCPairAnaNonMatchedProdL{\ZCMV}{\ECMV}} + \zWellFormed{\ZCProjL{\ZCMV}} } - \inferrule[WFPair4]{ + \inferrule[WFProjL2]{ \zWellFormed{\ZCMV} }{ - \zWellFormed{\ZCPairAnaNonMatchedProdR{\ECMV}{\ZCMV}} + \zWellFormed{\ZCProjLSynNonMatchedProd{\ZCMV}} } - \inferrule[WFProjL2]{ + \inferrule[WFProjR1]{ \zWellFormed{\ZCMV} }{ - \zWellFormed{\ZCProjLSynNonMatchedProd{\ZCMV}} + \zWellFormed{\ZCProjR{\ZCMV}} } \inferrule[WFProjR2]{ @@ -217,6 +210,13 @@ \subsubsection{Well-formedness} }{ \zWellFormed{\ZCProjRSynNonMatchedProd{\ZCMV}} } + + \inferrule[WFInconsistentTypes]{ + \notEqual{\ZCMV}{\ZCCursor{\ECMV}} \\ + \zWellFormed{\ZCMV} + }{ + \zWellFormed{\ZCInconType{\ZCMV}} + } \end{mathpar} \subsection{Cursor erasure} @@ -233,10 +233,17 @@ \subsubsection{Expression cursor erasure} \newcommand{\cursorErasesToRow}[2]{\ensuremath{\cursorErase{#1} & = & #2}} \[\begin{array}{rcl} \cursorErasesToRow{\ZCCursor{\ECMV}}{\ECMV} \\ + \cursorErasesToRow{\ZCFree{x}}{\cursorErase{\ECFree{x}}} \\ \cursorErasesToRow{(\ZCLamT{x}{\ZTMV}{\ECMV})}{\ECLam{x}{(\cursorErase{\ZTMV})}{\ECMV}} \\ \cursorErasesToRow{(\ZCLamE{x}{\TMV}{\ZCMV})}{\ECLam{x}{\TMV}{(\cursorErase{\ZCMV})}} \\ + \cursorErasesToRow{\ZCLamAnaNonMatchedArrowT{x}{\ZTMV}{\ECMV}}{\ECLamAnaNonMatchedArrow{x}{(\cursorErase{\ZTMV})}{\ECMV}} \\ + \cursorErasesToRow{\ZCLamAnaNonMatchedArrowE{x}{\TMV}{\ZCMV}}{\ECLamAnaNonMatchedArrow{x}{\TMV}{(\cursorErase{\ZCMV})}} \\ + \cursorErasesToRow{\ZCLamInconAscT{x}{\ZTMV}{\ECMV}}{\ECLamInconAsc{x}{(\cursorErase{\ZTMV})}{\ECMV}} \\ + \cursorErasesToRow{\ZCLamInconAscE{x}{\TMV}{\ZCMV}}{\ECLamInconAsc{x}{\TMV}{(\cursorErase{\ZCMV})}} \\ \cursorErasesToRow{(\ZCApL{\ZCMV}{\ECMV})}{\ECAp{(\cursorErase{\ZCMV})}{\ECMV}} \\ \cursorErasesToRow{(\ZCApR{\ECMV}{\ZCMV})}{\ECAp{\ECMV}{(\cursorErase{\ZCMV})}} \\ + \cursorErasesToRow{(\ZCApSynNonMatchedArrowL{\ZCMV}{\ECMV})}{\ECApSynNonMatchedArrow{\cursorErase{\ZCMV}}{\ECMV}} \\ + \cursorErasesToRow{(\ZCApSynNonMatchedArrowR{\ECMV}{\ZCMV})}{\ECApSynNonMatchedArrow{\ECMV}{(\cursorErase{\ZCMV})}} \\ \cursorErasesToRow{(\ZCLetL{x}{\ZCMV}{\ECMV})}{\ECLet{x}{(\cursorErase{\ZCMV})}{\ECMV}} \\ \cursorErasesToRow{(\ZCLetR{x}{\ECMV}{\ZCMV})}{\ECLet{x}{\ECMV}{(\cursorErase{\ZCMV})}} \\ \cursorErasesToRow{(\ZCPlusL{\ZCMV}{\ECMV})}{\ECPlus{(\cursorErase{\ZCMV})}{\ECMV}} \\ @@ -244,25 +251,18 @@ \subsubsection{Expression cursor erasure} \cursorErasesToRow{(\ZCIfC{\ZCMV}{\ECMV_1}{\ECMV_2})}{\ECIf{(\cursorErase{\ZCMV})}{\ECMV_1}{\ECMV_2}} \\ \cursorErasesToRow{(\ZCIfL{\ECMV_1}{\ZCMV}{\ECMV_2})}{\ECIf{\ECMV_1}{(\cursorErase{\ZCMV})}{\ECMV_2}} \\ \cursorErasesToRow{(\ZCIfL{\ECMV_1}{\ECMV_2}{\ZCMV})}{\ECIf{\ECMV_1}{\ECMV_2}{(\cursorErase{\ZCMV})}} \\ + \cursorErasesToRow{\ZCInconBrC{\ZCMV}{\ECMV_1}{\ECMV_2}}{\ECInconBr{(\cursorErase{\ZCMV})}{\ECMV_1}{\ECMV_2}} \\ + \cursorErasesToRow{\ZCInconBrL{\ECMV_1}{\ZCMV}{\ECMV_2}}{\ECInconBr{\ECMV_1}{(\cursorErase{\ZCMV})}{\ECMV_2}} \\ + \cursorErasesToRow{\ZCInconBrR{\ECMV_1}{\ECMV_2}{\ZCMV}}{\ECInconBr{\ECMV_1}{\ECMV_2}{(\cursorErase{\ZCMV})}} \\ \cursorErasesToRow{\ZCPairL{\ZCMV}{\ECMV}}{\ECPair{\cursorErase{\ZCMV}}{\ECMV}} \\ \cursorErasesToRow{\ZCPairR{\ECMV}{\ZCMV}}{\ECPair{\ECMV}{\cursorErase{\ZCMV}}} \\ - \cursorErasesToRow{(\ZCProjL{\ZCMV})}{\ECProjL{(\cursorErase{\ZCMV})}} \\ - \cursorErasesToRow{(\ZCProjR{\ZCMV})}{\ECProjR{(\cursorErase{\ZCMV})}} \\ - \cursorErasesToRow{\ZCFree{x}}{\cursorErase{\ECFree{x}}} \\ - \cursorErasesToRow{\ZCInconType{\ZCMV}}{\ECInconType{\cursorErase{\ZCMV}}} \\ - \cursorErasesToRow{\ZCLamInconAscT{x}{\ZTMV}{\ECMV}}{\ECLamInconAsc{x}{\cursorErase{\ZTMV}}{\ECMV}} \\ - \cursorErasesToRow{\ZCLamInconAscE{x}{\TMV}{\ZCMV}}{\ECLamInconAsc{x}{\TMV}{\cursorErase{\ZCMV}}} \\ - \cursorErasesToRow{\ZCLamAnaNonMatchedArrowT{x}{\ZTMV}{\ECMV}}{\ECLamAnaNonMatchedArrow{x}{\cursorErase{\ZTMV}}{\ECMV}} \\ - \cursorErasesToRow{\ZCLamAnaNonMatchedArrowE{x}{\TMV}{\ZCMV}}{\ECLamAnaNonMatchedArrow{x}{\TMV}{\cursorErase{\ZCMV}}} \\ - \cursorErasesToRow{(\ZCApSynNonMatchedArrowL{\ZCMV}{\ECMV})}{\ECApSynNonMatchedArrow{\cursorErase{\ZCMV}}{\ECMV}} \\ - \cursorErasesToRow{(\ZCApSynNonMatchedArrowR{\ECMV}{\ZCMV})}{\ECApSynNonMatchedArrow{\ECMV}{(\cursorErase{\ZCMV})}} \\ - \cursorErasesToRow{\ZCInconBrC{\ZCMV}{\ECMV_1}{\ECMV_2}}{\ECInconBr{\cursorErase{\ZCMV}}{\ECMV_1}{\ECMV_2}} \\ - \cursorErasesToRow{\ZCInconBrL{\ECMV_1}{\ZCMV}{\ECMV_2}}{\ECInconBr{\ECMV_1}{\cursorErase{\ZCMV}}{\ECMV_2}} \\ - \cursorErasesToRow{\ZCInconBrR{\ECMV_1}{\ECMV_2}{\ZCMV}}{\ECInconBr{\ECMV_1}{\ECMV_2}{\cursorErase{\ZCMV}}} \\ \cursorErasesToRow{\ZCPairAnaNonMatchedProdL{\ZCMV}{\ECMV}}{\ECPairAnaNonMatchedProd{\cursorErase{\ZCMV}}{\ECMV}} \\ \cursorErasesToRow{\ZCPairAnaNonMatchedProdR{\ECMV}{\ZCMV}}{\ECPairAnaNonMatchedProd{\ECMV}{\cursorErase{\ZCMV}}} \\ + \cursorErasesToRow{(\ZCProjL{\ZCMV})}{\ECProjL{(\cursorErase{\ZCMV})}} \\ \cursorErasesToRow{(\ZCProjLSynNonMatchedProd{\ZCMV})}{\ECProjLSynNonMatchedProd{\cursorErase{\ZCMV}}} \\ + \cursorErasesToRow{(\ZCProjR{\ZCMV})}{\ECProjR{(\cursorErase{\ZCMV})}} \\ \cursorErasesToRow{(\ZCProjRSynNonMatchedProd{\ZCMV})}{\ECProjRSynNonMatchedProd{\cursorErase{\ZCMV}}} \\ + \cursorErasesToRow{\ZCInconType{\ZCMV}}{\ECInconType{\cursorErase{\ZCMV}}} \\ \end{array}\] \subsection{Action model} @@ -290,6 +290,22 @@ \subsubsection{Expression movement} \ASEMChild{\ECLam{x}{\TMV}{\ECMV}}{\ZCLamE{x}{\TMV}{\ZCCursor{\ECMV}}}{2} } + \inferrule[AEMLamChild3]{ }{ + \ASEMChild{\ECLamAnaNonMatchedArrow{x}{\TMV}{\ECMV}}{\ZCLamAnaNonMatchedArrowT{x}{\ZTCursor{\TMV}}{\ECMV}}{1} + } + + \inferrule[AEMLamChild4]{ }{ + \ASEMChild{\ECLamAnaNonMatchedArrow{x}{\TMV}{\ECMV}}{\ZCLamAnaNonMatchedArrowE{x}{\TMV}{\ZCCursor{\ECMV}}}{2} + } + + \inferrule[AEMLamChild5]{ }{ + \ASEMChild{\ECLamInconAsc{x}{\TMV}{\ECMV}}{\ZCLamInconAscT{x}{\ZTCursor{\TMV}}{\ECMV}}{1} + } + + \inferrule[AEMLamChild6]{ }{ + \ASEMChild{\ECLamInconAsc{x}{\TMV}{\ECMV}}{\ZCLamInconAscE{x}{\TMV}{\ZCCursor{\ECMV}}}{2} + } + \inferrule[AEMLamParent1]{ }{ \ASEMParent{\ZCLamT{x}{\ZTCursor{\TMV}}{\ECMV}}{\ECLam{x}{\TMV}{\ECMV}} } @@ -298,6 +314,22 @@ \subsubsection{Expression movement} \ASEMParent{\ZCLamE{x}{\TMV}{\ZCCursor{\ECMV}}}{\ECLam{x}{\TMV}{\ECMV}} } + \inferrule[AEMLamParent3]{ }{ + \ASEMParent{\ZCLamAnaNonMatchedArrowT{x}{\ZTCursor{\TMV}}{\ECMV}}{\ECLamAnaNonMatchedArrow{x}{\TMV}{\ECMV}} + } + + \inferrule[AEMLamParent4]{ }{ + \ASEMParent{\ZCLamAnaNonMatchedArrowE{x}{\TMV}{\ZCCursor{\ECMV}}}{\ECLamAnaNonMatchedArrow{x}{\TMV}{\ECMV}} + } + + \inferrule[AEMLamParent5]{ }{ + \ASEMParent{\ZCLamInconAscT{x}{\ZTCursor{\TMV}}{\ECMV}}{\ECLamInconAsc{x}{\TMV}{\ECMV}} + } + + \inferrule[AEMLamParent6]{ }{ + \ASEMParent{\ZCLamInconAscE{x}{\TMV}{\ZCCursor{\ECMV}}}{\ECLamInconAsc{x}{\TMV}{\ECMV}} + } + \inferrule[AEMApChild1]{ }{ \ASEMChild{\ECAp{\ECMV_1}{\ECMV_2}}{\ZCApL{\ZCCursor{\ECMV_1}}{\ECMV_2}}{1} } @@ -306,6 +338,14 @@ \subsubsection{Expression movement} \ASEMChild{\ECAp{\ECMV_1}{\ECMV_2}}{\ZCApR{\ECMV_1}{\ZCCursor{\ECMV_2}}}{2} } + \inferrule[AEMApChild3]{ }{ + \ASEMChild{\ECApSynNonMatchedArrow{\ECMV_1}{\ECMV_2}}{\ZCApSynNonMatchedArrowL{\ZCCursor{\ECMV_1}}{\ECMV_2}}{1} + } + + \inferrule[AEMApChild4]{ }{ + \ASEMChild{\ECApSynNonMatchedArrow{\ECMV_1}{\ECMV_2}}{\ZCApSynNonMatchedArrowR{\ECMV_1}{\ZCCursor{\ECMV_2}}}{2} + } + \inferrule[AEMApParent1]{ }{ \ASEMParent{\ZCApL{\ZCCursor{\ECMV_1}}{\ECMV_2}}{\ECAp{\ECMV_1}{\ECMV_2}} } @@ -314,6 +354,14 @@ \subsubsection{Expression movement} \ASEMParent{\ZCApR{\ECMV_1}{\ZCCursor{\ECMV_2}}}{\ECAp{\ECMV_1}{\ECMV_2}} } + \inferrule[AEMApParent3]{ }{ + \ASEMParent{\ZCApSynNonMatchedArrowL{\ZCCursor{\ECMV_1}}{\ECMV_2}}{\ECApSynNonMatchedArrow{\ECMV_1}{\ECMV_2}} + } + + \inferrule[AEMApParent4]{ }{ + \ASEMParent{\ZCApSynNonMatchedArrowR{\ECMV_1}{\ZCCursor{\ECMV_2}}}{\ECApSynNonMatchedArrow{\ECMV_1}{\ECMV_2}} + } + \inferrule[AEMLetChild1]{ }{ \ASEMChild{\ECLet{x}{\ECMV_1}{\ECMV_2}}{\ZCLetL{x}{\ZCCursor{\ECMV_1}}{\ECMV_2}}{1} } @@ -370,98 +418,6 @@ \subsubsection{Expression movement} \ASEMParent{\ZCIfR{\ECMV_1}{\ECMV_2}{\ZCCursor{\ECMV_3}}}{\ECIf{\ECMV_1}{\ECMV_2}{\ECMV_3}} } - \inferrule[AEMPairChild1]{ }{ - \ASEMChild{\ECPair{\ECMV_1}{\ECMV_2}}{\ZCPairL{\ZCCursor{\ECMV_1}}{\ECMV_2}}{1} - } - - \inferrule[AEMPairChild2]{ }{ - \ASEMChild{\ECPair{\ECMV_1}{\ECMV_2}}{\ZCPairR{\ECMV_1}{\ZCCursor{\ECMV_2}}}{2} - } - - \inferrule[AEMPairParent1]{ }{ - \ASEMParent{\ZCPairL{\ZCCursor{\ECMV_1}}{\ECMV_2}}{\ECPair{\ECMV_1}{\ECMV_2}} - } - - \inferrule[AEMPairParent2]{ }{ - \ASEMParent{\ZCPairR{\ECMV_1}{\ZCCursor{\ECMV_2}}}{\ECPair{\ECMV_1}{\ECMV_2}} - } - - \inferrule[AEMProjLChild1]{ }{ - \ASEMChild{\ECProjL{\ECMV}}{\ZCProjL{\ZCCursor{\ECMV}}}{1} - } - - \inferrule[AEMProjLParent1]{ }{ - \ASEMParent{\ZCProjL{\ZCCursor{\ECMV}}}{\ECProjL{\ECMV}} - } - - \inferrule[AEMProjRChild1]{ }{ - \ASEMChild{\ECProjR{\ECMV}}{\ZCProjR{\ZCCursor{\ECMV}}}{1} - } - - \inferrule[AEMProjRParent1]{ }{ - \ASEMParent{\ZCProjR{\ZCCursor{\ECMV}}}{\ECProjR{\ECMV}} - } - - \inferrule[AEMInconsistentTypesChild]{ - \ASEMChild{\ZCMV}{\ZCMV'}{\MChildNMV} - }{ - \ASEMChild{\ZCInconType{\ZCMV}}{\ZCInconType{\ZCMV'}}{\MChildNMV} - } - - \inferrule[AEMInconsistentTypesParent]{ - \ASEMParent{\ZCMV}{\ZCMV'} - }{ - \ASEMParent{\ZCInconType{\ZCMV}}{\ZCInconType{\ZCMV'}} - } - - \inferrule[AEMLamChild3]{ }{ - \ASEMChild{\ECLamInconAsc{x}{\TMV}{\ECMV}}{\ZCLamInconAscT{x}{\ZTCursor{\TMV}}{\ECMV}}{1} - } - - \inferrule[AEMLamChild4]{ }{ - \ASEMChild{\ECLamInconAsc{x}{\TMV}{\ECMV}}{\ZCLamInconAscE{x}{\TMV}{\ZCCursor{\ECMV}}}{2} - } - - \inferrule[AEMLamParent3]{ }{ - \ASEMParent{\ZCLamInconAscT{x}{\ZTCursor{\TMV}}{\ECMV}}{\ECLamInconAsc{x}{\TMV}{\ECMV}} - } - - \inferrule[AEMLamParent4]{ }{ - \ASEMParent{\ZCLamInconAscE{x}{\TMV}{\ZCCursor{\ECMV}}}{\ECLamInconAsc{x}{\TMV}{\ECMV}} - } - - \inferrule[AEMLamChild5]{ }{ - \ASEMChild{\ECLamAnaNonMatchedArrow{x}{\TMV}{\ECMV}}{\ZCLamAnaNonMatchedArrowT{x}{\ZTCursor{\TMV}}{\ECMV}}{1} - } - - \inferrule[AEMLamChild6]{ }{ - \ASEMChild{\ECLamAnaNonMatchedArrow{x}{\TMV}{\ECMV}}{\ZCLamAnaNonMatchedArrowE{x}{\TMV}{\ZCCursor{\ECMV}}}{2} - } - - \inferrule[AEMLamParent5]{ }{ - \ASEMParent{\ZCLamAnaNonMatchedArrowT{x}{\ZTCursor{\TMV}}{\ECMV}}{\ECLamAnaNonMatchedArrow{x}{\TMV}{\ECMV}} - } - - \inferrule[AEMLamParent6]{ }{ - \ASEMParent{\ZCLamAnaNonMatchedArrowE{x}{\TMV}{\ZCCursor{\ECMV}}}{\ECLamAnaNonMatchedArrow{x}{\TMV}{\ECMV}} - } - - \inferrule[AEMApChild3]{ }{ - \ASEMChild{\ECApSynNonMatchedArrow{\ECMV_1}{\ECMV_2}}{\ZCApSynNonMatchedArrowL{\ZCCursor{\ECMV_1}}{\ECMV_2}}{1} - } - - \inferrule[AEMApChild4]{ }{ - \ASEMChild{\ECApSynNonMatchedArrow{\ECMV_1}{\ECMV_2}}{\ZCApSynNonMatchedArrowR{\ECMV_1}{\ZCCursor{\ECMV_2}}}{2} - } - - \inferrule[AEMApParent3]{ }{ - \ASEMParent{\ZCApSynNonMatchedArrowL{\ZCCursor{\ECMV_1}}{\ECMV_2}}{\ECApSynNonMatchedArrow{\ECMV_1}{\ECMV_2}} - } - - \inferrule[AEMApParent4]{ }{ - \ASEMParent{\ZCApSynNonMatchedArrowR{\ECMV_1}{\ZCCursor{\ECMV_2}}}{\ECApSynNonMatchedArrow{\ECMV_1}{\ECMV_2}} - } - \inferrule[AEMInconsistentBranchesChild1]{ }{ \ASEMChild{\ECInconBr{\ECMV_1}{\ECMV_2}{\ECMV_3}}{\ZCInconBrC{\ZCCursor{\ECMV_1}}{\ECMV_2}{\ECMV_3}}{1} } @@ -486,6 +442,14 @@ \subsubsection{Expression movement} \ASEMParent{\ZCInconBrC{\ECMV_1}{\ECMV_2}{\ZCCursor{\ECMV_3}}}{\ECInconBr{\ECMV_1}{\ECMV_2}{\ECMV_3}} } + \inferrule[AEMPairChild1]{ }{ + \ASEMChild{\ECPair{\ECMV_1}{\ECMV_2}}{\ZCPairL{\ZCCursor{\ECMV_1}}{\ECMV_2}}{1} + } + + \inferrule[AEMPairChild2]{ }{ + \ASEMChild{\ECPair{\ECMV_1}{\ECMV_2}}{\ZCPairR{\ECMV_1}{\ZCCursor{\ECMV_2}}}{2} + } + \inferrule[AEMPairChild3]{ }{ \ASEMChild{\ECPairAnaNonMatchedProd{\ECMV_1}{\ECMV_2}}{\ZCPairAnaNonMatchedProdL{\ZCCursor{\ECMV_1}}{\ECMV_2}}{1} } @@ -494,6 +458,14 @@ \subsubsection{Expression movement} \ASEMChild{\ECPairAnaNonMatchedProd{\ECMV_1}{\ECMV_2}}{\ZCPairAnaNonMatchedProdR{\ECMV_1}{\ZCCursor{\ECMV_2}}}{2} } + \inferrule[AEMPairParent1]{ }{ + \ASEMParent{\ZCPairL{\ZCCursor{\ECMV_1}}{\ECMV_2}}{\ECPair{\ECMV_1}{\ECMV_2}} + } + + \inferrule[AEMPairParent2]{ }{ + \ASEMParent{\ZCPairR{\ECMV_1}{\ZCCursor{\ECMV_2}}}{\ECPair{\ECMV_1}{\ECMV_2}} + } + \inferrule[AEMPairParent3]{ }{ \ASEMParent{\ZCPairAnaNonMatchedProdL{\ZCCursor{\ECMV_1}}{\ECMV_2}}{\ECPairAnaNonMatchedProd{\ECMV_1}{\ECMV_2}} } @@ -502,21 +474,49 @@ \subsubsection{Expression movement} \ASEMParent{\ZCPairAnaNonMatchedProdR{\ECMV_1}{\ZCCursor{\ECMV_2}}}{\ECPairAnaNonMatchedProd{\ECMV_1}{\ECMV_2}} } + \inferrule[AEMProjLChild1]{ }{ + \ASEMChild{\ECProjL{\ECMV}}{\ZCProjL{\ZCCursor{\ECMV}}}{1} + } + \inferrule[AEMProjLChild2]{ }{ \ASEMChild{\ECProjLSynNonMatchedProd{\ECMV}}{\ZCProjLSynNonMatchedProd{\ZCCursor{\ECMV}}}{1} } + \inferrule[AEMProjLParent1]{ }{ + \ASEMParent{\ZCProjL{\ZCCursor{\ECMV}}}{\ECProjL{\ECMV}} + } + \inferrule[AEMProjLParent2]{ }{ \ASEMParent{\ZCProjLSynNonMatchedProd{\ZCCursor{\ECMV}}}{\ECProjLSynNonMatchedProd{\ECMV}} } + \inferrule[AEMProjRChild1]{ }{ + \ASEMChild{\ECProjR{\ECMV}}{\ZCProjR{\ZCCursor{\ECMV}}}{1} + } + \inferrule[AEMProjRChild2]{ }{ \ASEMChild{\ECProjRSynNonMatchedProd{\ECMV}}{\ZCProjRSynNonMatchedProd{\ZCCursor{\ECMV}}}{1} } + \inferrule[AEMProjRParent1]{ }{ + \ASEMParent{\ZCProjR{\ZCCursor{\ECMV}}}{\ECProjR{\ECMV}} + } + \inferrule[AEMProjRParent2]{ }{ \ASEMParent{\ZCProjRSynNonMatchedProd{\ZCCursor{\ECMV}}}{\ECProjRSynNonMatchedProd{\ECMV}} } + + \inferrule[AEMInconsistentTypesChild]{ + \ASEMChild{\ZCMV}{\ZCMV'}{\MChildNMV} + }{ + \ASEMChild{\ZCInconType{\ZCMV}}{\ZCInconType{\ZCMV'}}{\MChildNMV} + } + + \inferrule[AEMInconsistentTypesParent]{ + \ASEMParent{\ZCMV}{\ZCMV'} + }{ + \ASEMParent{\ZCInconType{\ZCMV}}{\ZCInconType{\ZCMV'}} + } \end{mathparpagebreakable} \subsubsection{Synthetic expression actions} From 08b97ab737a933099579ac14f1353c3de08eecf7 Mon Sep 17 00:00:00 2001 From: Eric Zhao <21zhaoe@protonmail.com> Date: Mon, 9 Oct 2023 00:47:58 -0400 Subject: [PATCH 07/24] formalism: Add missing synthetic con rules for marked zexp --- formalism/typed.tex | 32 ++++++++++++++++++++++++++++++++ 1 file changed, 32 insertions(+) diff --git a/formalism/typed.tex b/formalism/typed.tex index 25ddc82..2c91cba 100644 --- a/formalism/typed.tex +++ b/formalism/typed.tex @@ -632,6 +632,38 @@ \subsubsection{Synthetic expression actions} \inferrule[ASEConIfR]{ }{ \ASCon{\ctx}{\ZCCursor{\ECMV}}{\TMV}{\ZCIfC{\ZCCursor{\ECEHole}}{\ECEHole}{\ECMV}}{\TMV}{\SIfR} } + + \inferrule[ASEConPairL]{ }{ + \ASCon{\ctx}{\ZCCursor{\ECMV}}{\TMV}{\ZCPairL{\ZCCursor{\ECMV}}{\ECEHole}}{\TProd{\TMV}{\TUnknown}}{\SPairL} + } + + \inferrule[ASEConPairR]{ }{ + \ASCon{\ctx}{\ZCCursor{\ECMV}}{\TMV}{\ZCPairR{\ECEHole}{\ZCCursor{\ECMV}}}{\TProd{\TUnknown}{\TMV}}{\SPairR} + } + + \inferrule[ASEConProjL1]{ + \matchedProd{\TMV}{\TMV_1}{\TMV_2} + }{ + \ASCon{\ctx}{\ZCCursor{\ECMV}}{\TMV}{\ZCProjL{\ZCCursor{\ECMV}}}{\TMV_1}{\SProjL} + } + + \inferrule[ASEConProjL2]{ + \notMatchedProd{\TMV} + }{ + \ASCon{\ctx}{\ZCCursor{\ECMV}}{\TMV}{\ZCProjLSynNonMatchedProd{\ZCCursor{\ECMV}}}{\TUnknown}{\SProjL} + } + + \inferrule[ASEConProjR1]{ + \matchedProd{\TMV}{\TMV_1}{\TMV_2} + }{ + \ASCon{\ctx}{\ZCCursor{\ECMV}}{\TMV}{\ZCProjR{\ZCCursor{\ECMV}}}{\TMV_2}{\SProjR} + } + + \inferrule[ASEConProjR2]{ + \notMatchedProd{\TMV} + }{ + \ASCon{\ctx}{\ZCCursor{\ECMV}}{\TMV}{\ZCProjRSynNonMatchedProd{\ZCCursor{\ECMV}}}{\TUnknown}{\SProjR} + } \end{mathparpagebreakable} \paragraph{Zipper Cases} \ \\ From 670d20e0ed43c12bf76bff8265810e9ec407a3cc Mon Sep 17 00:00:00 2001 From: Eric Zhao <21zhaoe@protonmail.com> Date: Mon, 9 Oct 2023 01:38:45 -0400 Subject: [PATCH 08/24] formalism: Add missing synthetic zipper rules for marked zexp --- formalism/typed.tex | 84 ++++++++++++++++++++++++++++++++++++++++++--- 1 file changed, 79 insertions(+), 5 deletions(-) diff --git a/formalism/typed.tex b/formalism/typed.tex index 2c91cba..40b0dc7 100644 --- a/formalism/typed.tex +++ b/formalism/typed.tex @@ -709,10 +709,10 @@ \subsubsection{Synthetic expression actions} \inferrule[ASEZipApL3]{ \ctxSynTypeM{\ctx}{\cursorErase{\ZCMV_1}}{\TMV_1} \\ - \ASEAction{\ctx}{\ZCMV}{\TMV_1}{\ZCMV'}{\TMV_1'}{\AMV} \\\\ + \ASEAction{\ctx}{\ZCMV_1}{\TMV_1}{\ZCMV_1'}{\TMV_1'}{\AMV} \\\\ \notMatchedArrow{\TMV_1'} }{ - \ASEAction{\ctx}{\ZCApL{\ZCMV_1}{\ECMV_2}}{\TMV}{\ZCApL{\ECInconType{\ZCMV_1'}}{\ECMV_2}}{\TUnknown}{\AMV} + \ASEAction{\ctx}{\ZCApL{\ZCMV_1}{\ECMV_2}}{\TMV}{\ZCApSynNonMatchedArrowL{\ZCMV_1'}{\ECMV_2}}{\TUnknown}{\AMV} } \inferrule[ASEZipApL4]{ @@ -741,7 +741,7 @@ \subsubsection{Synthetic expression actions} \ASEAction{\ctx}{\ZCApL{\ECInconType{\ZCMV_1}}{\ECMV_2}}{\TUnknown}{\ZCApL{\ECInconType{\ZCMV_1'}}{\ECMV_2}}{\TUnknown}{\AMV} } - \inferrule[ASEZipApR]{ + \inferrule[ASEZipApR1]{ \ctxSynTypeM{\ctx}{\ECMV_1}{\TMV_1} \\ \matchedArrow{\TMV_1}{\TMV_2}{\TMV_3} \\ \AAEAction{\ctx}{\ZCMV_2}{\ZCMV_2'}{\TMV_2}{\AMV} @@ -749,10 +749,16 @@ \subsubsection{Synthetic expression actions} \ASEAction{\ctx}{\ZCApR{\ECMV_1}{\ZCMV_2}}{\TMV}{\ZCApR{\ECMV_1}{\ZCMV_2'}}{\TMV_3}{\AMV} } + \inferrule[ASEZipApR2]{ + \AAEAction{\ctx}{\ZCMV_2}{\ZCMV_2'}{\TUnknown}{\AMV} + }{ + \ASEAction{\ctx}{\ZCApSynNonMatchedArrowR{\ECMV_1}{\ZCMV_2}}{\TUnknown}{\ZCApSynNonMatchedArrowR{\ECMV_1}{\ZCMV_2'}}{\TUnknown}{\AMV} + } + \inferrule[ASEZipLetL1]{ \ctxSynTypeM{\ctx}{\cursorErase{\ZCMV_1}}{\TMV_1} \\ \ASEAction{\ctx}{\ZCMV_1}{\TMV_1}{\ZCMV_1'}{\TMV_1'}{\AMV} \\ - \consistent{\TMV_1}{\TMV_1'} + \equal{\TMV_1}{\TMV_1'} }{ \ASEAction{\ctx}{\ZCLetL{x}{\ZCMV_1}{\ECMV_2}}{\TMV_2}{\ZCLetL{x}{\ZCMV_1'}{\ECMV_2}}{\TMV_2}{\AMV} } @@ -760,7 +766,7 @@ \subsubsection{Synthetic expression actions} \inferrule[ASEZipLetL2]{ \ctxSynTypeM{\ctx}{\cursorErase{\ZCMV_1}}{\TMV_1} \\ \ASEAction{\ctx}{\ZCMV_1}{\TMV_1}{\ZCMV_1'}{\TMV_1'}{\AMV} \\\\ - \inconsistent{\TMV_1}{\TMV_1'} \\ + \notEqual{\TMV_1}{\TMV_1'} \\ \ctxSynFixedInto{\extendCtx{\ctx}{x}{\TMV_1'}}{\erase{\ECMV_2}}{\ECMV_2'}{\TMV_2'} }{ \ASEAction{\ctx}{\ZCLetL{x}{\ZCMV_1}{\ECMV_2}}{\TMV_2}{\ZCLetL{x}{\ZCMV_1'}{\ECMV_2'}}{\TMV_2'}{\AMV} @@ -865,6 +871,74 @@ \subsubsection{Synthetic expression actions} }{ \ASEAction{\ctx}{\ZCInconBrR{\ECMV_1}{\ECMV_2}{\ZCMV}}{\TMV}{\ZCInconBrR{\ECMV_1}{\ECMV_2}{\ZCMV'}}{\TUnknown}{\AMV} } + + \inferrule[ASEZipPairL]{ + \ASEAction{\ctx}{\ZCMV}{\TMV_1}{\ZCMV'}{\TMV_1'}{\AMV} + }{ + \ASEAction{\ctx}{\ZCPairL{\ZCMV}{\ECMV}}{\TProd{\TMV_1}{\TMV_2}}{\ZCPairL{\ZCMV'}{\ECMV}}{\TProd{\TMV_1'}{\TMV_2}}{\AMV} + } + + \inferrule[ASEZipPairR]{ + \ASEAction{\ctx}{\ZCMV}{\TMV_2}{\ZCMV'}{\TMV_2'}{\AMV} + }{ + \ASEAction{\ctx}{\ZCPairR{\ECMV}{\ZCMV}}{\TProd{\TMV_1}{\TMV_2}}{\ZCPairR{\ECMV}{\ZCMV'}}{\TProd{\TMV_1'}{\TMV_2}}{\AMV} + } + + \inferrule[ASEZipProjL1]{ + \ASEAction{\ctx}{\ZCMV}{\TMV}{\ZCMV'}{\TMV'}{\AMV} \\ + \matchedProd{\TMV'}{\TMV_1'}{\TMV_2'} + }{ + \ASEAction{\ctx}{\ZCProjL{\ZCMV}}{\TMV_1}{\ZCProjL{\ZCMV'}}{\TMV_1'}{\AMV} + } + + \inferrule[ASEZipProjL2]{ + \ASEAction{\ctx}{\ZCMV}{\TMV}{\ZCMV'}{\TMV'}{\AMV} \\ + \notMatchedProd{\TMV'} + }{ + \ASEAction{\ctx}{\ZCProjL{\ZCMV}}{\TMV_1}{\ZCProjLSynNonMatchedProd{\ZCMV'}}{\TUnknown}{\AMV} + } + + \inferrule[ASEZipProjL3]{ + \ASEAction{\ctx}{\ZCMV}{\TMV}{\ZCMV'}{\TMV'}{\AMV} \\ + \matchedProd{\TMV'}{\TMV_1'}{\TMV_2'} + }{ + \ASEAction{\ctx}{\ZCProjLSynNonMatchedProd{\ZCMV}}{\TUnknown}{\ZCProjL{\ZCMV'}}{\TMV_1'}{\AMV} + } + + \inferrule[ASEZipProjL4]{ + \ASEAction{\ctx}{\ZCMV}{\TMV}{\ZCMV'}{\TMV'}{\AMV} \\ + \notMatchedProd{\TMV'} + }{ + \ASEAction{\ctx}{\ZCProjLSynNonMatchedProd{\ZCMV}}{\TUnknown}{\ZCProjLSynNonMatchedProd{\ZCMV'}}{\TUnknown}{\AMV} + } + + \inferrule[ASEZipProjR1]{ + \ASEAction{\ctx}{\ZCMV}{\TMV}{\ZCMV'}{\TMV'}{\AMV} \\ + \matchedProd{\TMV'}{\TMV_1'}{\TMV_2'} + }{ + \ASEAction{\ctx}{\ZCProjR{\ZCMV}}{\TMV_2}{\ZCProjR{\ZCMV'}}{\TMV_2'}{\AMV} + } + + \inferrule[ASEZipProjR2]{ + \ASEAction{\ctx}{\ZCMV}{\TMV}{\ZCMV'}{\TMV'}{\AMV} \\ + \notMatchedProd{\TMV'} + }{ + \ASEAction{\ctx}{\ZCProjR{\ZCMV}}{\TMV_2}{\ZCProjRSynNonMatchedProd{\ZCMV'}}{\TUnknown}{\AMV} + } + + \inferrule[ASEZipProjL3]{ + \ASEAction{\ctx}{\ZCMV}{\TMV}{\ZCMV'}{\TMV'}{\AMV} \\ + \matchedProd{\TMV'}{\TMV_1'}{\TMV_2'} + }{ + \ASEAction{\ctx}{\ZCProjRSynNonMatchedProd{\ZCMV}}{\TUnknown}{\ZCProjR{\ZCMV'}}{\TMV_2'}{\AMV} + } + + \inferrule[ASEZipProjR4]{ + \ASEAction{\ctx}{\ZCMV}{\TMV}{\ZCMV'}{\TMV'}{\AMV} \\ + \notMatchedProd{\TMV'} + }{ + \ASEAction{\ctx}{\ZCProjRSynNonMatchedProd{\ZCMV}}{\TUnknown}{\ZCProjRSynNonMatchedProd{\ZCMV'}}{\TUnknown}{\AMV} + } \end{mathparpagebreakable} \subsubsection{Analytic expression actions} From 220a6c0328ea93af0351e320de035e1fd6492779 Mon Sep 17 00:00:00 2001 From: Eric Zhao <21zhaoe@protonmail.com> Date: Mon, 9 Oct 2023 02:35:20 -0400 Subject: [PATCH 09/24] formalism: Fix typed con rules with mode change --- formalism/typed.tex | 44 ++++++++++++++------------------------------ 1 file changed, 14 insertions(+), 30 deletions(-) diff --git a/formalism/typed.tex b/formalism/typed.tex index 40b0dc7..b1b5676 100644 --- a/formalism/typed.tex +++ b/formalism/typed.tex @@ -571,8 +571,10 @@ \subsubsection{Synthetic expression actions} \ASCon{\ctx}{\ZCCursor{\ECMV}}{\TMV}{\ZCApL{\ECInconType{\ECMV}}{\ZCCursor{\ECEHole}}}{\TUnknown}{\SApL} } - \inferrule[ASEConApR]{ }{ - \ASCon{\ctx}{\ZCCursor{\ECMV}}{\TMV}{\ZCApR{\ZCCursor{\ECEHole}}{\ECMV}}{\TUnknown}{\SApR} + \inferrule[ASEConApR]{ + \ctxAnaFixedInto{\ctx}{\erase{\ECMV}}{\ECMV'}{\TUnknown} + }{ + \ASCon{\ctx}{\ZCCursor{\ECMV}}{\TMV}{\ZCApR{\ZCCursor{\ECEHole}}{\ECMV'}}{\TUnknown}{\SApR} } \inferrule[ASEConLet1]{ }{ @@ -589,40 +591,22 @@ \subsubsection{Synthetic expression actions} \ASCon{\ctx}{\ZCCursor{\ECEHole}}{\TUnknown}{\ZCCursor{\ENumMV}}{\TNum}{\SLit{\ENumMV}} } - \inferrule[ASEConPlusL1]{ - \consistent{\TMV}{\TNum} - }{ - \ASCon{\ctx}{\ZCCursor{\ECMV}}{\TMV}{\ZCPlusR{\ECMV}{\ZCCursor{\ECEHole}}}{\TNum}{\SPlusL} - } - - \inferrule[ASEConPlusL2]{ - \inconsistent{\TMV}{\TNum} - }{ - \ASCon{\ctx}{\ZCCursor{\ECMV}}{\TMV}{\ZCPlusR{\ECInconType{\ECMV}}{\ZCCursor{\ECEHole}}}{\TNum}{\SPlusL} - } \\ - - \inferrule[ASEConPlusR1]{ - \consistent{\TMV}{\TNum} - }{ - \ASCon{\ctx}{\ZCCursor{\ECMV}}{\TMV}{\ZCPlusL{\ZCCursor{\ECEHole}}{\ECMV}}{\TNum}{\SPlusR} - } - - \inferrule[ASEConPlusR2]{ - \inconsistent{\TMV}{\TNum} + \inferrule[ASEConPlusL]{ + \ctxAnaFixedInto{\ctx}{\erase{\ECMV}}{\ECMV'}{\TNum} }{ - \ASCon{\ctx}{\ZCCursor{\ECMV}}{\TMV}{\ZCPlusL{\ZCCursor{\ECEHole}}{\ECInconType{\ECMV}}}{\TNum}{\SPlusR} + \ASCon{\ctx}{\ZCCursor{\ECMV}}{\TMV}{\ZCPlusR{\ECMV'}{\ZCCursor{\ECEHole}}}{\TNum}{\SPlusL} } - \inferrule[ASEConIfC1]{ - \consistent{\TMV}{\TBool} + \inferrule[ASEConPlusR]{ + \ctxAnaFixedInto{\ctx}{\erase{\ECMV}}{\ECMV'}{\TNum} }{ - \ASCon{\ctx}{\ZCCursor{\ECMV}}{\TMV}{\ZCIfL{\ECMV}{\ZCCursor{\ECEHole}}{\ECEHole}}{\TUnknown}{\SIfC} + \ASCon{\ctx}{\ZCCursor{\ECMV}}{\TMV}{\ZCPlusL{\ZCCursor{\ECEHole}}{\ECMV'}}{\TNum}{\SPlusR} } - \inferrule[ASEConIfC2]{ - \inconsistent{\TMV}{\TBool} + \inferrule[ASEConIfC]{ + \ctxAnaFixedInto{\ctx}{\erase{\ECMV}}{\ECMV'}{\TBool} }{ - \ASCon{\ctx}{\ZCCursor{\ECMV}}{\TMV}{\ZCIfL{\ECInconType{\ECMV}}{\ZCCursor{\ECEHole}}{\ECEHole}}{\TUnknown}{\SIfC} + \ASCon{\ctx}{\ZCCursor{\ECMV}}{\TMV}{\ZCIfL{\ECMV'}{\ZCCursor{\ECEHole}}{\ECEHole}}{\TUnknown}{\SIfC} } \inferrule[ASEConIfL]{ }{ @@ -641,7 +625,7 @@ \subsubsection{Synthetic expression actions} \ASCon{\ctx}{\ZCCursor{\ECMV}}{\TMV}{\ZCPairR{\ECEHole}{\ZCCursor{\ECMV}}}{\TProd{\TUnknown}{\TMV}}{\SPairR} } - \inferrule[ASEConProjL1]{ + \inferrule[ASEConProjL]{ \matchedProd{\TMV}{\TMV_1}{\TMV_2} }{ \ASCon{\ctx}{\ZCCursor{\ECMV}}{\TMV}{\ZCProjL{\ZCCursor{\ECMV}}}{\TMV_1}{\SProjL} From e90b60579ebf85fc45a071e3d69864a594574791 Mon Sep 17 00:00:00 2001 From: Eric Zhao <21zhaoe@protonmail.com> Date: Mon, 9 Oct 2023 02:46:34 -0400 Subject: [PATCH 10/24] formalism: Add mising analytic con rules for typed model --- formalism/typed.tex | 57 ++++++++++++++++++++++++++++++++++++--------- 1 file changed, 46 insertions(+), 11 deletions(-) diff --git a/formalism/typed.tex b/formalism/typed.tex index b1b5676..13a8176 100644 --- a/formalism/typed.tex +++ b/formalism/typed.tex @@ -952,19 +952,19 @@ \subsubsection{Analytic expression actions} \inferrule[AAEInconsistentTypes1]{ \ctxSynTypeM{\ctx}{\cursorErase{\ZCMV}}{\TMV'} \\ \ASAction{\ctx}{\ZCMV}{\TMV'}{\ZCMV'}{\TMV''}{\AMV} \\\\ - \inconsistent{\TMV}{\TMV''} \\ + \consistent{\TMV}{\TMV''} \\ \subsumable{\cursorErase{\ZCMV}} }{ - \AAAction{\ctx}{\ZCInconType{\ZCMV}}{\ZCInconType{\ZCMV'}}{\TMV}{\AMV} + \AAAction{\ctx}{\ZCInconType{\ZCMV}}{\ZCMV'}{\TMV}{\AMV} } \inferrule[AAEInconsistentTypes2]{ \ctxSynTypeM{\ctx}{\cursorErase{\ZCMV}}{\TMV'} \\ \ASAction{\ctx}{\ZCMV}{\TMV'}{\ZCMV'}{\TMV''}{\AMV} \\\\ - \consistent{\TMV}{\TMV''} \\ + \inconsistent{\TMV}{\TMV''} \\ \subsumable{\cursorErase{\ZCMV}} }{ - \AAAction{\ctx}{\ZCInconType{\ZCMV}}{\ZCMV'}{\TMV}{\AMV} + \AAAction{\ctx}{\ZCInconType{\ZCMV}}{\ZCInconType{\ZCMV'}}{\TMV}{\AMV} } \end{mathpar} @@ -988,20 +988,22 @@ \subsubsection{Analytic expression actions} \begin{mathparpagebreakable} \inferrule[AAEConLam1]{ \matchedArrow{\TMV}{\TMV_1}{\TMV_2} \\ - \ctxAnaFixedInto{\extendCtx{\ctx}{x}{\TMV_1}}{\ECMV}{\ECMV'}{\TMV_2} + \ctxAnaFixedInto{\extendCtx{\ctx}{x}{\TMV_1}}{\erase{\ECMV}}{\ECMV'}{\TMV_2} }{ \AACon{\ctx}{\ZCCursor{\ECMV}}{\ZCLamT{x}{\ZTCursor{\TMV_1}}{\ECMV'}}{\TMV}{\SLam{x}} } \inferrule[AAEConLam2]{ \notMatchedArrow{\TMV} \\ - \ctxAnaFixedInto{\extendCtx{\ctx}{x}{\TUnknown}}{\ECMV}{\ECMV'}{\TUnknown} + \ctxAnaFixedInto{\extendCtx{\ctx}{x}{\TUnknown}}{\erase{\ECMV}}{\ECMV'}{\TUnknown} }{ \AACon{\ctx}{\ZCCursor{\ECMV}}{\ZCInconType{\ZCLamT{x}{\ZTCursor{\TUnknown}}{\ECMV'}}}{\TMV}{\SLam{x}} } - \inferrule[AAEConLetL]{ }{ - \AACon{\ctx}{\ZCCursor{\ECMV}}{\ZCLetL{x}{\ECMV}{\ZCCursor{\ECEHole}}}{\TMV}{\SLetL{x}} + \inferrule[AAEConLetL]{ + \ctxSynFixedInto{\ctx}{\erase{\ECMV}}{\ECMV'}{\TMV} + }{ + \AACon{\ctx}{\ZCCursor{\ECMV}}{\ZCLetL{x}{\ECMV'}{\ZCCursor{\ECEHole}}}{\TMV}{\SLetL{x}} } \inferrule[AAEConLetR]{ @@ -1010,13 +1012,46 @@ \subsubsection{Analytic expression actions} \AACon{\ctx}{\ZCCursor{\ECMV}}{\ZCLetR{x}{\ZCCursor{\ECEHole}}{\ECMV'}}{\TMV}{\SLetR{x}} } + \inferrule[AAEConIfC]{ + \ctxAnaFixedInto{\ctx}{\ECMV}{\ECMV'}{\TBool} + }{ + \AACon{\ctx}{\ZCCursor{\ECMV}}{\ZCIfL{\ECMV'}{\ZCCursor{\ECEHole}}{\ECEHole}}{\TMV}{\SIfC} + } + \inferrule[AAEConIfL]{ }{ - \AACon{\ctx}{\ZCCursor{\ECMV}}{\ZCIfC{\ZCCursor{\ECEHole}}{\ECMV}{\ECEHole}}{\TMV}{\SIfL} + \AACon{\ctx}{\ZCCursor{\ECMV}}{\ZCIfC{\ZCCursor{\ECEHole}}{\ECMV'}{\ECEHole}}{\TMV}{\SIfL} } - \inferrule[AAEConIfR]{ + \inferrule[AAEConIfR]{ }{ + \AACon{\ctx}{\ZCCursor{\ECMV}}{\ZCIfC{\ZCCursor{\ECEHole}}{\ECEHole}{\ECMV'}}{\TMV}{\SIfR} + } + + \inferrule[AAEConPairL1]{ + \matchedProd{\TMV}{\TMV_1}{\TMV_2} \\ + \ctxAnaFixedInto{\ctx}{\erase{\ECMV}}{\ECMV'}{\TMV_1} + }{ + \AACon{\ctx}{\ZCursor{\ECMV}}{\ZCPairL{\ECMV'}{\ZCursor{\ECEHole}}}{\TMV}{\SPairL} + } + + \inferrule[AAEConPairL2]{ + \notMatchedProd{\TMV} \\ + \ctxAnaFixedInto{\ctx}{\erase{\ECMV}}{\ECMV'}{\TUnknown} + }{ + \AACon{\ctx}{\ZCursor{\ECMV}}{\ZCPairAnaNonMatchedProdL{\ECMV'}{\ZCursor{\ECEHole}}}{\TMV}{\SPairL} + } + + \inferrule[AAEConPairR1]{ + \matchedProd{\TMV}{\TMV_1}{\TMV_2} \\ + \ctxAnaFixedInto{\ctx}{\erase{\ECMV}}{\ECMV'}{\TMV_2} + }{ + \AACon{\ctx}{\ZCursor{\ECMV}}{\ZCPairR{\ZCursor{\ECEHole}}{\ECMV'}}{\TMV}{\SPairR} + } + + \inferrule[AAEConPairR2]{ + \notMatchedProd{\TMV} \\ + \ctxAnaFixedInto{\ctx}{\erase{\ECMV}}{\ECMV'}{\TUnknown} }{ - \AACon{\ctx}{\ZCCursor{\ECMV}}{\ZCIfC{\ZCCursor{\ECEHole}}{\ECEHole}{\ECMV}}{\TMV}{\SIfR} + \AACon{\ctx}{\ZCursor{\ECMV}}{\ZCPairAnaNonMatchedProdR{\ZCursor{\ECEHole}}{\ECMV'}}{\TMV}{\SPairR} } \end{mathparpagebreakable} From 31c49241f09bbe5b3f01400ab2528eb918745eca Mon Sep 17 00:00:00 2001 From: Eric Zhao <21zhaoe@protonmail.com> Date: Mon, 9 Oct 2023 13:43:01 -0400 Subject: [PATCH 11/24] formalism: Fix some analytic zipper rules for marked zexp lambda --- formalism/typed.tex | 32 +++++++++++++++++++------------- 1 file changed, 19 insertions(+), 13 deletions(-) diff --git a/formalism/typed.tex b/formalism/typed.tex index 13a8176..7442847 100644 --- a/formalism/typed.tex +++ b/formalism/typed.tex @@ -1058,33 +1058,39 @@ \subsubsection{Analytic expression actions} \paragraph{Zipper Cases} \ \\ \begin{mathparpagebreakable} \inferrule[AAEZipLamT1]{ - \AUTAction{\ZTMV}{\ZTMV'}{\AMV} \\ - \consistent{\cursorErase{\ZTMV}}{\cursorErase{\ZTMV'}} + \AUTAction{\ZTMV_3}{\ZTMV_3'}{\AMV} \\ + \equal{\cursorErase{\ZTMV_3}}{\cursorErase{\ZTMV_3'}} }{ - \AAAction{\ctx}{\ZCLamT{x}{\ZTMV}{\ECMV}}{\ZCLamT{x}{\ZTMV'}{\ECMV}}{\TMV}{\AMV} + \AAAction{\ctx}{\ZCLamT{x}{\ZTMV_3}{\ECMV}}{\ZCLamT{x}{\ZTMV_3'}{\ECMV}}{\TMV}{\AMV} } \inferrule[AAEZipLamT2]{ - \AUTAction{\ZTMV}{\ZTMV'}{\AMV} \\ - \inconsistent{\cursorErase{\ZTMV}}{\cursorErase{\ZTMV'}} \\ + \AUTAction{\ZTMV_3}{\ZTMV_3'}{\AMV} \\ + \notEqual{\cursorErase{\ZTMV_3}}{\cursorErase{\ZTMV_3'}} \\ \matchedArrow{\TMV}{\TMV_1}{\TMV_2} \\\\ - \consistent{\cursorErase{\ZTMV'}}{\TMV_1} \\ - \ctxAnaFixedInto{\extendCtx{\ctx}{x}{\cursorErase{\ZTMV'}}}{\erase{\ECMV}}{\ECMV'}{\TMV_2} + \consistent{\cursorErase{\ZTMV_3'}}{\TMV_1} \\ + \ctxAnaFixedInto{\extendCtx{\ctx}{x}{\cursorErase{\ZTMV_3'}}}{\erase{\ECMV}}{\ECMV'}{\TMV_2} }{ - \AAAction{\ctx}{\ZCLamT{x}{\ZTMV}{\ECMV}}{\ZCLamT{x}{\ZTMV'}{\ECMV'}}{\TMV}{\AMV} + \AAAction{\ctx}{\ZCLamT{x}{\ZTMV_3}{\ECMV}}{\ZCLamT{x}{\ZTMV_3'}{\ECMV'}}{\TMV}{\AMV} } \inferrule[AAEZipLamT3]{ - \AUTAction{\ZTMV}{\ZTMV'}{\AMV} \\ - \inconsistent{\cursorErase{\ZTMV}}{\cursorErase{\ZTMV'}} \\ + \AUTAction{\ZTMV_3}{\ZTMV_3'}{\AMV} \\ + \notEqual{\cursorErase{\ZTMV_3}}{\cursorErase{\ZTMV'}} \\ \matchedArrow{\TMV}{\TMV_1}{\TMV_2} \\\\ - \inconsistent{\cursorErase{\ZTMV'}}{\TMV_1} \\ + \inconsistent{\cursorErase{\ZTMV_3'}}{\TMV_1} \\ \ctxAnaFixedInto{\extendCtx{\ctx}{x}{\TMV_1}}{\erase{\ECMV}}{\ECMV'}{\TMV_2} }{ - \AAAction{\ctx}{\ZCLamT{x}{\ZTMV}{\ECMV}}{\ZCInconType{\ZCLamT{x}{\ZTMV'}{\ECMV'}}}{\TMV}{\AMV} + \AAAction{\ctx}{\ZCLamT{x}{\ZTMV_3}{\ECMV}}{\ZCInconType{\ZCLamT{x}{\ZTMV_3'}{\ECMV'}}}{\TMV}{\AMV} } - \inferrule[AAEZipLamE]{ + \inferrule[AAEZipLamT4]{ + \AUTAction{\ZTMV_3}{\ZTMV_3'}{\AMV} \\ + }{ + \AAAction{\ctx}{\ZCLamAnaNonMatchedArrowT{x}{\ZTMV_3}{\ECMV}}{\ZCLamT{x}{\ZTMV_3'}{\ECMV}}{\TMV}{\AMV} + } + + \inferrule[AAEZipLamE1]{ \matchedArrow{\TMV}{\TMV_1}{\TMV_2} \\ \AAAction{\extendCtx{\ctx}{x}{\TMV_3}}{\ZCMV}{\ZCMV'}{\TMV_2}{\AMV} }{ From 0b53159c752d904ce45c5658d4cc4a2b8c830c52 Mon Sep 17 00:00:00 2001 From: Eric Zhao <21zhaoe@protonmail.com> Date: Tue, 10 Oct 2023 01:18:13 -0400 Subject: [PATCH 12/24] formalism: Fix and add missing analytic zipper rules for zippered marked lambda --- formalism/typed.tex | 57 +++++++++++++++++++++++++++++++++++++++++---- 1 file changed, 53 insertions(+), 4 deletions(-) diff --git a/formalism/typed.tex b/formalism/typed.tex index 7442847..0d27e78 100644 --- a/formalism/typed.tex +++ b/formalism/typed.tex @@ -997,7 +997,7 @@ \subsubsection{Analytic expression actions} \notMatchedArrow{\TMV} \\ \ctxAnaFixedInto{\extendCtx{\ctx}{x}{\TUnknown}}{\erase{\ECMV}}{\ECMV'}{\TUnknown} }{ - \AACon{\ctx}{\ZCCursor{\ECMV}}{\ZCInconType{\ZCLamT{x}{\ZTCursor{\TUnknown}}{\ECMV'}}}{\TMV}{\SLam{x}} + \AACon{\ctx}{\ZCCursor{\ECMV}}{\ZCLamAnaNonMatchedArrowT{x}{\ZTCursor{\TUnknown}}{\ECMV'}}{\TMV}{\SLam{x}} } \inferrule[AAEConLetL]{ @@ -1079,15 +1079,51 @@ \subsubsection{Analytic expression actions} \notEqual{\cursorErase{\ZTMV_3}}{\cursorErase{\ZTMV'}} \\ \matchedArrow{\TMV}{\TMV_1}{\TMV_2} \\\\ \inconsistent{\cursorErase{\ZTMV_3'}}{\TMV_1} \\ - \ctxAnaFixedInto{\extendCtx{\ctx}{x}{\TMV_1}}{\erase{\ECMV}}{\ECMV'}{\TMV_2} + \ctxAnaFixedInto{\extendCtx{\ctx}{x}{\cursorErase{\ZTMV_3'}}}{\erase{\ECMV}}{\ECMV'}{\TMV_2} }{ - \AAAction{\ctx}{\ZCLamT{x}{\ZTMV_3}{\ECMV}}{\ZCInconType{\ZCLamT{x}{\ZTMV_3'}{\ECMV'}}}{\TMV}{\AMV} + \AAAction{\ctx}{\ZCLamT{x}{\ZTMV_3}{\ECMV}}{\ZCLamInconAscT{x}{\ZTMV_3'}{\ECMV'}}{\TMV}{\AMV} } \inferrule[AAEZipLamT4]{ \AUTAction{\ZTMV_3}{\ZTMV_3'}{\AMV} \\ + \equal{\cursorErase{\ZTMV_3}}{\cursorErase{\ZTMV_3'}} + }{ + \AAAction{\ctx}{\ZCLamAnaNonMatchedArrowT{x}{\ZTMV_3}{\ECMV}}{\ZCLamAnaNonMatchedArrowT{x}{\ZTMV_3'}{\ECMV}}{\TMV}{\AMV} + } + + \inferrule[AAEZipLamT5]{ + \AUTAction{\ZTMV_3}{\ZTMV_3'}{\AMV} \\ + \notEqual{\cursorErase{\ZTMV_3}}{\cursorErase{\ZTMV_3'}} \\\\ + \ctxAnaFixedInto{\extendCtx{\ctx}{x}{\cursorErase{\ZTMV_3'}}}{\erase{\ECMV}}{\ECMV'}{\TUnknown} + }{ + \AAAction{\ctx}{\ZCLamAnaNonMatchedArrowT{x}{\ZTMV_3}{\ECMV}}{\ZCLamAnaNonMatchedArrowT{x}{\ZTMV_3'}{\ECMV}}{\TMV}{\AMV} + } + + \inferrule[AAEZipLamT6]{ + \AUTAction{\ZTMV_3}{\ZTMV_3'}{\AMV} \\ + \equal{\cursorErase{\ZTMV_3}}{\cursorErase{\ZTMV_3'}} + }{ + \AAAction{\ctx}{\ZCLamInconAscT{x}{\ZTMV_3}{\ECMV}}{\ZCLamInconAscT{x}{\ZTMV_3'}{\ECMV}}{\TMV}{\AMV} + } + + \inferrule[AAEZipLamT7]{ + \AUTAction{\ZTMV_3}{\ZTMV_3'}{\AMV} \\ + \notEqual{\cursorErase{\ZTMV_3}}{\cursorErase{\ZTMV_3'}} \\ + \matchedArrow{\TMV}{\TMV_1}{\TMV_2} \\\\ + \consistent{\cursorErase{\ZTMV_3'}}{\TMV_1} \\ + \ctxAnaFixedInto{\extendCtx{\ctx}{x}{\cursorErase{\ZTMV_3'}}}{\erase{\ECMV}}{\ECMV'}{\TMV_2} + }{ + \AAAction{\ctx}{\ZCLamInconAscT{x}{\ZTMV_3}{\ECMV}}{\ZCLamT{x}{\ZTMV_3'}{\ECMV'}}{\TMV}{\AMV} + } + + \inferrule[AAEZipLamT8]{ + \AUTAction{\ZTMV_3}{\ZTMV_3'}{\AMV} \\ + \notEqual{\cursorErase{\ZTMV_3}}{\cursorErase{\ZTMV_3'}} \\ + \matchedArrow{\TMV}{\TMV_1}{\TMV_2} \\\\ + \inconsistent{\cursorErase{\ZTMV_3'}}{\TMV_1} \\ + \ctxAnaFixedInto{\extendCtx{\ctx}{x}{\cursorErase{\ZTMV_3'}}}{\erase{\ECMV}}{\ECMV'}{\TMV_2} }{ - \AAAction{\ctx}{\ZCLamAnaNonMatchedArrowT{x}{\ZTMV_3}{\ECMV}}{\ZCLamT{x}{\ZTMV_3'}{\ECMV}}{\TMV}{\AMV} + \AAAction{\ctx}{\ZCLamInconAscT{x}{\ZTMV_3}{\ECMV}}{\ZCLamInconAscT{x}{\ZTMV_3'}{\ECMV'}}{\TMV}{\AMV} } \inferrule[AAEZipLamE1]{ @@ -1097,6 +1133,19 @@ \subsubsection{Analytic expression actions} \AAAction{\ctx}{\ZCLamE{x}{\TMV_3}{\ZCMV}}{\ZCLamE{x}{\TMV_3}{\ZCMV'}}{\TMV}{\AMV} } + \inferrule[AAEZipLamE2]{ + \AAAction{\extendCtx{\ctx}{x}{\TMV_3}}{\ZCMV}{\ZCMV'}{\TUnknown}{\AMV} + }{ + \AAAction{\ctx}{\ZCLamAnaNonMatchedArrowE{x}{\TMV_3}{\ZCMV}}{\ZCLamAnaNonMatchedArrowE{x}{\TMV_3}{\ZCMV'}}{\TMV}{\AMV} + } + + \inferrule[AAEZipLamE3]{ + \matchedArrow{\TMV}{\TMV_1}{\TMV_2} \\ + \AAAction{\extendCtx{\ctx}{x}{\TMV_3}}{\ZCMV}{\ZCMV'}{\TMV_2}{\AMV} + }{ + \AAAction{\ctx}{\ZCLamInconAscE{x}{\TMV_3}{\ZCMV}}{\ZCLamInconAscE{x}{\TMV_3}{\ZCMV'}}{\TMV}{\AMV} + } + \inferrule[AAEZipLetL1]{ \ctxSynTypeM{\ctx}{\cursorErase{\ZCMV}}{\TMV_1} \\ \ASEAction{\ctx}{\ZCMV}{\TMV_1}{\ZCMV'}{\TMV_1'}{\AMV} \\ From 7496f6e6dcd925cf1d03575a809bad82b4c4aede Mon Sep 17 00:00:00 2001 From: Eric Zhao <21zhaoe@protonmail.com> Date: Tue, 10 Oct 2023 01:23:19 -0400 Subject: [PATCH 13/24] formalism: Move type meet occurrences to premise in typed hazelnut model --- formalism/typed.tex | 28 ++++++++++++++++------------ 1 file changed, 16 insertions(+), 12 deletions(-) diff --git a/formalism/typed.tex b/formalism/typed.tex index 0d27e78..c1f6135 100644 --- a/formalism/typed.tex +++ b/formalism/typed.tex @@ -786,9 +786,10 @@ \subsubsection{Synthetic expression actions} \ctxSynTypeM{\ctx}{\cursorErase{\ZCMV}}{\TMV_1} \\ \ctxSynTypeM{\ctx}{\ECMV_2}{\TMV_2} \\\\ \ASEAction{\ctx}{\ZCMV}{\TMV_1}{\ZCMV'}{\TMV_1'}{\AMV} \\ - \consistent{\TMV_1'}{\TMV_2} + \consistent{\TMV_1'}{\TMV_2} \\ + \TMV' = \TMeet{\TMV_1'}{\TMV_2} }{ - \ASEAction{\ctx}{\ZCIfL{\ECMV_1}{\ZCMV}{\ECMV_2}}{\TMV}{\ZCIfL{\ECMV_1}{\ZCMV'}{\ECMV_2}}{\TMeet{\TMV_1'}{\TMV_2}}{\AMV} + \ASEAction{\ctx}{\ZCIfL{\ECMV_1}{\ZCMV}{\ECMV_2}}{\TMV}{\ZCIfL{\ECMV_1}{\ZCMV'}{\ECMV_2}}{\TMV'}{\AMV} } \inferrule[ASEZipIfL2]{ @@ -804,9 +805,10 @@ \subsubsection{Synthetic expression actions} \ctxSynTypeM{\ctx}{\ECMV_2}{\TMV_1} \\ \ctxSynTypeM{\ctx}{\cursorErase{\ZCMV}}{\TMV_2} \\\\ \ASEAction{\ctx}{\ZCMV}{\TMV_2}{\ZCMV'}{\TMV_2'}{\AMV} \\ - \consistent{\TMV_1}{\TMV_2'} + \consistent{\TMV_1}{\TMV_2'} \\ + \TMV' = \TMeet{\TMV_1}{\TMV_2'} }{ - \ASEAction{\ctx}{\ZCIfR{\ECMV_1}{\ECMV_2}{\ZCMV}}{\TMV}{\ZCIfR{\ECMV_1}{\ECMV_2}{\ZCMV'}}{\TMeet{\TMV_1}{\TMV_2'}}{\AMV} + \ASEAction{\ctx}{\ZCIfR{\ECMV_1}{\ECMV_2}{\ZCMV}}{\TMV}{\ZCIfR{\ECMV_1}{\ECMV_2}{\ZCMV'}}{\TMV'}{\AMV} } \inferrule[ASEZipIfR2]{ @@ -825,15 +827,16 @@ \subsubsection{Synthetic expression actions} } \inferrule[ASEZipInconsistentBranchesL1]{ - \ASEAction{\ctx}{\ZCMV}{\TMV_1}{\ZCMV'}{\TMV_1'}{\AMV} \\ + \ASEAction{\ctx}{\ZCMV}{\TMV_1}{\ZCMV'}{\TMV_1'}{\AMV} \\\\ \ctxSynTypeM{\ctx}{\ECMV_2}{\TMV_2} \\ - \consistent{\TMV_1'}{\TMV_2} + \consistent{\TMV_1'}{\TMV_2} \\ + \TMV' = \TMeet{\TMV_1'}{\TMV_2} }{ - \ASEAction{\ctx}{\ZCInconBrL{\ECMV_1}{\ZCMV}{\ECMV_2}}{\TMV}{\ZCIfL{\ECMV_1}{\ZCMV'}{\ECMV_2}}{\TMeet{\TMV_1'}{\TMV_2}}{\AMV} + \ASEAction{\ctx}{\ZCInconBrL{\ECMV_1}{\ZCMV}{\ECMV_2}}{\TMV}{\ZCIfL{\ECMV_1}{\ZCMV'}{\ECMV_2}}{\TMV'}{\AMV} } \inferrule[ASEZipInconsistentBranchesL2]{ - \ASEAction{\ctx}{\ZCMV}{\TMV_1}{\ZCMV'}{\TMV_1'}{\AMV} \\ + \ASEAction{\ctx}{\ZCMV}{\TMV_1}{\ZCMV'}{\TMV_1'}{\AMV} \\\\ \ctxSynTypeM{\ctx}{\ECMV_2}{\TMV_2} \\ \inconsistent{\TMV_1'}{\TMV_2} }{ @@ -841,16 +844,17 @@ \subsubsection{Synthetic expression actions} } \inferrule[ASEZipInconsistentBranchesR1]{ - \ctxSynTypeM{\ctx}{\ECMV_1}{\TMV_1} \\ + \ctxSynTypeM{\ctx}{\ECMV_1}{\TMV_1} \\\\ \ASEAction{\ctx}{\ZCMV}{\TMV_2}{\ZCMV'}{\TMV_2'}{\AMV} \\ - \consistent{\TMV_1}{\TMV_2'} + \consistent{\TMV_1}{\TMV_2'} \\ + \TMV' = \TMeet{\TMV_1}{\TMV_2'} }{ - \ASEAction{\ctx}{\ZCInconBrR{\ECMV_1}{\ECMV_2}{\ZCMV}}{\TMV}{\ZCIfL{\ECMV_1}{\ECMV_2}{\ZCMV'}}{\TMeet{\TMV_1}{\TMV_2'}}{\AMV} + \ASEAction{\ctx}{\ZCInconBrR{\ECMV_1}{\ECMV_2}{\ZCMV}}{\TMV}{\ZCIfL{\ECMV_1}{\ECMV_2}{\ZCMV'}}{\TMV'}{\AMV} } \inferrule[ASEZipInconsistentBranchesR2]{ + \ASEAction{\ctx}{\ZCMV}{\TMV_2}{\ZCMV'}{\TMV_2'}{\AMV} \\\\ \ctxSynTypeM{\ctx}{\ECMV_2}{\TMV_1} \\ - \ASEAction{\ctx}{\ZCMV}{\TMV_2}{\ZCMV'}{\TMV_2'}{\AMV} \\ \inconsistent{\TMV_1}{\TMV_2'} }{ \ASEAction{\ctx}{\ZCInconBrR{\ECMV_1}{\ECMV_2}{\ZCMV}}{\TMV}{\ZCInconBrR{\ECMV_1}{\ECMV_2}{\ZCMV'}}{\TUnknown}{\AMV} From 74dd71ec241ceb82033c007545403d0c4fd62785 Mon Sep 17 00:00:00 2001 From: Eric Zhao <21zhaoe@protonmail.com> Date: Tue, 10 Oct 2023 01:33:41 -0400 Subject: [PATCH 14/24] formalism: Fix and add remaining analytic zipper rules for typed hazelnut model --- formalism/typed.tex | 33 ++++++++++++++++++++++++++++++--- 1 file changed, 30 insertions(+), 3 deletions(-) diff --git a/formalism/typed.tex b/formalism/typed.tex index c1f6135..6a49301 100644 --- a/formalism/typed.tex +++ b/formalism/typed.tex @@ -1153,7 +1153,7 @@ \subsubsection{Analytic expression actions} \inferrule[AAEZipLetL1]{ \ctxSynTypeM{\ctx}{\cursorErase{\ZCMV}}{\TMV_1} \\ \ASEAction{\ctx}{\ZCMV}{\TMV_1}{\ZCMV'}{\TMV_1'}{\AMV} \\ - \consistent{\TMV_1}{\TMV_1'} + \equal{\TMV_1}{\TMV_1'} }{ \AAAction{\ctx}{\ZCLetL{x}{\ZCMV}{\ECMV}}{\ZCLetL{x}{\ZCMV'}{\ECMV}}{\TMV}{\AMV} } @@ -1161,14 +1161,15 @@ \subsubsection{Analytic expression actions} \inferrule[AAEZipLetL2]{ \ctxSynTypeM{\ctx}{\cursorErase{\ZCMV}}{\TMV_1} \\ \ASEAction{\ctx}{\ZCMV}{\TMV_1}{\ZCMV'}{\TMV_1'}{\AMV} \\\\ + \notEqual{\TMV_1}{\TMV_1'} \\ \ctxAnaFixedInto{\extendCtx{\ctx}{x}{\TMV_1'}}{\erase{\ECMV}}{\ECMV'}{\TMV} }{ \AAAction{\ctx}{\ZCLetL{x}{\ZCMV}{\ECMV}}{\ZCLetL{x}{\ZCMV'}{\ECMV'}}{\TMV}{\AMV} } \inferrule[AAEZipLetR]{ - \ctxSynTypeM{\ctx}{\ECMV}{\TMV'} \\ - \AAAction{\extendCtx{\ctx}{x}{\TMV'}}{\ZCMV}{\ZCMV'}{\TMV}{\AMV} + \ctxSynTypeM{\ctx}{\ECMV}{\TMV_1} \\ + \AAAction{\extendCtx{\ctx}{x}{\TMV_1}}{\ZCMV}{\ZCMV'}{\TMV}{\AMV} }{ \AAAction{\ctx}{\ZCLetR{x}{\ECMV}{\ZCMV}}{\ZCLetL{x}{\ECMV}{\ZCMV'}}{\TMV}{\AMV} } @@ -1190,6 +1191,32 @@ \subsubsection{Analytic expression actions} }{ \AAAction{\ctx}{\ZCIfR{\ECMV_1}{\ECMV_2}{\ZCMV}}{\ZCIfR{\ECMV_1}{\ECMV_2}{\ZCMV'}}{\TMV}{\AMV} } + + \inferrule[AAEZipPairL1]{ + \matchedProd{\TMV}{\TMV_1}{\TMV_2} \\ + \AAAction{\ctx}{\ZCMV}{\ZCMV'}{\TMV_1}{\AMV} + }{ + \AAAction{\ctx}{\ZCPairL{\ZCMV}{\ECMV}}{\ZCPairL{\ZCMV'}{\ECMV}}{\TMV}{\AMV} + } + + \inferrule[AAEZipPairL2]{ + \AAAction{\ctx}{\ZCMV}{\ZCMV'}{\TUnknown}{\AMV} + }{ + \AAAction{\ctx}{\ZCPairAnaNonMatchedProdL{\ZCMV}{\ECMV}}{\ZCPairAnaNonMatchedProdL{\ZCMV'}{\ECMV}}{\TMV}{\AMV} + } + + \inferrule[AAEZipPairR1]{ + \matchedProd{\TMV}{\TMV_1}{\TMV_2} \\ + \AAAction{\ctx}{\ZCMV}{\ZCMV'}{\TMV_2}{\AMV} + }{ + \AAAction{\ctx}{\ZCPairR{\ECMV}{\ZCMV}}{\ZCPairR{\ECMV}{\ZCMV'}}{\TMV}{\AMV} + } + + \inferrule[AAEZipPairR2]{ + \AAAction{\ctx}{\ZCMV}{\ZCMV'}{\TUnknown}{\AMV} + }{ + \AAAction{\ctx}{\ZCPairAnaNonMatchedProdR{\ECMV}{\ZCMV}}{\ZCPairAnaNonMatchedProdR{\ECMV}{\ZCMV'}}{\TMV}{\AMV} + } \end{mathparpagebreakable} \subsubsection{Iterated actions} From 108637ced60c1d94f8826f784d3caab1b1d85dac Mon Sep 17 00:00:00 2001 From: Eric Zhao <21zhaoe@protonmail.com> Date: Tue, 10 Oct 2023 01:38:02 -0400 Subject: [PATCH 15/24] formalism: Remove spurious free variable zmexp definition --- formalism/symbols/typed.tex | 1 - formalism/typed.tex | 9 ++------- 2 files changed, 2 insertions(+), 8 deletions(-) diff --git a/formalism/symbols/typed.tex b/formalism/symbols/typed.tex index 4893be8..cadb681 100644 --- a/formalism/symbols/typed.tex +++ b/formalism/symbols/typed.tex @@ -38,7 +38,6 @@ \newcommand{\ZCProjR}[1]{\ensuremath{\ECProjR{#1}}} % errors -\newcommand{\ZCFree}[1]{\ensuremath{\ECFree{#1}}} \newcommand{\ZCInconType}[1]{\ensuremath{\ECInconType{#1}}} \newcommand{\ZCInconBrC}[3]{\ensuremath{\ECInconBr{#1}{#2}{#3}}} \newcommand{\ZCInconBrL}[3]{\ensuremath{\ECInconBr{#1}{#2}{#3}}} diff --git a/formalism/typed.tex b/formalism/typed.tex index 6a49301..de17f96 100644 --- a/formalism/typed.tex +++ b/formalism/typed.tex @@ -26,7 +26,7 @@ \subsection{Syntax} & & \mid & \ZCPlusL{\ZCMV}{\ECMV} \mid \ZCPlusR{\ECMV}{\ZCMV} \\ & & \mid & \ZCIfC{\ZCMV}{\ECMV}{\ECMV} \mid \ZCIfL{\ECMV}{\ZCMV}{\ECMV} \mid \ZCIfR{\ECMV}{\ECMV}{\ZCMV} \\ & & \mid & \ZCPairL{\ZCMV}{\EMV} \mid \ZCPairR{\EMV}{\ZCMV} \mid \ZCProjL{\ZCMV} \mid \ZCProjR{\ZCMV} \\ - & & \mid & \ZCFree{x} \mid \ZCInconType{\ZCMV} \\ + & & \mid & \ZCInconType{\ZCMV} \\ & & \mid & \ZCLamInconAscT{x}{\ZTMV}{\ECMV} \mid \ZCLamInconAscE{x}{\TMV}{\ZCMV} \mid \ZCLamAnaNonMatchedArrowT{x}{\ZTMV}{\ECMV} \mid \ZCLamAnaNonMatchedArrowE{x}{\TMV}{\ZCMV} \mid \ZCApSynNonMatchedArrowL{\ZCMV}{\ECMV} \mid \ZCApSynNonMatchedArrowR{\ECMV}{\ZCMV} \\ @@ -44,10 +44,6 @@ \subsubsection{Well-formedness} \zWellFormed{\ZCCursor{\ECMV}} } - \inferrule[WFFree]{ }{ - \zWellFormed{\ZCFree{x}} - } - \inferrule[WFLam1]{ }{ \zWellFormed{\ZCLamT{x}{\ZTMV}{\ECMV}} } @@ -233,7 +229,6 @@ \subsubsection{Expression cursor erasure} \newcommand{\cursorErasesToRow}[2]{\ensuremath{\cursorErase{#1} & = & #2}} \[\begin{array}{rcl} \cursorErasesToRow{\ZCCursor{\ECMV}}{\ECMV} \\ - \cursorErasesToRow{\ZCFree{x}}{\cursorErase{\ECFree{x}}} \\ \cursorErasesToRow{(\ZCLamT{x}{\ZTMV}{\ECMV})}{\ECLam{x}{(\cursorErase{\ZTMV})}{\ECMV}} \\ \cursorErasesToRow{(\ZCLamE{x}{\TMV}{\ZCMV})}{\ECLam{x}{\TMV}{(\cursorErase{\ZCMV})}} \\ \cursorErasesToRow{\ZCLamAnaNonMatchedArrowT{x}{\ZTMV}{\ECMV}}{\ECLamAnaNonMatchedArrow{x}{(\cursorErase{\ZTMV})}{\ECMV}} \\ @@ -550,7 +545,7 @@ \subsubsection{Synthetic expression actions} \inferrule[ASEConFree]{ \notInCtx{\ctx}{x} }{ - \ASCon{\ctx}{\ZCCursor{\ECEHole}}{\TUnknown}{\ZCCursor{\ZCFree{x}}}{\TUnknown}{\SVar{x}} + \ASCon{\ctx}{\ZCCursor{\ECEHole}}{\TUnknown}{\ZCCursor{\ECFree{x}}}{\TUnknown}{\SVar{x}} } \inferrule[ASEConLam]{ From 0c8acbbc2c9643c807a57bf7bff4837fe57f8dad Mon Sep 17 00:00:00 2001 From: Eric Zhao <21zhaoe@protonmail.com> Date: Tue, 10 Oct 2023 01:47:58 -0400 Subject: [PATCH 16/24] formalism: Define mark erasure on zmexp -> zexp --- formalism/typed.tex | 38 ++++++++++++++++++++++++++++++++++++++ 1 file changed, 38 insertions(+) diff --git a/formalism/typed.tex b/formalism/typed.tex index de17f96..9464f1d 100644 --- a/formalism/typed.tex +++ b/formalism/typed.tex @@ -1248,6 +1248,44 @@ \subsubsection{Iterated actions} } \end{mathpar} +\subsection{Mark erasure} +\label{sec:typed-mark-erasure} +\judgbox{\ensuremath{\erase{\ZCMV}}} is a metafunction $\ZCMName \to \ZMName$ defined as follows: +% +\newcommand{\erasesToRow}[2]{\erase{#1} & = & #2} +\[\begin{array}{rcl} + \erasesToRow{\ZCCursor{\ECMV}}{\ZCCursor{\erase{\ECMV}}} \\ + \erasesToRow{(\ZCLamT{x}{\ZTMV}{\ECMV})}{\ZCLamT{x}{\ZTMV}{(\erase{\ECMV})}} \\ + \erasesToRow{(\ZCLamE{x}{\TMV}{\ZCMV})}{\ZCLamE{x}{\TMV}{(\erase{\ZCMV})}} \\ + \erasesToRow{\ZCLamAnaNonMatchedArrowT{x}{\ZTMV}{\ECMV}}{\ZCLamT{x}{\ZTMV}{(\erase{\ECMV})}} \\ + \erasesToRow{\ZCLamAnaNonMatchedArrowE{x}{\TMV}{\ZCMV}}{\ZCLamE{x}{\TMV}{(\erase{\ZCMV})}} \\ + \erasesToRow{\ZCLamInconAscT{x}{\ZTMV}{\ECMV}}{\ZCLamT{x}{\ZTMV}{(\erase{\ECMV})}} \\ + \erasesToRow{\ZCLamInconAscE{x}{\TMV}{\ZCMV}}{\ZCLamE{x}{\TMV}{(\erase{\ZCMV})}} \\ + \erasesToRow{(\ZCApL{\ZCMV}{\ECMV})}{\ZCApL{(\erase{\ZCMV})}{(\erase{\ZCMV})}} \\ + \erasesToRow{(\ZCApR{\ECMV}{\ZCMV})}{\ZCApR{(\erase{\ECMV})}{(\erase{\ZCMV})}} \\ + \erasesToRow{(\ZCApSynNonMatchedArrowL{\ZCMV}{\ECMV})}{\ZCApL{\erase{\ZCMV}}{(\erase{\ECMV})}} \\ + \erasesToRow{(\ZCApSynNonMatchedArrowR{\ECMV}{\ZCMV})}{\ZCApR{\erase{\ECMV}}{(\erase{\ZCMV})}} \\ + \erasesToRow{(\ZCLetL{x}{\ZCMV}{\ECMV})}{\ZCLetL{x}{(\erase{\ZCMV})}{(\erase{\ECMV})}} \\ + \erasesToRow{(\ZCLetR{x}{\ECMV}{\ZCMV})}{\ZCLetR{x}{(\erase{\ECMV})}{(\erase{\ZCMV})}} \\ + \erasesToRow{(\ZCPlusL{\ZCMV}{\ECMV})}{\ZCPlusL{(\erase{\ZCMV})}{(\erase{\ECMV})}} \\ + \erasesToRow{(\ZCPlusR{\ECMV}{\ZCMV})}{\ZCPlusR{(\erase{\ECMV})}{(\erase{\ZCMV})}} \\ + \erasesToRow{(\ZCIfC{\ZCMV}{\ECMV_1}{\ECMV_2})}{\ZCIfC{(\erase{\ZCMV})}{(\erase{\ECMV_1})}{(\erase{\ECMV_2})}} \\ + \erasesToRow{(\ZCIfL{\ECMV_1}{\ZCMV}{\ECMV_2})}{\ZCIfL{(\erase{\ECMV_1})}{(\erase{\ZCMV})}{(\erase{\ECMV_2})}} \\ + \erasesToRow{(\ZCIfL{\ECMV_1}{\ECMV_2}{\ZCMV})}{\ZCIfR{(\erase{\ECMV_1})}{(\erase{\ECMV_2})}{(\erase{\ZCMV})}} \\ + \erasesToRow{\ZCInconBrC{\ZCMV}{\ECMV_1}{\ECMV_2}}{\ZCIfC{(\erase{\ZCMV})}{(\erase{\ECMV_1})}{(\erase{\ECMV_2})}} \\ + \erasesToRow{\ZCInconBrL{\ECMV_1}{\ZCMV}{\ECMV_2}}{\ZCIfL{(\erase{\ECMV_1})}{(\erase{\ZCMV})}{(\erase{\ECMV_2})}} \\ + \erasesToRow{\ZCInconBrR{\ECMV_1}{\ECMV_2}{\ZCMV}}{\ZCIfR{(\erase{\ECMV_1})}{(\erase{\ECMV_2})}{(\erase{\ZCMV})}} \\ + \erasesToRow{\ZCPairL{\ZCMV}{\ECMV}}{\ZCPairL{\erase{\ZCMV}}{\erase{\ECMV}}} \\ + \erasesToRow{\ZCPairR{\ECMV}{\ZCMV}}{\ZCPairR{\erase{\ECMV}}{\erase{\ZCMV}}} \\ + \erasesToRow{\ZCPairAnaNonMatchedProdL{\ZCMV}{\ECMV}}{\ZCPairL{\erase{\ZCMV}}{\erase{\ECMV}}} \\ + \erasesToRow{\ZCPairAnaNonMatchedProdR{\ECMV}{\ZCMV}}{\ZCPairR{\erase{\ECMV}}{\erase{\ZCMV}}} \\ + \erasesToRow{(\ZCProjL{\ZCMV})}{\ZCProjL{(\erase{\ZCMV})}} \\ + \erasesToRow{(\ZCProjLSynNonMatchedProd{\ZCMV})}{\ZCProjL{\erase{\ZCMV}}} \\ + \erasesToRow{(\ZCProjR{\ZCMV})}{\ZCProjR{(\erase{\ZCMV})}} \\ + \erasesToRow{(\ZCProjRSynNonMatchedProd{\ZCMV})}{\ZCProjR{\erase{\ZCMV}}} \\ + \erasesToRow{\ZCInconType{\ZCMV}}{\erase{\ZCMV}} \\ +\end{array}\] + \subsection{Metatheorems} \label{sec:typed-metatheorems} \begin{theorem}[name=Sensibility] \ From 698915b6726b85ec910c5e3fc6b34faf2c95d059 Mon Sep 17 00:00:00 2001 From: Eric Zhao <21zhaoe@protonmail.com> Date: Tue, 10 Oct 2023 02:02:40 -0400 Subject: [PATCH 17/24] formalism: Indicate domain/codomain for metafunctions --- formalism/typed.tex | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/formalism/typed.tex b/formalism/typed.tex index 9464f1d..b331534 100644 --- a/formalism/typed.tex +++ b/formalism/typed.tex @@ -224,7 +224,7 @@ \subsubsection{Type cursor erasure} \subsubsection{Expression cursor erasure} \label{sec:typed-expression-cursor-erasure} -\judgbox{\ensuremath{\cursorErase{\ZCMV}}} is a metafunction defined as follows: +\judgbox{\ensuremath{\cursorErase{\ZCMV}}} is a metafunction $\ZCMName \to \ECMName$ defined as follows: % \newcommand{\cursorErasesToRow}[2]{\ensuremath{\cursorErase{#1} & = & #2}} \[\begin{array}{rcl} From 9518f095708db7e00967729b3e77b000b4b409ae Mon Sep 17 00:00:00 2001 From: Eric Zhao <21zhaoe@protonmail.com> Date: Tue, 10 Oct 2023 02:24:01 -0400 Subject: [PATCH 18/24] formalism: Add quiver package --- formalism/preamble/preamble.tex | 3 +++ formalism/quiver.sty | 40 +++++++++++++++++++++++++++++++++ 2 files changed, 43 insertions(+) create mode 100644 formalism/quiver.sty diff --git a/formalism/preamble/preamble.tex b/formalism/preamble/preamble.tex index 9420c87..e757a82 100644 --- a/formalism/preamble/preamble.tex +++ b/formalism/preamble/preamble.tex @@ -48,6 +48,9 @@ \usepackage[dvipsnames]{xcolor} \usepackage[most]{tcolorbox} +% diagrams +\usepackage{quiver} + % theorem types \declaretheorem[name=Theorem, parent=section]{theorem} \declaretheorem[name=Lemma, parent=theorem]{lemma} diff --git a/formalism/quiver.sty b/formalism/quiver.sty new file mode 100644 index 0000000..d1d7d07 --- /dev/null +++ b/formalism/quiver.sty @@ -0,0 +1,40 @@ +% *** quiver *** +% A package for drawing commutative diagrams exported from https://q.uiver.app. +% +% This package is currently a wrapper around the `tikz-cd` package, importing necessary TikZ +% libraries, and defining a new TikZ style for curves of a fixed height. +% +% Version: 1.3.0 +% Authors: +% - varkor (https://github.com/varkor) +% - AndréC (https://tex.stackexchange.com/users/138900/andr%C3%A9c) + +\NeedsTeXFormat{LaTeX2e} +\ProvidesPackage{quiver}[2021/01/11 quiver] + +% `tikz-cd` is necessary to draw commutative diagrams. +\RequirePackage{tikz-cd} +% `amssymb` is necessary for `\lrcorner` and `\ulcorner`. +\RequirePackage{amssymb} +% `calc` is necessary to draw curved arrows. +\usetikzlibrary{calc} +% `pathmorphing` is necessary to draw squiggly arrows. +\usetikzlibrary{decorations.pathmorphing} + +% A TikZ style for curved arrows of a fixed height, due to AndréC. +\tikzset{curve/.style={settings={#1},to path={(\tikztostart) + .. controls ($(\tikztostart)!\pv{pos}!(\tikztotarget)!\pv{height}!270:(\tikztotarget)$) + and ($(\tikztostart)!1-\pv{pos}!(\tikztotarget)!\pv{height}!270:(\tikztotarget)$) + .. (\tikztotarget)\tikztonodes}}, + settings/.code={\tikzset{quiver/.cd,#1} + \def\pv##1{\pgfkeysvalueof{/tikz/quiver/##1}}}, + quiver/.cd,pos/.initial=0.35,height/.initial=0} + +% TikZ arrowhead/tail styles. +\tikzset{tail reversed/.code={\pgfsetarrowsstart{tikzcd to}}} +\tikzset{2tail/.code={\pgfsetarrowsstart{Implies[reversed]}}} +\tikzset{2tail reversed/.code={\pgfsetarrowsstart{Implies}}} +% TikZ arrow styles. +\tikzset{no body/.style={/tikz/dash pattern=on 0 off 1mm}} + +\endinput From b315dff669089cae07384ad60dabb4b4d2ab6541 Mon Sep 17 00:00:00 2001 From: Eric Zhao <21zhaoe@protonmail.com> Date: Tue, 10 Oct 2023 02:24:11 -0400 Subject: [PATCH 19/24] formalism: Define erasure commutativity theorem --- formalism/typed.tex | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/formalism/typed.tex b/formalism/typed.tex index b331534..bc1f869 100644 --- a/formalism/typed.tex +++ b/formalism/typed.tex @@ -1288,6 +1288,19 @@ \subsection{Mark erasure} \subsection{Metatheorems} \label{sec:typed-metatheorems} +\begin{theorem}[name=Erasure Commutativity] + For all $\ZCMV$, $\cursorErase{(\erase{\ZCMV})} = \erase{(\cursorErase{\ZCMV})}$. + % + \[\begin{tikzcd} + \ZCMV \mathsmaller{~\in~ \ZCMName} && \ZMV \mathsmaller{~\in~ \ZMName} \\\\ + \ECMV \mathsmaller{~\in~ \ECMName} && \EMV \mathsmaller{~\in~ \EMName} + \arrow["{\cursorErase{\_}}"', from=1-1, to=3-1] + \arrow["{\erase{\_}}", from=1-1, to=1-3] + \arrow["{\cursorErase{\_}}", from=1-3, to=3-3] + \arrow["{\erase{\_}}"', from=3-1, to=3-3] + \end{tikzcd}\] +\end{theorem} + \begin{theorem}[name=Sensibility] \ \begin{enumerate} \item If $\zWellFormed{\ZCMV}$ and $\ctxSynTypeM{\ctx}{\cursorErase{\ZCMV}}{\TMV}$ and From 712ed56a57416f226af531f812c50e3d4f8c9e2a Mon Sep 17 00:00:00 2001 From: Eric Zhao <21zhaoe@protonmail.com> Date: Tue, 10 Oct 2023 02:28:00 -0400 Subject: [PATCH 20/24] formalism: Fix marked analysis judgment in typed hazelnut metatheorem statements --- formalism/typed.tex | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/formalism/typed.tex b/formalism/typed.tex index bc1f869..7a87922 100644 --- a/formalism/typed.tex +++ b/formalism/typed.tex @@ -1307,7 +1307,7 @@ \subsection{Metatheorems} $\ASEAction{\ctx}{\ZCMV}{\TMV}{\ZCMV'}{\TMV'}{\AMV}$, then $\zWellFormed{\ZCMV'}$ and $\ctxSynTypeM{\ctx}{\cursorErase{\ZCMV'}}{\TMV'}$. - \item If $\zWellFormed{\ZCMV}$ and $\ctxAnaType{\ctx}{\cursorErase{\ZCMV}}{\TMV}$ and + \item If $\zWellFormed{\ZCMV}$ and $\ctxAnaTypeM{\ctx}{\cursorErase{\ZCMV}}{\TMV}$ and $\AAEAction{\ctx}{\ZCMV}{\ZCMV'}{\TMV}{\AMV}$, then $\zWellFormed{\ZCMV'}$ and $\ctxAnaType{\ctx}{\cursorErase{\ZCMV'}}{\TMV}$. \end{enumerate} @@ -1322,7 +1322,7 @@ \subsection{Metatheorems} $\ASEAction{\ctx}{\ZCMV}{\TMV}{\ZCMV'}{\TMV'}{\AMove{\MMV}}$, then $\zWellFormed{\ZCMV'}$ and $\cursorErase{\ZCMV} = \cursorErase{\ZCMV'}$ and $\equal{\TMV}{\TMV'}$. - \item If $\zWellFormed{\ZCMV}$ and $\ctxAnaType{\ctx}{\cursorErase{\ZCMV}}{\TMV}$ and + \item If $\zWellFormed{\ZCMV}$ and $\ctxAnaTypeM{\ctx}{\cursorErase{\ZCMV}}{\TMV}$ and $\AAEAction{\ctx}{\ZCMV}{\ZCMV'}{\TMV}{\AMove{\MMV}}$, then $\zWellFormed{\ZCMV'}$ and $\cursorErase{\ZCMV} = \cursorErase{\ZCMV'}$. \end{enumerate} @@ -1339,7 +1339,7 @@ \subsection{Metatheorems} $\ASEActionIter{\ctx}{\ZCMV}{\TMV}{\ZCMV'}{\TMV}{\AIMV}$. \item If $\zWellFormed{\ZCMV}$ and $\zWellFormed{\ZCMV'}$ and - $\ctxAnaType{\ctx}{\cursorErase{\ZCMV}}{\TMV}$ and $\cursorErase{\ZCMV} = \cursorErase{\ZCMV'}$, + $\ctxAnaTypeM{\ctx}{\cursorErase{\ZCMV}}{\TMV}$ and $\cursorErase{\ZCMV} = \cursorErase{\ZCMV'}$, then there exists $\AIMV$ such that $\movements{\AIMV}$ and $\AAEActionIter{\ctx}{\ZCMV}{\ZCMV'}{\TMV}{\AIMV}$. \end{enumerate} @@ -1354,7 +1354,7 @@ \subsection{Metatheorems} $\cursorErase{\ZCMV} = \ECMV$, then there exists $\AIMV$ such that $\movements{\AIMV}$ and $\ASEActionIter{\ctx}{\ZCMV}{\TMV}{\ZCCursor{\ECMV}}{\TMV}{\AIMV}$. - \item If $\zWellFormed{\ZCMV}$ and $\ctxAnaType{\ctx}{\cursorErase{\ZCMV}}{\TMV}$ and + \item If $\zWellFormed{\ZCMV}$ and $\ctxAnaTypeM{\ctx}{\cursorErase{\ZCMV}}{\TMV}$ and $\cursorErase{\ZCMV} = \ECMV$, then there exists $\AIMV$ such that $\movements{\AIMV}$ and $\AAEActionIter{\ctx}{\ZCMV}{\ZCCursor{\ECMV}}{\TMV}{\AIMV}$. \end{enumerate} @@ -1369,7 +1369,7 @@ \subsection{Metatheorems} $\cursorErase{\ZCMV} = \ECMV$, then there exists $\AIMV$ such that $\movements{\AIMV}$ and $\ASEActionIter{\ctx}{\ZCCursor{\ECMV}}{\TMV}{\ZCMV}{\TMV}{\AIMV}$. - \item If $\zWellFormed{\ZCMV}$ and $\ctxAnaType{\ctx}{\cursorErase{\ZCMV}}{\TMV}$ and + \item If $\zWellFormed{\ZCMV}$ and $\ctxAnaTypeM{\ctx}{\cursorErase{\ZCMV}}{\TMV}$ and $\cursorErase{\ZCMV} = \ECMV$, then there exists $\AIMV$ such that $\movements{\AIMV}$ and $\AAEActionIter{\ctx}{\ZCCursor{\ECMV}}{\ZCMV}{\TMV}{\AIMV}$. \end{enumerate} @@ -1383,7 +1383,7 @@ \subsection{Metatheorems} \item If $\ctxSynTypeM{\ctx}{\ECMV}{\TMV}$, then there exists $\AIMV$ such that $\ASEActionIter{\ctx}{\ZCCursor{\EEHole}}{\TUnknown}{\ZCCursor{\ECMV}}{\TMV}{\AIMV}$. - \item If $\ctxAnaType{\ctx}{\ECMV}{\TMV}$, then there exists $\AIMV$ such that + \item If $\ctxAnaTypeM{\ctx}{\ECMV}{\TMV}$, then there exists $\AIMV$ such that $\AAEActionIter{\ctx}{\ZCCursor{\EEHole}}{\ZCCursor{\ECMV}}{\TMV}{\AIMV}$. \end{enumerate} \end{theorem} @@ -1398,7 +1398,7 @@ \subsection{Metatheorems} $\ASEActionIter{\ctx}{\ZCMV}{\TMV}{\ZCMV''}{\TMV''}{\AMV}$, then $\ZCMV' = \ZCMV''$ and $\equal{\TMV'}{\TMV''}$. - \item If $\zWellFormed{\ZCMV}$ and $\ctxAnaType{\ctx}{\cursorErase{\ZCMV}}{\TMV}$ and + \item If $\zWellFormed{\ZCMV}$ and $\ctxAnaTypeM{\ctx}{\cursorErase{\ZCMV}}{\TMV}$ and $\AAEActionIter{\ctx}{\ZCMV}{\ZCMV'}{\TMV}{\AMV}$ and $\AAEActionIter{\ctx}{\ZCMV}{\ZCMV''}{\TMV}{\AMV}$, then $\ZCMV' = \ZCMV''$. \end{enumerate} From 69c917e92311203e56e6f2745f2f20bd97f03282 Mon Sep 17 00:00:00 2001 From: Eric Zhao <21zhaoe@protonmail.com> Date: Tue, 10 Oct 2023 02:31:41 -0400 Subject: [PATCH 21/24] formalism: Give correctness metatheorem for typed hazelnut in relation to untyped --- formalism/typed.tex | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/formalism/typed.tex b/formalism/typed.tex index 7a87922..7237066 100644 --- a/formalism/typed.tex +++ b/formalism/typed.tex @@ -1301,6 +1301,18 @@ \subsection{Metatheorems} \end{tikzcd}\] \end{theorem} +\begin{theorem}[name=Correctness] \ + \begin{enumerate} + \item If $\zWellFormed{\ZCMV}$ and $\ctxSynTypeM{\ctx}{\cursorErase{\ZCMV}}{\TMV}$ and + $\ASEAction{\ctx}{\ZCMV}{\TMV}{\ZCMV'}{\TMV'}{\AMV}$ and + $\AUEAction{\erase{\ZCMV}}{\ZMV'}{\AMV}$, then $\equal{\erase{\ZCMV'}}{\ZMV'}$. + + \item If $\zWellFormed{\ZCMV}$ and $\ctxAnaTypeM{\ctx}{\cursorErase{\ZCMV}}{\TMV}$ and + $\AAEAction{\ctx}{\ZCMV}{\ZCMV'}{\TMV}{\AMV}$ and + $\AUEAction{\erase{\ZCMV}}{\ZMV'}{\AMV}$, then $\equal{\erase{\ZCMV'}}{\ZMV'}$. + \end{enumerate} +\end{theorem} + \begin{theorem}[name=Sensibility] \ \begin{enumerate} \item If $\zWellFormed{\ZCMV}$ and $\ctxSynTypeM{\ctx}{\cursorErase{\ZCMV}}{\TMV}$ and From 51d99b7e3c4c395bda32bd02c7b5e963f8085734 Mon Sep 17 00:00:00 2001 From: Eric Zhao <21zhaoe@protonmail.com> Date: Tue, 10 Oct 2023 02:38:28 -0400 Subject: [PATCH 22/24] formalism: Clean up formatting of metatheorem section for typed hazelnut --- formalism/typed.tex | 176 +++++++++++++++++++++++++++----------------- 1 file changed, 109 insertions(+), 67 deletions(-) diff --git a/formalism/typed.tex b/formalism/typed.tex index 7237066..eadad7d 100644 --- a/formalism/typed.tex +++ b/formalism/typed.tex @@ -1303,87 +1303,124 @@ \subsection{Metatheorems} \begin{theorem}[name=Correctness] \ \begin{enumerate} - \item If $\zWellFormed{\ZCMV}$ and $\ctxSynTypeM{\ctx}{\cursorErase{\ZCMV}}{\TMV}$ and - $\ASEAction{\ctx}{\ZCMV}{\TMV}{\ZCMV'}{\TMV'}{\AMV}$ and - $\AUEAction{\erase{\ZCMV}}{\ZMV'}{\AMV}$, then $\equal{\erase{\ZCMV'}}{\ZMV'}$. - - \item If $\zWellFormed{\ZCMV}$ and $\ctxAnaTypeM{\ctx}{\cursorErase{\ZCMV}}{\TMV}$ and - $\AAEAction{\ctx}{\ZCMV}{\ZCMV'}{\TMV}{\AMV}$ and - $\AUEAction{\erase{\ZCMV}}{\ZMV'}{\AMV}$, then $\equal{\erase{\ZCMV'}}{\ZMV'}$. + \item If $\zWellFormed{\ZCMV}$ + and $\ctxSynTypeM{\ctx}{\cursorErase{\ZCMV}}{\TMV}$ + and $\ASEAction{\ctx}{\ZCMV}{\TMV}{\ZCMV'}{\TMV'}{\AMV}$ + and $\AUEAction{\erase{\ZCMV}}{\ZMV'}{\AMV}$, + then $\equal{\erase{\ZCMV'}}{\ZMV'}$. + + \item If $\zWellFormed{\ZCMV}$ + and $\ctxAnaTypeM{\ctx}{\cursorErase{\ZCMV}}{\TMV}$ + and $\AAEAction{\ctx}{\ZCMV}{\ZCMV'}{\TMV}{\AMV}$ + and $\AUEAction{\erase{\ZCMV}}{\ZMV'}{\AMV}$, + then $\equal{\erase{\ZCMV'}}{\ZMV'}$. \end{enumerate} \end{theorem} \begin{theorem}[name=Sensibility] \ \begin{enumerate} - \item If $\zWellFormed{\ZCMV}$ and $\ctxSynTypeM{\ctx}{\cursorErase{\ZCMV}}{\TMV}$ and - $\ASEAction{\ctx}{\ZCMV}{\TMV}{\ZCMV'}{\TMV'}{\AMV}$, then $\zWellFormed{\ZCMV'}$ and - $\ctxSynTypeM{\ctx}{\cursorErase{\ZCMV'}}{\TMV'}$. - - \item If $\zWellFormed{\ZCMV}$ and $\ctxAnaTypeM{\ctx}{\cursorErase{\ZCMV}}{\TMV}$ and - $\AAEAction{\ctx}{\ZCMV}{\ZCMV'}{\TMV}{\AMV}$, then $\zWellFormed{\ZCMV'}$ and - $\ctxAnaType{\ctx}{\cursorErase{\ZCMV'}}{\TMV}$. + \item If $\zWellFormed{\ZCMV}$ + and $\ctxSynTypeM{\ctx}{\cursorErase{\ZCMV}}{\TMV}$ + and $\ASEAction{\ctx}{\ZCMV}{\TMV}{\ZCMV'}{\TMV'}{\AMV}$, + then $\zWellFormed{\ZCMV'}$ + and $\ctxSynTypeM{\ctx}{\cursorErase{\ZCMV'}}{\TMV'}$. + + \item If $\zWellFormed{\ZCMV}$ + and $\ctxAnaTypeM{\ctx}{\cursorErase{\ZCMV}}{\TMV}$ + and $\AAEAction{\ctx}{\ZCMV}{\ZCMV'}{\TMV}{\AMV}$, + then $\zWellFormed{\ZCMV'}$ + and $\ctxAnaType{\ctx}{\cursorErase{\ZCMV'}}{\TMV}$. \end{enumerate} \end{theorem} \begin{theorem}[name=Movement Erasure Invariance] \ \begin{enumerate} - \item If $\AUTAction{\ZTMV}{\ZTMV'}{\AMove{\MMV}}$, then $\cursorErase{\ZTMV} = - \cursorErase{\ZTMV'}$. - - \item If $\zWellFormed{\ZCMV}$ and $\ctxSynTypeM{\ctx}{\cursorErase{\ZCMV}}{\TMV}$ and - $\ASEAction{\ctx}{\ZCMV}{\TMV}{\ZCMV'}{\TMV'}{\AMove{\MMV}}$, then $\zWellFormed{\ZCMV'}$ and - $\cursorErase{\ZCMV} = \cursorErase{\ZCMV'}$ and $\equal{\TMV}{\TMV'}$. - - \item If $\zWellFormed{\ZCMV}$ and $\ctxAnaTypeM{\ctx}{\cursorErase{\ZCMV}}{\TMV}$ and - $\AAEAction{\ctx}{\ZCMV}{\ZCMV'}{\TMV}{\AMove{\MMV}}$, then $\zWellFormed{\ZCMV'}$ and - $\cursorErase{\ZCMV} = \cursorErase{\ZCMV'}$. + \item If $\AUTAction{\ZTMV}{\ZTMV'}{\AMove{\MMV}}$, + then $\cursorErase{\ZTMV} = \cursorErase{\ZTMV'}$. + + \item If $\zWellFormed{\ZCMV}$ + and $\ctxSynTypeM{\ctx}{\cursorErase{\ZCMV}}{\TMV}$ + and $\ASEAction{\ctx}{\ZCMV}{\TMV}{\ZCMV'}{\TMV'}{\AMove{\MMV}}$, + then $\zWellFormed{\ZCMV'}$ + and $\cursorErase{\ZCMV} = \cursorErase{\ZCMV'}$ + and $\equal{\TMV}{\TMV'}$. + + \item If $\zWellFormed{\ZCMV}$ + and $\ctxAnaTypeM{\ctx}{\cursorErase{\ZCMV}}{\TMV}$ + and $\AAEAction{\ctx}{\ZCMV}{\ZCMV'}{\TMV}{\AMove{\MMV}}$, + then $\zWellFormed{\ZCMV'}$ + and $\cursorErase{\ZCMV} = \cursorErase{\ZCMV'}$. \end{enumerate} \end{theorem} \begin{theorem}[name=Reachability] \ \begin{enumerate} - \item If $\cursorErase{\ZTMV} = \cursorErase{\ZTMV'}$, then there exists $\AIMV$ such that - $\movements{\AIMV}$ and $\AUTActionIter{\ZTMV}{\ZTMV'}{\AIMV}$. - - \item If $\zWellFormed{\ZCMV}$ and $\zWellFormed{\ZCMV'}$ and - $\ctxSynTypeM{\ctx}{\cursorErase{\ZCMV}}{\TMV}$ and $\cursorErase{\ZCMV} = \cursorErase{\ZCMV'}$, - then there exists $\AIMV$ such that $\movements{\AIMV}$ and - $\ASEActionIter{\ctx}{\ZCMV}{\TMV}{\ZCMV'}{\TMV}{\AIMV}$. - - \item If $\zWellFormed{\ZCMV}$ and $\zWellFormed{\ZCMV'}$ and - $\ctxAnaTypeM{\ctx}{\cursorErase{\ZCMV}}{\TMV}$ and $\cursorErase{\ZCMV} = \cursorErase{\ZCMV'}$, - then there exists $\AIMV$ such that $\movements{\AIMV}$ and - $\AAEActionIter{\ctx}{\ZCMV}{\ZCMV'}{\TMV}{\AIMV}$. + \item If $\cursorErase{\ZTMV} = \cursorErase{\ZTMV'}$, + then there exists $\AIMV$ + such that $\movements{\AIMV}$ + and $\AUTActionIter{\ZTMV}{\ZTMV'}{\AIMV}$. + + \item If $\zWellFormed{\ZCMV}$ + and $\zWellFormed{\ZCMV'}$ + and $\ctxSynTypeM{\ctx}{\cursorErase{\ZCMV}}{\TMV}$ + and $\cursorErase{\ZCMV} = \cursorErase{\ZCMV'}$, + then there exists $\AIMV$ + such that $\movements{\AIMV}$ + and $\ASEActionIter{\ctx}{\ZCMV}{\TMV}{\ZCMV'}{\TMV}{\AIMV}$. + + \item If $\zWellFormed{\ZCMV}$ + and $\zWellFormed{\ZCMV'}$ + and $\ctxAnaTypeM{\ctx}{\cursorErase{\ZCMV}}{\TMV}$ + and $\cursorErase{\ZCMV} = \cursorErase{\ZCMV'}$, + then there exists $\AIMV$ + such that $\movements{\AIMV}$ + and $\AAEActionIter{\ctx}{\ZCMV}{\ZCMV'}{\TMV}{\AIMV}$. \end{enumerate} \end{theorem} \begin{lemma}[name=Reach Up] \ \begin{enumerate} - \item If $\cursorErase{\ZTMV} = \TMV$, then there exists $\AIMV$ such that $\movements{\AIMV}$ - and $\AUTActionIter{\ZTMV}{\ZTCursor{\TMV}}{\AIMV}$. - - \item If $\zWellFormed{\ZCMV}$ and $\ctxSynTypeM{\ctx}{\cursorErase{\ZCMV}}{\TMV}$ and - $\cursorErase{\ZCMV} = \ECMV$, then there exists $\AIMV$ such that $\movements{\AIMV}$ and - $\ASEActionIter{\ctx}{\ZCMV}{\TMV}{\ZCCursor{\ECMV}}{\TMV}{\AIMV}$. - - \item If $\zWellFormed{\ZCMV}$ and $\ctxAnaTypeM{\ctx}{\cursorErase{\ZCMV}}{\TMV}$ and - $\cursorErase{\ZCMV} = \ECMV$, then there exists $\AIMV$ such that $\movements{\AIMV}$ and - $\AAEActionIter{\ctx}{\ZCMV}{\ZCCursor{\ECMV}}{\TMV}{\AIMV}$. + \item If $\cursorErase{\ZTMV} = \TMV$, + then there exists $\AIMV$ + such that $\movements{\AIMV}$ + and $\AUTActionIter{\ZTMV}{\ZTCursor{\TMV}}{\AIMV}$. + + \item If $\zWellFormed{\ZCMV}$ + and $\ctxSynTypeM{\ctx}{\cursorErase{\ZCMV}}{\TMV}$ + and $\cursorErase{\ZCMV} = \ECMV$, + then there exists $\AIMV$ + such that $\movements{\AIMV}$ + and $\ASEActionIter{\ctx}{\ZCMV}{\TMV}{\ZCCursor{\ECMV}}{\TMV}{\AIMV}$. + + \item If $\zWellFormed{\ZCMV}$ + and $\ctxAnaTypeM{\ctx}{\cursorErase{\ZCMV}}{\TMV}$ + and $\cursorErase{\ZCMV} = \ECMV$, + then there exists $\AIMV$ + such that $\movements{\AIMV}$ + and $\AAEActionIter{\ctx}{\ZCMV}{\ZCCursor{\ECMV}}{\TMV}{\AIMV}$. \end{enumerate} \end{lemma} \begin{lemma}[name=Reach Down] \ \begin{enumerate} - \item If $\cursorErase{\ZTMV} = \TMV$, then there exists $\AIMV$ such that $\movements{\AIMV}$ - and $\AUTActionIter{\ZTCursor{\TMV}}{\ZTMV}{\AIMV}$. - - \item If $\zWellFormed{\ZCMV}$ and $\ctxSynTypeM{\ctx}{\cursorErase{\ZCMV}}{\TMV}$ and - $\cursorErase{\ZCMV} = \ECMV$, then there exists $\AIMV$ such that $\movements{\AIMV}$ and - $\ASEActionIter{\ctx}{\ZCCursor{\ECMV}}{\TMV}{\ZCMV}{\TMV}{\AIMV}$. - - \item If $\zWellFormed{\ZCMV}$ and $\ctxAnaTypeM{\ctx}{\cursorErase{\ZCMV}}{\TMV}$ and - $\cursorErase{\ZCMV} = \ECMV$, then there exists $\AIMV$ such that $\movements{\AIMV}$ and - $\AAEActionIter{\ctx}{\ZCCursor{\ECMV}}{\ZCMV}{\TMV}{\AIMV}$. + \item If $\cursorErase{\ZTMV} = \TMV$, + then there exists $\AIMV$ + such that $\movements{\AIMV}$ + and $\AUTActionIter{\ZTCursor{\TMV}}{\ZTMV}{\AIMV}$. + + \item If $\zWellFormed{\ZCMV}$ + and $\ctxSynTypeM{\ctx}{\cursorErase{\ZCMV}}{\TMV}$ + and $\cursorErase{\ZCMV} = \ECMV$, + then there exists $\AIMV$ + such that $\movements{\AIMV}$ + and $\ASEActionIter{\ctx}{\ZCCursor{\ECMV}}{\TMV}{\ZCMV}{\TMV}{\AIMV}$. + + \item If $\zWellFormed{\ZCMV}$ + and $\ctxAnaTypeM{\ctx}{\cursorErase{\ZCMV}}{\TMV}$ + and $\cursorErase{\ZCMV} = \ECMV$, + then there exists $\AIMV$ + such that $\movements{\AIMV}$ + and $\AAEActionIter{\ctx}{\ZCCursor{\ECMV}}{\ZCMV}{\TMV}{\AIMV}$. \end{enumerate} \end{lemma} @@ -1402,17 +1439,22 @@ \subsection{Metatheorems} \begin{theorem}[name=Determinism] \ \begin{enumerate} - \item If $\AUTActionIter{\ZTMV}{\ZTMV'}{\AMV}$ and $\AUTActionIter{\ZTMV}{\ZTMV''}{\AMV}$, then - $\ZTMV' = \ZTMV''$. - - \item If $\zWellFormed{\ZCMV}$ and $\ctxSynTypeM{\ctx}{\cursorErase{\ZCMV}}{\TMV}$ and - $\ASEActionIter{\ctx}{\ZCMV}{\TMV}{\ZCMV'}{\TMV'}{\AMV}$ and - $\ASEActionIter{\ctx}{\ZCMV}{\TMV}{\ZCMV''}{\TMV''}{\AMV}$, then $\ZCMV' = \ZCMV''$ and - $\equal{\TMV'}{\TMV''}$. - - \item If $\zWellFormed{\ZCMV}$ and $\ctxAnaTypeM{\ctx}{\cursorErase{\ZCMV}}{\TMV}$ and - $\AAEActionIter{\ctx}{\ZCMV}{\ZCMV'}{\TMV}{\AMV}$ and - $\AAEActionIter{\ctx}{\ZCMV}{\ZCMV''}{\TMV}{\AMV}$, then $\ZCMV' = \ZCMV''$. + \item If $\AUTActionIter{\ZTMV}{\ZTMV'}{\AMV}$ + and $\AUTActionIter{\ZTMV}{\ZTMV''}{\AMV}$ + then $\ZTMV' = \ZTMV''$. + + \item If $\zWellFormed{\ZCMV}$ + and $\ctxSynTypeM{\ctx}{\cursorErase{\ZCMV}}{\TMV}$ + and $\ASEActionIter{\ctx}{\ZCMV}{\TMV}{\ZCMV'}{\TMV'}{\AMV}$ + and $\ASEActionIter{\ctx}{\ZCMV}{\TMV}{\ZCMV''}{\TMV''}{\AMV}$, + then $\ZCMV' = \ZCMV''$ + and $\equal{\TMV'}{\TMV''}$. + + \item If $\zWellFormed{\ZCMV}$ + and $\ctxAnaTypeM{\ctx}{\cursorErase{\ZCMV}}{\TMV}$ + and $\AAEActionIter{\ctx}{\ZCMV}{\ZCMV'}{\TMV}{\AMV}$ + and $\AAEActionIter{\ctx}{\ZCMV}{\ZCMV''}{\TMV}{\AMV}$, + then $\ZCMV' = \ZCMV''$. \end{enumerate} \end{theorem} From d2b9018880c25fe3714632c3b7777fdb5a33f06a Mon Sep 17 00:00:00 2001 From: Eric Zhao <21zhaoe@protonmail.com> Date: Sun, 8 Oct 2023 19:36:25 -0400 Subject: [PATCH 23/24] formalism: Add missing marked zexp well-formedness rules --- formalism/typed.tex | 75 +++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 75 insertions(+) diff --git a/formalism/typed.tex b/formalism/typed.tex index eadad7d..f430594 100644 --- a/formalism/typed.tex +++ b/formalism/typed.tex @@ -213,6 +213,81 @@ \subsubsection{Well-formedness} }{ \zWellFormed{\ZCInconType{\ZCMV}} } + + \inferrule[WFLam3]{ }{ + \zWellFormed{\ZLamInconAscT{x}{\ZTMV}{\ECMV}} + } + + \inferrule[WFLam4]{ + \zWellFormed{\ZMV} + }{ + \zWellFormed{\ZLamInconAscE{x}{\TMV}{\ZMV}} + } + + \inferrule[WFLam5]{ + }{ + \zWellFormed{\ZLamAnaNonMatchedArrowT{x}{\ZTMV}{\ECMV}} + } + + \inferrule[WFLam6]{ + \zWellFormed{\ZMV} + }{ + \zWellFormed{\ZLamAnaNonMatchedArrowE{x}{\TMV}{\ZMV}} + } + + \inferrule[WFAp3]{ + \zWellFormed{\ZMV} + }{ + \zWellFormed{\ZApSynNonMatchedArrowL{\ZMV}{\ECMV}} + } + + \inferrule[WFAp4]{ + \zWellFormed{\ZMV} + }{ + \zWellFormed{\ZApSynNonMatchedArrowR{\ECMV}{\ZMV}} + } + + \inferrule[WFInconsistentBranches1]{ + \zWellFormed{\ZMV} + }{ + \zWellFormed{\ZInconBrC{\ZMV}{\ECMV_1}{\ECMV_2}} + } + + \inferrule[WFInconsistentBranches2]{ + \zWellFormed{\ZMV} + }{ + \zWellFormed{\ZInconBrL{\ECMV_1}{\ZMV}{\ECMV_2}} + } + + \inferrule[WFInconsistentBranches3]{ + \zWellFormed{\ZMV} + }{ + \zWellFormed{\ZInconBrR{\ECMV_1}{\ECMV_2}{\ZMV}} + } + + \inferrule[WFPair3]{ + \zWellFormed{\ZMV} + }{ + \zWellFormed{\ZPairAnaNonMatchedProdL{\ZMV}{\ECMV}} + } + + \inferrule[WFPair4]{ + \zWellFormed{\ZMV} + }{ + \zWellFormed{\ZPairAnaNonMatchedProdR{\ECMV}{\ZMV}} + } + + \inferrule[WFProjL2]{ + \zWellFormed{\ZMV} + }{ + \zWellFormed{\ZProjLSynNonMatchedProd{\ZMV}} + } + + \inferrule[WFProjR2]{ + \zWellFormed{\ZMV} + }{ + \zWellFormed{\ZProjRSynNonMatchedProd{\ZMV}} + } \end{mathpar} \subsection{Cursor erasure} From cf7db283719ad98b606c46f5a4701fa204f79a0f Mon Sep 17 00:00:00 2001 From: Eric Zhao <21zhaoe@protonmail.com> Date: Tue, 10 Oct 2023 03:03:10 -0400 Subject: [PATCH 24/24] formalism: Break well-formedness rules across two pages --- formalism/typed.tex | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/formalism/typed.tex b/formalism/typed.tex index f430594..bf59932 100644 --- a/formalism/typed.tex +++ b/formalism/typed.tex @@ -39,7 +39,7 @@ \subsubsection{Well-formedness} \label{sec:typed-well-formedness} \judgbox{\ensuremath{\zWellFormed{\ZCMV}}} $\ZCMV$ is well-formed % -\begin{mathpar} +\begin{mathparpagebreakable} \inferrule[WFCursor]{ }{ \zWellFormed{\ZCCursor{\ECMV}} } @@ -288,7 +288,7 @@ \subsubsection{Well-formedness} }{ \zWellFormed{\ZProjRSynNonMatchedProd{\ZMV}} } -\end{mathpar} +\end{mathparpagebreakable} \subsection{Cursor erasure} \label{sec:typed-cursor-erasure}