Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

formalism: Clean up section on untyped Hazelnut #7

Merged
merged 8 commits into from
Oct 10, 2023
Merged

formalism: Clean up section on untyped Hazelnut #7

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
8 commits
Select commit Hold shift + click to select a range
217e80e
formalism: Add missing syntax forms for typed hazelnut
mirryi Oct 8, 2023
7671d01
formalism: Add missing marked zexp well-formedness rules
mirryi Oct 8, 2023
cf1e7dc
formalism: Add brief description for untyped action calculus
mirryi Jun 6, 2023
4c533d5
formalism: Use more parens to clarify cursor erasure definitions
mirryi Oct 8, 2023
331aa34
formalism: Fix AEZipProjL and AEZipProjR
mirryi Oct 8, 2023
c03ab91
formalism: Use underline instead of hat for zexp
mirryi Oct 9, 2023
c70bb9d
formalism: Indicate domain/codomain for metafunctions
mirryi Oct 10, 2023
4478209
formalism: Clean up formatting of untyped hazelnut metatheorems
mirryi Oct 10, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
31 changes: 23 additions & 8 deletions formalism/symbols/untyped.tex
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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}}}
Expand All @@ -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}
Expand All @@ -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}}}
Expand All @@ -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
Expand Down
130 changes: 111 additions & 19 deletions formalism/typed.tex
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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}
Expand All @@ -33,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]{
Expand All @@ -121,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}
Expand Down
Loading