Bug fixes + recompilation

- use macros for push, pop, PIEO, PIEOTree, etc - change iff to implies in Defn 1.1, eq (2)
cucapra · Aug 10, 2024 · c744185 · c744185
1 parent d9ee59c
commit c744185
Show file tree

Hide file tree

Showing 2 changed files with 6 additions and 8 deletions.
diff --git a/pieo-trees/notes.pdf b/pieo-trees/notes.pdf
diff --git a/pieo-trees/notes.tex b/pieo-trees/notes.tex
@@ -122,7 +122,7 @@ \section{Structure \& Semantics}
     These three maps play nicely together: 
     \begin{align}
         \pop(p, f) \text{ is undefined} &\iff \pop(\proj(p, f)) \text{ is undefined} \label{eq:pieo1}\\
-        \pop(p, f) = (\pkt, p^\prime) &\iff \pop(\proj(p, f)) = (\pkt, \proj(p^\prime, f)) \label{eq:pieo2}\\
+        \pop(p, f) = (\pkt, p^\prime) &\implies \pop(\proj(p, f)) = (\pkt, \proj(p^\prime, f)) \label{eq:pieo2}\\
         \proj(\push(p, s, d, r), f) &= 
         \begin{cases}
             \push(\proj(p, f), s, r) & f(d) \text{ holds true}\\
@@ -163,7 +163,7 @@ \section{Structure \& Semantics}
             \forall i \in [1, n]. \; qs[i] \in \mathbf{PIEOTree}(ts[i])
         }
         {
-            \Internal(qs, p) \in \mathbf{PIEOTree}(\Node(ts))
+            \Internal(qs, p) \in \PIEOTree(\Node(ts))
         }
     \end{align*}
 \end{dfn}
@@ -174,15 +174,15 @@ \section{Structure \& Semantics}
     \begin{align*}
         \inference{}
         {
-            \text{POP}(p, f) = (\pkt, p^\prime)
+            \pop(p, f) = (\pkt, p^\prime)
         }
         {
             \pop(\Leaf(p), f) = (\pkt, \Leaf(p^\prime))
         }
         &&
         \inference{}
         {
-            \text{POP}(p, f) = (i, p^\prime)\\
+            \pop(p, f) = (i, p^\prime)\\
             \pop(qs[i], f) = (\pkt, q^\prime)
         }
         {
@@ -197,15 +197,15 @@ \section{Structure \& Semantics}
     \begin{align*}
         \inference{}
         {
-            \text{PUSH}(p, \pkt, d, r) = p^\prime
+            \push(p, \pkt, d, r) = p^\prime
         }
         {
             \push(\Leaf(p), \pkt, d, r) = \Leaf(p^\prime)
         }
         &&
         \inference{}
         {
-            \text{PUSH}(p, i, d, r) = p^\prime\\ 
+            \push(p, i, d, r) = p^\prime\\ 
             \push(qs[i],  \pkt, d, pt) = q^\prime
         }
         {
@@ -260,8 +260,6 @@ \section{Well-Formedness}
     \textcolor{red}{TBD}
 \end{proof}
 
-\newpage
-
 \section{Projection}
 
 \begin{dfn}