From eb67f0635d19240425323e3b1dad95dfb1e5ceb7 Mon Sep 17 00:00:00 2001 From: "Jip J. Dekker" Date: Wed, 7 Apr 2021 10:10:11 +1000 Subject: [PATCH] Adjust grammar and proofs in Rewriting chapter --- .chktexrc | 2 +- chapters/4_rewriting.tex | 129 +++++++++++++++++++-------------------- 2 files changed, 63 insertions(+), 68 deletions(-) diff --git a/.chktexrc b/.chktexrc index c9a9413..48dc70a 100644 --- a/.chktexrc +++ b/.chktexrc @@ -1,5 +1,5 @@ # Exclude these environments from syntax checking VerbEnvir { pgfpicture tikzpicture mzn nzn grammar proof } -MathCmd { hypo infer1 infer2 infer3 } +MathCmd { \hypo } WipeArg { \mzninline:{} \nzninline:{} \Sem:{} \texttt:{} } diff --git a/chapters/4_rewriting.tex b/chapters/4_rewriting.tex index 42fbf32..d6f0627 100644 --- a/chapters/4_rewriting.tex +++ b/chapters/4_rewriting.tex @@ -68,15 +68,17 @@ and where expressions have \mzninline{par} type. \begin{figure} \begin{grammar} - ::= * + ::= ** - ::= "function" ":" "(" ["," ]* ")" [ "=" ]";" + ::= "predicate" "(" ["," ]* ");" + + ::= "function" ":" "(" ["," ]* ")" "=" ";" ::= | ::= - \alt "(" ["," ]* ")" - \alt "let" "{" * "}" "in" + \alt "(" ["," ]* ")" + \alt "let" "{" * "}" "in" \alt "if" "then" "else" "endif" \alt "[" "|" "where" "]" \alt "(" ["," ]* ")" @@ -164,22 +166,23 @@ The translation from \minizinc\ to \microzinc\ involves the following steps: constraint for each element of the array. \begin{mzn} - predicate all_different(array[int] of var int: x) = - forall([ - int_neq(element(x,i),element(x,j)) - | i in range(1,length(x)), - j in range(1,length(x)) - where int_lt(i,j) - ]); + function var bool: all_different(array[int] of var int: x) = + forall([ + int_neq(element(x, i),element(x, j)) + | i in range(1, length(x)), + j in range(1, length(x)) + where int_lt(i,j) + ]); - predicate main(int: n) = let { - array[range(1,n)] of var int: pigeon; + function var bool: main(int: n) = let { + var bool: root_ctx; + array[range(1, n)] of var int: pigeon; constraint forall([ - set_in(element(pigeon,i), range(1,int_minus(n,1))) - | i in range(1,n) + set_in(element(pigeon, i), range(1, int_minus(n,1))) + | i in range(1, n) ]) constraint all_different(pigeon); - } in true; + } in root_ctx; \end{mzn} For a concrete instance of the model, we can then create a simple \nanozinc\ @@ -308,24 +311,20 @@ suitable alpha renaming. \begin{figure*} \centering \begin{prooftree} - \hypo{\ptinline{F(\(p_1, \ldots, p_k\)) = E;} \in \Prog \text{~where the~} p_i \text{~are fresh}} - \infer[no rule]1{\Sem{\(a_i\)}{\Prog, \Env_{i-1}} \Rightarrow \tuple{v_i, - \Env_i'}, \ \Env_0=\Env, \Env_i=\Env_i'\cup\{p_i\mapsto v_i\sep[]\}, \forall 1 \leq i \leq k} - \infer[no rule]1{\Sem{E}{\Prog, \Env_k} \Rightarrow \tuple{v, \Env'}} - \infer1[(Call)]{\Sem{F(\(a_1, \ldots, a_k\))}{\Prog, \Env_{0}} \Rightarrow \tuple{v, \Env'}} + \hypo{\ptinline{F(\(p_1, \ldots{}, p_k\)) = E;} \in{} \Prog{} \text{~where the~} p_i \text{~are fresh}} + \infer[no rule]1{\Sem{E}{\Prog, \Env_{[p_i \mapsto a_i, \forall{} 1 \leq{} i \leq{} k]}} \Rightarrow \tuple{v, \Env'}} + \infer1[(Call)]{\Sem{F(\(a_1, \ldots, a_k\))}{\Prog, \Env} \Rightarrow{} \tuple{v, \Env'_{[a_i \mapsto p_i, \forall{} 1 \leq{} i \leq{} k]}}} \end{prooftree} \\ -\medskip +\bigskip \begin{prooftree} \hypo{\ptinline{F} \in \text{Builtins}} - \hypo{\Sem{\(a_i\)}{\Prog, \Env} \Rightarrow \tuple{v_i, \Env}, \forall{} 1 \leq{} i \leq{} k} - \infer2[(CallBuiltin)]{\Sem{F(\(a_1, \ldots, a_k\))}{\Prog, \Env} \Rightarrow \tuple{ \mathit{eval}(\ptinline{F}(v_1,\ldots, v_k)), \Env}} + \infer1[(CallBuiltin)]{\Sem{F(\(a_1, \ldots, a_k\))}{\Prog, \Env} \Rightarrow{} \tuple{ \mathit{eval}(\ptinline{F}(a_1,\ldots, a_k)), \Env}} \end{prooftree} \\ -\medskip +\bigskip \begin{prooftree} \hypo{\ptinline{F(\(p_1, \ldots, p_k\));} \in \Prog} - \hypo{\Sem{\(a_i\)}{\Prog, \Env_{i-1}} \Rightarrow \tuple{v_i, \Env_i}, \forall 1 \leq i \leq k} - \infer2[(CallPrimitive)]{\Sem{F(\(a_1, \ldots, a_k\))}{\Prog, \Env_0} \Rightarrow - \tuple{ x, \{ x \mapsto \ptinline{F}(v_1,\ldots, v_k) \sep [] \} \cup \Env_k}} + \infer1[(CallPredicate)]{\Sem{F(\(a_1, \ldots, a_k\))}{\Prog, \Env_0} \Rightarrow + \tuple{\texttt{constraint~} \text{F}(v_1, \ldots, v_k), \Env_k}} \end{prooftree} \caption{\label{fig:4-rewrite-to-nzn-calls} Rewriting rules for partial evaluation of \microzinc\ calls to \nanozinc.} @@ -343,45 +342,44 @@ directly, such as arithmetic and Boolean operations on fixed values. The rule simply returns the result of evaluating the built-in function on the evaluated parameter values. -The (CallPrimitive) rule applies to non-built-in functions that are defined -without a function body. These are considered primitives, and as such simply -need to be transferred into the \nanozinc\ program. The rule evaluates all -actual parameters, and creates a new variable \(x\) to store the result, which is -simply the function applied to the evaluated parameters. +The (CallPredicate) rule applies to calls to solver predicates. These are +considered primitives, and as such simply need to be transferred into the +\nanozinc\ program. The rule evaluates all actual parameters, and creates a new +variable \(x\) to store the result, which is simply the function applied to the +evaluated parameters. \begin{figure*} \centering \begin{prooftree} \hypo{\Sem{\(\mathbf{I}\)}{\Prog, \Env} \Rightarrow (\Ctx, \Env')} - \hypo{\Sem{\(E\)}{\Prog, \Env'} \Rightarrow \tuple{v, \Env''}} - \hypo{x \text{~fresh}} - \infer3[(LetC)]{\Sem{let \{ \(\mathbf{I}\) \} in \(E\)}{\Prog, \Env} \Rightarrow - \tuple{x, \{ x \mapsto v \sep \Ctx \} \cup \Env''}} + \hypo{\Sem{\(E\)}{\Prog, \Env'} \Rightarrow \tuple{x, \{ t : x \}\cup{}\Env''}} + \infer2[(LetC)]{\Sem{let \{ \(\mathbf{I}\) \} in \(E\)}{\Prog, \Env} \Rightarrow + \tuple{x, \{ t : x_{\texttt{~└──~}} \Ctx \} \cup \Env''}} \end{prooftree} \\ -\medskip +\bigskip \begin{prooftree} \hypo{} \infer1[(Item0)]{\Sem{\(\epsilon\)}{\Prog, \Env} \Rightarrow \tuple{\ptinline{true}, \Env}} \end{prooftree} \\ -\medskip +\bigskip \begin{prooftree} - \hypo{\Sem{\(\mathbf{I}\)}{\Prog, \Env\ \cup\ \{x \mapsto\ \texttt{mkvar()} \sep\ []\}} \Rightarrow \tuple{\Ctx, \Env'}} + \hypo{\Sem{\(\mathbf{I}\)}{\Prog, \Env\ \cup\ \{t : x\}} \Rightarrow \tuple{\Ctx, \Env'}} \infer1[(ItemT)]{\Sem{\(t:x, \mathbf{I}\)}{\Prog, \Env} \Rightarrow \tuple{\Ctx, \Env'}} \end{prooftree} \\ -\medskip +\bigskip \begin{prooftree} \hypo{\Sem{\(E\)}{\Prog, \Env} \Rightarrow \tuple{v, \Env'}} - \hypo{\Sem{\(\mathbf{I}\)}{\Prog, \Env' \cup\ \{x \mapsto\ v \sep\ [] \}} \Rightarrow \tuple{\Ctx, \Env''}} + \hypo{\Sem{\(\mathbf{I}\)}{\Prog, \Env'_{[x \mapsto v]}} \Rightarrow \tuple{\Ctx, \Env''}} \infer2[(ItemTE)]{\Sem{\(t:x = E, \mathbf{I}\)}{\Prog, \Env} \Rightarrow \tuple{\Ctx, \Env''}} \end{prooftree} \\ -\medskip +\bigskip \begin{prooftree} - \hypo{\Sem{\(E\)}{\Prog, \Env} \Rightarrow \tuple{\left(v_{1}, \ldots, v_{n}\right), \Env'}} - \infer[no rule]1{\Sem{\(\mathbf{I}\)}{\Prog, \Env' \cup\ \{x_{1} \mapsto\ v_{1} \sep\ [] \} \cup\ \ldots\ \cup\ \{x_{n} \mapsto\ v_{n} \sep\ [] \}} \Rightarrow \tuple{\Ctx, \Env''}} - \infer1[(ItemTD)]{\Sem{\(\left(t_{1}: x_{1}, \ldots, t_{n}: x_{n}\right) = E, \mathbf{I}\)}{\Prog, \Env} \Rightarrow + \hypo{\Sem{\(E\)}{\Prog, \Env} \Rightarrow \tuple{\left(v_{\langle{}1\rangle}, \ldots, v_{\langle{}k\rangle}\right), \Env'}} + \infer[no rule]1{\Sem{\(\mathbf{I}\)}{\Prog, \Env'_{[x_{i} \mapsto v_{\langle{}i\rangle}, \forall{} 1 \leq{} i \leq{} k]}} \Rightarrow\ \tuple{\Ctx, \Env''}} + \infer1[(ItemTD)]{\Sem{\(\left(t_{1}: x_{1}, \ldots, t_{k}: x_{k}\right) = E, \mathbf{I}\)}{\Prog, \Env} \Rightarrow\ \tuple{\Ctx, \Env''}} \end{prooftree} \\ -\medskip +\bigskip \begin{prooftree} \hypo{\Sem{\(C\)}{\Prog, \Env} \Rightarrow \tuple{v, \Env'}} \hypo{\Sem{\(\mathbf{I}\)}{\Prog, \Env'} \Rightarrow \tuple{\Ctx, \Env''}} @@ -405,56 +403,53 @@ is the base case for a list of let items. \begin{figure*} \centering +% \begin{prooftree} +% \hypo{x \in \langle \text{ident} \rangle} +% \hypo{v \in \langle \text{literal} \rangle} +% \infer2[(IdC)]{\Sem{\(x\)}{\Prog, \{x \mapsto\ v \sep\ []\} \cup\ \Env} \Rightarrow \tuple{v, \{x \mapsto v \sep [] \} \cup \Env}} +% \end{prooftree} \\ +% \bigskip \begin{prooftree} - \hypo{x \in \syntax{}} - \hypo{v \in \syntax{}} - \infer2[(IdC)]{\Sem{\(x\)}{\Prog, \{x \mapsto\ v \sep\ []\} \cup\ \Env} \Rightarrow \tuple{v, \{x \mapsto v \sep [] \} \cup \Env}} -\end{prooftree} \\ -\medskip -\begin{prooftree} - \hypo{x \in \syntax{}} + \hypo{x \in \langle \text{ident} \rangle} \hypo{v} \hypo{\phi \text{~otherwise}} - \infer3[(IdX)]{\Sem{\(x\)}{\Prog, \{x \mapsto\ v \sep\ \phi\ \} \cup\ \Env} \Rightarrow \tuple{x, \{x \mapsto v \sep \phi \} \cup \Env}} + \infer3[(IdX)]{\Sem{\(x\)}{\Prog, \{t: x^{\texttt{~└──~}} \phi\ \} \cup\ \Env} \Rightarrow \tuple{x, \{t: x^{\texttt{~└──~}} \phi \cup \phi}} \end{prooftree} \\ -\medskip +\bigskip \begin{prooftree} \hypo{c \text{~constant}} \infer1[(Const)]{\Sem{c}{\Prog, \Env} \Rightarrow \tuple{c, \Env}} \end{prooftree} \\ -\medskip +\bigskip \begin{prooftree} \hypo{\Sem{\(E_{i}\)}{\Prog,\Env^{i-1}} \Rightarrow \tuple{v_{i}, \Env^{i}}, \forall{} 1 \leq{} i \leq{} k} - \infer1[(Tuple)]{\Sem{\(\left(E_{1}, \ldots, E_{k}\right)\)}{\Prog, \Env^{0}} \Rightarrow \tuple{x, \{x \mapsto \left(v_{1}, \ldots, v_{n}\right) \sep [] \} \cup \Env^{k}}} + \infer1[(Tuple)]{\Sem{\(\left(E_{1}, \ldots, E_{k}\right)\)}{\Prog, \Env^{0}} \Rightarrow \tuple{x, \Env^{k}_{[x_{\langle{}i\rangle} \mapsto v_{i}, \forall{} 1 \leq{} i \leq{} k]}}} \end{prooftree} \\ -\medskip +\bigskip \begin{prooftree} \hypo{\Sem{\(C\)}{\Prog, \Env} \Rightarrow \tuple{\ptinline{true}, \_}} \infer1[(If\(_T\))]{\Sem{if \(C\) then \(E_t\) else \(E_e\) endif}{\Prog, \Env} \Rightarrow \Sem{\(E_t\)}{\Prog, \Env}} \end{prooftree} \\ -\medskip +\bigskip \begin{prooftree} \hypo{\Sem{\(C\)}{\Prog, \Env} \Rightarrow \tuple{\ptinline{false}, \_}} \infer1[(If\(_F\))]{\Sem{if \(C\) then \(E_t\) else \(E_e\) endif}{\Prog, \Env} \Rightarrow \Sem{\(E_e\)}{\Prog, \Env}} \end{prooftree} \\ -\medskip +\bigskip \begin{prooftree} \hypo{\Sem{G}{\Prog,\Env} \Rightarrow \tuple{ \ptinline{true}, \_}} \hypo{\Sem{\(E\)}{\Prog, \Env} \Rightarrow \tuple {v, \Env'}} \infer2[(WhereT)]{\Sem{\([E ~|~ \mbox{where~} G]\)}{\Prog, \Env} \Rightarrow \tuple{[v], \Env'}} \end{prooftree} \\ -\medskip +\bigskip \begin{prooftree} \hypo{\Sem{G}{\Prog,\Env} \Rightarrow \tuple{\ptinline{false}, \_}} \infer1[(WhereF)]{\Sem{\([E ~|~ \mbox{where~} G]\)}{\Prog, \Env} \Rightarrow \tuple{[], \Env}} \end{prooftree} \\ -\medskip +\bigskip \begin{prooftree} \hypo{\Sem{\(\mathit{PE}\)}{\Prog,\Env} \Rightarrow \tuple{S, \_}} - \infer[no rule]1{\Sem{\([E ~|~ \mathit{GE} \mbox{~where~} G]\)}{\Prog, \Env\ \cup\ \{ x\mapsto\ - v \sep\ []\}}} - \infer[no rule]1{\hspace{8em} \Rightarrow \tuple{A_v, \Env \cup \{x \mapsto v \sep []\} \cup \Env_v}, \forall - v \in S } + \infer[no rule]1{\Sem{\([E ~|~ \mathit{GE} \mbox{~where~} G]\)}{\Prog, \Env_{[x \mapsto v]}} \Rightarrow \tuple{A_v, \Env_{[x \mapsto v]} \cup \Env_v}, \forall{} v \in S } \infer1[(ListG)]{\Sem{\([E~|~ x \mbox{~in~} \mathit{PE}, \mathit{GE} \mbox{~where~} G]\)}{\Prog, \Env} \Rightarrow \tuple{\mbox{concat} [ A_v ~|~ v \in S ], \Env \cup \bigcup_{v \in S} \Env_v}} \end{prooftree}