From a53ccd6f47c4f0fbe4e7bf78a26b71a1254396f0 Mon Sep 17 00:00:00 2001 From: Eric Zhao <21zhaoe@protonmail.com> Date: Sun, 8 Oct 2023 18:52:13 -0400 Subject: [PATCH 1/8] formalism: Add missing syntax forms for typed hazelnut --- formalism/symbols/untyped.tex | 23 +++++++++++++++++++---- formalism/typed.tex | 9 ++++++++- 2 files changed, 27 insertions(+), 5 deletions(-) diff --git a/formalism/symbols/untyped.tex b/formalism/symbols/untyped.tex index f1e5c8f..0d35afd 100644 --- a/formalism/symbols/untyped.tex +++ b/formalism/symbols/untyped.tex @@ -42,9 +42,6 @@ \newcommand{\ZIfC}[3]{\ensuremath{\ECIf{#1}{#2}{#3}}} \newcommand{\ZIfL}[3]{\ensuremath{\ECIf{#1}{#2}{#3}}} \newcommand{\ZIfR}[3]{\ensuremath{\ECIf{#1}{#2}{#3}}} -\newcommand{\ZInconBrC}[3]{\ensuremath{\ECInconBr{#1}{#2}{#3}}} -\newcommand{\ZInconBrL}[3]{\ensuremath{\ECInconBr{#1}{#2}{#3}}} -\newcommand{\ZInconBrR}[3]{\ensuremath{\ECInconBr{#1}{#2}{#3}}} % let \newcommand{\ZLetL}[3]{\ensuremath{\ECLet{#1}{#2}{#3}}} @@ -59,7 +56,25 @@ % errors \newcommand{\ZFree}[1]{\ensuremath{\ECFree{#1}}} \newcommand{\ZInconType}[1]{\ensuremath{\ECInconType{#1}}} -\newcommand{\ZInconBr}[3]{\ensuremath{\ECInconBr{#1}{#2}{#3}}} +\newcommand{\ZInconBrC}[3]{\ensuremath{\ECInconBr{#1}{#2}{#3}}} +\newcommand{\ZInconBrL}[3]{\ensuremath{\ECInconBr{#1}{#2}{#3}}} +\newcommand{\ZInconBrR}[3]{\ensuremath{\ECInconBr{#1}{#2}{#3}}} +\newcommand{\ZInconAsc}[1]{\ensuremath{\ECInconAsc{#1}}} +\newcommand{\ZSynNonMatchedArrow}[1]{\ensuremath{\ECSynNonMatchedArrow{#1}}} +\newcommand{\ZSynNonMatchedProd}[1]{\ensuremath{\ECSynNonMatchedProd{#1}}} +\newcommand{\ZAnaNonMatchedArrow}[1]{\ensuremath{\ECAnaNonMatchedArrow{#1}}} +\newcommand{\ZAnaNonMatchedProd}[1]{\ensuremath{\ECAnaNonMatchedProd{#1}}} + +\newcommand{\ZLamInconAscT}[3]{\ensuremath{\ECInconAsc{\ECLam{#1}{#2}{#3}}}} +\newcommand{\ZLamInconAscE}[3]{\ensuremath{\ECInconAsc{\ECLam{#1}{#2}{#3}}}} +\newcommand{\ZApSynNonMatchedArrowL}[2]{\ensuremath{\ECAp{\ECSynNonMatchedArrow{#1}}{#2}}} +\newcommand{\ZApSynNonMatchedArrowR}[2]{\ensuremath{\ECAp{\ECSynNonMatchedArrow{#1}}{#2}}} +\newcommand{\ZProjLSynNonMatchedProd}[1]{\ensuremath{\ECProjL{\ECSynNonMatchedProd{#1}}}} +\newcommand{\ZProjRSynNonMatchedProd}[1]{\ensuremath{\ECProjR{\ECSynNonMatchedProd{#1}}}} +\newcommand{\ZLamAnaNonMatchedArrowT}[3]{\ensuremath{\ECAnaNonMatchedArrow{\ECLam{#1}{#2}{#3}}}} +\newcommand{\ZLamAnaNonMatchedArrowE}[3]{\ensuremath{\ECAnaNonMatchedArrow{\ECLam{#1}{#2}{#3}}}} +\newcommand{\ZPairAnaNonMatchedProdL}[2]{\ensuremath{\ECAnaNonMatchedProd{\ECPair{#1}{#2}}}} +\newcommand{\ZPairAnaNonMatchedProdR}[2]{\ensuremath{\ECAnaNonMatchedProd{\ECPair{#1}{#2}}}} % % zipper judgments diff --git a/formalism/typed.tex b/formalism/typed.tex index ec5f84b..901abd2 100644 --- a/formalism/typed.tex +++ b/formalism/typed.tex @@ -21,7 +21,14 @@ \subsection{Syntax} & & \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 & \ZInconType{\ZMV} \mid \ZInconBrC{\ZMV}{\ECMV}{\ECMV} \mid \ZInconBrL{\ECMV}{\ZMV}{\ECMV} \mid \ZInconBrR{\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} \end{array}\] \subsubsection{Well-formedness} From 24e06bafd4c9698732a2afba79e8d8e9e29d1f91 Mon Sep 17 00:00:00 2001 From: Eric Zhao <21zhaoe@protonmail.com> Date: Sun, 8 Oct 2023 19:36:25 -0400 Subject: [PATCH 2/8] formalism: Add missing marked zexp well-formedness rules --- formalism/typed.tex | 121 +++++++++++++++++++++++++++++++++++++------- 1 file changed, 103 insertions(+), 18 deletions(-) diff --git a/formalism/typed.tex b/formalism/typed.tex index 901abd2..92854d3 100644 --- a/formalism/typed.tex +++ b/formalism/typed.tex @@ -40,86 +40,96 @@ \subsubsection{Well-formedness} \zWellFormed{\ZCursor{\ECMV}} } - \inferrule[WFLamT]{ }{ + \inferrule[WFLam1]{ }{ \zWellFormed{\ZLamT{x}{\ZTMV}{\ECMV}} } - \inferrule[WFLamE]{ + \inferrule[WFLam2]{ \zWellFormed{\ZMV} }{ \zWellFormed{\ZLamE{x}{\TMV}{\ZMV}} } - \inferrule[WFApL]{ + \inferrule[WFAp1]{ \zWellFormed{\ZMV} }{ \zWellFormed{\ZApL{\ZMV}{\ECMV}} } - \inferrule[WFApR]{ + \inferrule[WFAp2]{ \zWellFormed{\ZMV} }{ \zWellFormed{\ZApR{\ECMV}{\ZMV}} } - \inferrule[WFLetL]{ + \inferrule[WFLet1]{ \zWellFormed{\ZMV} }{ \zWellFormed{\ZLetL{x}{\ZMV}{\ECMV}} } - \inferrule[WFLetR]{ + \inferrule[WFLet2]{ \zWellFormed{\ZMV} }{ \zWellFormed{\ZLetR{x}{\ECMV}{\ZMV}} } - \inferrule[WFPlusL]{ + \inferrule[WFPlus1]{ \zWellFormed{\ZMV} }{ \zWellFormed{\ZPlusL{\ZMV}{\ECMV}} } - \inferrule[WFPlusR]{ + \inferrule[WFPlus2]{ \zWellFormed{\ZMV} }{ \zWellFormed{\ZPlusR{\ECMV}{\ZMV}} } - \inferrule[WFIfC]{ + \inferrule[WFIf1]{ \zWellFormed{\ZMV} }{ \zWellFormed{\ZIfC{\ZMV}{\ECMV_1}{\ECMV_2}} } - \inferrule[WFIfL]{ + \inferrule[WFIf2]{ \zWellFormed{\ZMV} }{ \zWellFormed{\ZIfL{\ECMV_1}{\ZMV}{\ECMV_2}} } - \inferrule[WFIfC]{ + \inferrule[WFIf3]{ \zWellFormed{\ZMV} }{ - \zWellFormed{\ZIfL{\ZMV}{\ECMV_1}{\ECMV_2}} + \zWellFormed{\ZIfR{\ECMV_1}{\ECMV_2}{\ZMV}} } - \inferrule[WFInconsistentBranchesC]{ + \inferrule[WFPair1]{ \zWellFormed{\ZMV} }{ - \zWellFormed{\ZInconBrC{\ZMV}{\ECMV_1}{\ECMV_2}} + \zWellFormed{\ZPairL{\ZMV}{\ECMV}} } - \inferrule[WFInconsistentBranchesL]{ + \inferrule[WFPair2]{ \zWellFormed{\ZMV} }{ - \zWellFormed{\ZInconBrL{\ECMV_1}{\ZMV}{\ECMV_2}} + \zWellFormed{\ZPairR{\ECMV}{\ZMV}} + } + + \inferrule[WFProjL1]{ + \zWellFormed{\ZMV} + }{ + \zWellFormed{\ZProjL{\ZMV}} } - \inferrule[WFInconsistentBranchesR]{ + \inferrule[WFProjR1]{ \zWellFormed{\ZMV} }{ - \zWellFormed{\ZInconBrL{\ZMV}{\ECMV_1}{\ECMV_2}} + \zWellFormed{\ZProjR{\ZMV}} + } + + \inferrule[WFFree]{ }{ + \zWellFormed{\ZFree{x}} } \inferrule[WFInconsistentTypes]{ @@ -128,6 +138,81 @@ \subsubsection{Well-formedness} }{ \zWellFormed{\ZInconType{\ZMV}} } + + \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 e1dd7f1a570f8da81ebb1a4b388a53d9d051e5d6 Mon Sep 17 00:00:00 2001 From: Eric Zhao <21zhaoe@protonmail.com> Date: Tue, 6 Jun 2023 15:35:50 -0400 Subject: [PATCH 3/8] formalism: Add brief description for untyped action calculus --- formalism/untyped.tex | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) diff --git a/formalism/untyped.tex b/formalism/untyped.tex index fe9b6d6..fbaeda6 100644 --- a/formalism/untyped.tex +++ b/formalism/untyped.tex @@ -7,6 +7,14 @@ \section{Untyped hazelnut} \label{sec:untyped} +In this section we describe an \emph{untyped} version of the Hazelnut action calculus that might be +layered with the marked lambda calculus to yield a structure editing calculus that supports +non-local hole fixes. + +In comparison with the original calculus, this untyped version is not concerned at all with typing +but only the manipulation of syntax. As such, the action judgments are simplified considerably; in +particular, they are no longer bidirectional. The same core metatheorems, except sensibility which +is no longer meaningful in this untyped context, still hold (see \cref{sec:untyped-metatheorems}). \begin{mechanization} \item hazelnut.agda @@ -644,8 +652,6 @@ \subsubsection{Iterated actions} \subsection{Metatheorems} \label{sec:untyped-metatheorems} -\begin{theorem}[name=Sensibility] -\end{theorem} \begin{theorem}[name=Movement Erasure Invariance] \ \begin{enumerate} From 200fdc31cd693ba75c9c3d35419f3108ef331cd0 Mon Sep 17 00:00:00 2001 From: Eric Zhao <21zhaoe@protonmail.com> Date: Sun, 8 Oct 2023 19:52:06 -0400 Subject: [PATCH 4/8] formalism: Use more parens to clarify cursor erasure definitions --- formalism/untyped.tex | 38 +++++++++++++++++++------------------- 1 file changed, 19 insertions(+), 19 deletions(-) diff --git a/formalism/untyped.tex b/formalism/untyped.tex index fbaeda6..769bfb7 100644 --- a/formalism/untyped.tex +++ b/formalism/untyped.tex @@ -41,10 +41,10 @@ \subsubsection{Type cursor erasure} \newcommand{\cursorErasesToRow}[2]{\ensuremath{\cursorErase{#1} & = & #2}} \[\begin{array}{rcl} \cursorErasesToRow{\ZTCursor{\TMV}}{\TMV} \\ - \cursorErasesToRow{(\ZTArrowL{\ZTMV}{\TMV})}{\TArrow{\cursorErase{\ZTMV}}{\TMV}} \\ - \cursorErasesToRow{(\ZTArrowR{\TMV}{\ZTMV})}{\TArrow{\TMV}{\cursorErase{\ZTMV}}} \\ - \cursorErasesToRow{(\ZTProdL{\ZTMV}{\TMV})}{\TProd{\cursorErase{\ZTMV}}{\TMV}} \\ - \cursorErasesToRow{(\ZTProdR{\TMV}{\ZTMV})}{\TProd{\TMV}{\cursorErase{\ZTMV}}} \\ + \cursorErasesToRow{(\ZTArrowL{\ZTMV}{\TMV})}{\TArrow{(\cursorErase{\ZTMV})}{\TMV}} \\ + \cursorErasesToRow{(\ZTArrowR{\TMV}{\ZTMV})}{\TArrow{\TMV}{(\cursorErase{\ZTMV})}} \\ + \cursorErasesToRow{(\ZTProdL{\ZTMV}{\TMV})}{\TProd{(\cursorErase{\ZTMV})}{\TMV}} \\ + \cursorErasesToRow{(\ZTProdR{\TMV}{\ZTMV})}{\TProd{\TMV}{(\cursorErase{\ZTMV})}} \\ \end{array}\] \subsubsection{Expression cursor erasure} @@ -53,21 +53,21 @@ \subsubsection{Expression cursor erasure} % \[\begin{array}{rcl} \cursorErasesToRow{\ZCursor{\EMV}}{\EMV} \\ - \cursorErasesToRow{(\ZLamT{x}{\ZTMV}{\EMV})}{\ELam{x}{\cursorErase{\ZTMV}}{\EMV}} \\ - \cursorErasesToRow{(\ZLamE{x}{\TMV}{\ZMV})}{\ELam{x}{\TMV}{\cursorErase{\ZMV}}} \\ - \cursorErasesToRow{(\ZApL{\ZMV}{\EMV})}{\EAp{\cursorErase{\ZMV}}{\EMV}} \\ - \cursorErasesToRow{(\ZApR{\EMV}{\ZMV})}{\EAp{\EMV}{\cursorErase{\ZMV}}} \\ - \cursorErasesToRow{(\ZLetL{x}{\ZMV}{\EMV})}{\ELet{x}{\cursorErase{\ZMV}}{\EMV}} \\ - \cursorErasesToRow{(\ZLetR{x}{\EMV}{\ZMV})}{\ELet{x}{\EMV}{\cursorErase{\ZMV}}} \\ - \cursorErasesToRow{(\ZPlusL{\ZMV}{\EMV})}{\EPlus{\cursorErase{\ZMV}}{\EMV}} \\ - \cursorErasesToRow{(\ZPlusR{\EMV}{\ZMV})}{\EPlus{\EMV}{\cursorErase{\ZMV}}} \\ - \cursorErasesToRow{(\ZIfC{\ZMV}{\EMV_1}{\EMV_2})}{\EIf{\cursorErase{\ZMV}}{\EMV_1}{\EMV_2}} \\ - \cursorErasesToRow{(\ZIfL{\EMV_1}{\ZMV}{\EMV_2})}{\EIf{\EMV_1}{\cursorErase{\ZMV}}{\EMV_2}} \\ - \cursorErasesToRow{(\ZIfL{\EMV_1}{\EMV_2}{\ZMV})}{\EIf{\EMV_1}{\EMV_2}{\cursorErase{\ZMV}}} \\ - \cursorErasesToRow{(\ZPairL{\ZMV}{\EMV})}{\EPair{\cursorErase{\ZMV}}{\EMV}} \\ - \cursorErasesToRow{(\ZPairR{\EMV}{\ZMV})}{\EPair{\EMV}{\cursorErase{\ZMV}}} \\ - \cursorErasesToRow{(\ZProjL{\ZMV})}{\EProjL{\cursorErase{\ZMV}}} \\ - \cursorErasesToRow{(\ZProjR{\ZMV})}{\EProjR{\cursorErase{\ZMV}}} \\ + \cursorErasesToRow{(\ZLamT{x}{\ZTMV}{\EMV})}{\ELam{x}{(\cursorErase{\ZTMV})}{\EMV}} \\ + \cursorErasesToRow{(\ZLamE{x}{\TMV}{\ZMV})}{\ELam{x}{\TMV}{(\cursorErase{\ZMV})}} \\ + \cursorErasesToRow{(\ZApL{\ZMV}{\EMV})}{\EAp{(\cursorErase{\ZMV})}{\EMV}} \\ + \cursorErasesToRow{(\ZApR{\EMV}{\ZMV})}{\EAp{\EMV}{(\cursorErase{\ZMV})}} \\ + \cursorErasesToRow{(\ZLetL{x}{\ZMV}{\EMV})}{\ELet{x}{(\cursorErase{\ZMV})}{\EMV}} \\ + \cursorErasesToRow{(\ZLetR{x}{\EMV}{\ZMV})}{\ELet{x}{\EMV}{(\cursorErase{\ZMV})}} \\ + \cursorErasesToRow{(\ZPlusL{\ZMV}{\EMV})}{\EPlus{(\cursorErase{\ZMV})}{\EMV}} \\ + \cursorErasesToRow{(\ZPlusR{\EMV}{\ZMV})}{\EPlus{\EMV}{(\cursorErase{\ZMV})}} \\ + \cursorErasesToRow{(\ZIfC{\ZMV}{\EMV_1}{\EMV_2})}{\EIf{(\cursorErase{\ZMV})}{\EMV_1}{\EMV_2}} \\ + \cursorErasesToRow{(\ZIfL{\EMV_1}{\ZMV}{\EMV_2})}{\EIf{\EMV_1}{(\cursorErase{\ZMV})}{\EMV_2}} \\ + \cursorErasesToRow{(\ZIfL{\EMV_1}{\EMV_2}{\ZMV})}{\EIf{\EMV_1}{\EMV_2}{(\cursorErase{\ZMV})}} \\ + \cursorErasesToRow{\ZPairL{\ZMV}{\EMV}}{\EPair{\cursorErase{\ZMV}}{\EMV}} \\ + \cursorErasesToRow{\ZPairR{\EMV}{\ZMV}}{\EPair{\EMV}{\cursorErase{\ZMV}}} \\ + \cursorErasesToRow{(\ZProjL{\ZMV})}{\EProjL{(\cursorErase{\ZMV})}} \\ + \cursorErasesToRow{(\ZProjR{\ZMV})}{\EProjR{(\cursorErase{\ZMV})}} \\ \end{array}\] \subsection{Action model} From 04e9c92ac05ea70596fa91f0c290ed0f2bf7e862 Mon Sep 17 00:00:00 2001 From: Eric Zhao <21zhaoe@protonmail.com> Date: Sun, 8 Oct 2023 19:53:17 -0400 Subject: [PATCH 5/8] formalism: Fix AEZipProjL and AEZipProjR --- formalism/untyped.tex | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/formalism/untyped.tex b/formalism/untyped.tex index 769bfb7..ae4e454 100644 --- a/formalism/untyped.tex +++ b/formalism/untyped.tex @@ -594,13 +594,13 @@ \subsubsection{Expression actions} \inferrule[AEZipProjL]{ \AUEAction{\ZMV}{\ZMV'}{\AMV} }{ - \AUEAction{\ZProjL{\ZMV}{\EMV}}{\ZProjL{\ZMV'}{\EMV}}{\AMV} + \AUEAction{\ZProjL{\ZMV}}{\ZProjL{\ZMV'}}{\AMV} } \inferrule[AEZipProjR]{ \AUEAction{\ZMV}{\ZMV'}{\AMV} }{ - \AUEAction{\ZProjR{\EMV}{\ZMV}}{\ZProjR{\EMV}{\ZMV'}}{\AMV} + \AUEAction{\ZProjR{\ZMV}}{\ZProjR{\ZMV'}}{\AMV} } \end{mathparpagebreakable} From b3b18e232f1b7488d2a564a86d9ddc0672d5d67e Mon Sep 17 00:00:00 2001 From: Eric Zhao <21zhaoe@protonmail.com> Date: Sun, 8 Oct 2023 20:34:03 -0400 Subject: [PATCH 6/8] formalism: Use underline instead of hat for zexp --- formalism/symbols/untyped.tex | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/formalism/symbols/untyped.tex b/formalism/symbols/untyped.tex index 0d35afd..91dae5e 100644 --- a/formalism/symbols/untyped.tex +++ b/formalism/symbols/untyped.tex @@ -4,8 +4,8 @@ % zippered types % \newcommand{\ZTMName}{{\normalfont\textsf{ZType}}} -\newcommand{\ZTMSet}{\ensuremath{\hat{T}}} -\newcommand{\ZTMV}{\ensuremath{\hat{\tau}}} +\newcommand{\ZTMSet}{\ensuremath{\underline{T}}} +\newcommand{\ZTMV}{\ensuremath{\underline{\tau}}} % cursor \newcommand{\ZTCursor}[1]{\ensuremath{\ZCursor{#1}}} @@ -20,8 +20,8 @@ % zippered expressions % \newcommand{\ZMName}{{\normalfont\textsf{ZExp}}} -\newcommand{\ZMSet}{\ensuremath{\hat{E}}} -\newcommand{\ZMV}{\ensuremath{\hat{e}}} +\newcommand{\ZMSet}{\ensuremath{\underline{E}}} +\newcommand{\ZMV}{\ensuremath{\underline{e}}} % cursor \definecolor{cursorhighlight}{RGB}{230,255,230} From 350d92c6b3d2f712e772c4309133bdd657831334 Mon Sep 17 00:00:00 2001 From: Eric Zhao <21zhaoe@protonmail.com> Date: Tue, 10 Oct 2023 02:00:38 -0400 Subject: [PATCH 7/8] formalism: Indicate domain/codomain for metafunctions --- formalism/untyped.tex | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/formalism/untyped.tex b/formalism/untyped.tex index ae4e454..6ab16b0 100644 --- a/formalism/untyped.tex +++ b/formalism/untyped.tex @@ -36,7 +36,7 @@ \subsection{Cursor erasure} \subsubsection{Type cursor erasure} \label{sec:untyped-type-cursor-erasure} -\judgbox{\ensuremath{\cursorErase{\ZTMV}}} is a metafunction defined as follows: +\judgbox{\ensuremath{\cursorErase{\ZTMV}}} is a metafunction $\ZTMName \to \TMName$ defined as follows: % \newcommand{\cursorErasesToRow}[2]{\ensuremath{\cursorErase{#1} & = & #2}} \[\begin{array}{rcl} @@ -49,7 +49,7 @@ \subsubsection{Type cursor erasure} \subsubsection{Expression cursor erasure} \label{sec:untyped-expression-cursor-erasure} -\judgbox{\ensuremath{\cursorErase{\ZMV}}} is a metafunction defined as follows: +\judgbox{\ensuremath{\cursorErase{\ZMV}}} is a metafunction $\ZMName \to \EMName$ defined as follows: % \[\begin{array}{rcl} \cursorErasesToRow{\ZCursor{\EMV}}{\EMV} \\ From b1939cec79e6e7748d16d1f29981735880512ba3 Mon Sep 17 00:00:00 2001 From: Eric Zhao <21zhaoe@protonmail.com> Date: Tue, 10 Oct 2023 02:41:18 -0400 Subject: [PATCH 8/8] formalism: Clean up formatting of untyped hazelnut metatheorems --- formalism/untyped.tex | 70 ++++++++++++++++++++++++++----------------- 1 file changed, 43 insertions(+), 27 deletions(-) diff --git a/formalism/untyped.tex b/formalism/untyped.tex index 6ab16b0..541203d 100644 --- a/formalism/untyped.tex +++ b/formalism/untyped.tex @@ -655,61 +655,77 @@ \subsection{Metatheorems} \begin{theorem}[name=Movement Erasure Invariance] \ \begin{enumerate} - \item If $\AUTAction{\ZTMV}{\ZTMV'}{\AMove{\MMV}}$, then $\cursorErase{\ZTMV} = - \cursorErase{\ZTMV'}$. + \item If $\AUTAction{\ZTMV}{\ZTMV'}{\AMove{\MMV}}$, + then $\cursorErase{\ZTMV} = \cursorErase{\ZTMV'}$. - \item If $\AUEAction{\ZMV}{\ZMV'}{\AMove{\MMV}}$, then $\cursorErase{\ZMV} = - \cursorErase{\ZMV'}$. + \item If $\AUEAction{\ZMV}{\ZMV'}{\AMove{\MMV}}$, + then $\cursorErase{\ZMV} = \cursorErase{\ZMV'}$. \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 $\cursorErase{\ZMV} = \cursorErase{\ZMV'}$, then there exists $\AIMV$ such that - $\movements{\AIMV}$ and $\AUEActionIter{\ZMV}{\ZMV'}{\AIMV}$. + \item If $\cursorErase{\ZTMV} = \cursorErase{\ZTMV'}$, + then there exists $\AIMV$ + such that $\movements{\AIMV}$ + and $\AUTActionIter{\ZTMV}{\ZTMV'}{\AIMV}$. + + \item If $\cursorErase{\ZMV} = \cursorErase{\ZMV'}$, + then there exists $\AIMV$ + such that $\movements{\AIMV}$ + and $\AUEActionIter{\ZMV}{\ZMV'}{\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 $\cursorErase{\ZMV} = \EMV$, then there exists $\AIMV$ such that $\movements{\AIMV}$ - and $\AUEActionIter{\ZMV}{\ZTCursor{\EMV}}{\AIMV}$. + \item If $\cursorErase{\ZTMV} = \TMV$, + then there exists $\AIMV$ + such that $\movements{\AIMV}$ + and $\AUTActionIter{\ZTMV}{\ZTCursor{\TMV}}{\AIMV}$. + + \item If $\cursorErase{\ZMV} = \EMV$, + then there exists $\AIMV$ + such that $\movements{\AIMV}$ + and $\AUEActionIter{\ZMV}{\ZTCursor{\EMV}}{\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 $\cursorErase{\ZMV} = \EMV$, then there exists $\AIMV$ such that $\movements{\AIMV}$ - and $\AUEActionIter{\ZTCursor{\EMV}}{\ZMV}{\AIMV}$. + \item If $\cursorErase{\ZTMV} = \TMV$, + then there exists $\AIMV$ + such that $\movements{\AIMV}$ + and $\AUTActionIter{\ZTCursor{\TMV}}{\ZTMV}{\AIMV}$. + + \item If $\cursorErase{\ZMV} = \EMV$, + then there exists $\AIMV$ + such that $\movements{\AIMV}$ + and $\AUEActionIter{\ZTCursor{\EMV}}{\ZMV}{\AIMV}$. \end{enumerate} \end{lemma} \begin{theorem}[name=Constructability] \ \begin{enumerate} - \item For every $\TMV$, there exists $\AIMV$ such that - $\AUTActionIter{\ZTCursor{\TUnknown}}{\ZTCursor{\TMV}}{\AIMV}$. + \item For every $\TMV$, + there exists $\AIMV$ + such that $\AUTActionIter{\ZTCursor{\TUnknown}}{\ZTCursor{\TMV}}{\AIMV}$. - \item For every $\EMV$, there exists $\AIMV$ such that - $\AUEActionIter{\ZCursor{\EEHole}}{\ZCursor{\EMV}}{\AIMV}$. + \item For every $\EMV$, + there exists $\AIMV$ + such that $\AUEActionIter{\ZCursor{\EEHole}}{\ZCursor{\EMV}}{\AIMV}$. \end{enumerate} \end{theorem} \begin{theorem}[name=Determinism] \ \begin{enumerate} - \item If $\AUTActionIter{\ZTMV}{\ZTMV'}{\AMV}$ and $\AUTActionIter{\ZTMV}{\ZTMV''}{\AMV}$, then - $\ZTMV' = \ZTMV''$. + \item If $\AUTActionIter{\ZTMV}{\ZTMV'}{\AMV}$ + and $\AUTActionIter{\ZTMV}{\ZTMV''}{\AMV}$, + then $\ZTMV' = \ZTMV''$. - \item If $\AUEActionIter{\ZMV}{\ZMV'}{\AMV}$ and $\AUEActionIter{\ZMV}{\ZMV''}{\AMV}$, then - $\ZMV' = \ZMV''$. + \item If $\AUEActionIter{\ZMV}{\ZMV'}{\AMV}$ + and $\AUEActionIter{\ZMV}{\ZMV''}{\AMV}$, + then $\ZMV' = \ZMV''$. \end{enumerate} \end{theorem}