diff --git a/tesi/ltximg/org-ltximg_1031ca755ec4bd798a690ed9350f68282bc11561.png b/tesi/ltximg/org-ltximg_1031ca755ec4bd798a690ed9350f68282bc11561.png new file mode 100644 index 0000000..a624488 Binary files /dev/null and b/tesi/ltximg/org-ltximg_1031ca755ec4bd798a690ed9350f68282bc11561.png differ diff --git a/tesi/ltximg/org-ltximg_15cc44285208b6cf43ee96ac8e9f497e5f3191eb.png b/tesi/ltximg/org-ltximg_15cc44285208b6cf43ee96ac8e9f497e5f3191eb.png new file mode 100644 index 0000000..3296a02 Binary files /dev/null and b/tesi/ltximg/org-ltximg_15cc44285208b6cf43ee96ac8e9f497e5f3191eb.png differ diff --git a/tesi/ltximg/org-ltximg_20120fd1e8cd49ab0dab3ef97353929c15f4113a.png b/tesi/ltximg/org-ltximg_20120fd1e8cd49ab0dab3ef97353929c15f4113a.png new file mode 100644 index 0000000..c5b5517 Binary files /dev/null and b/tesi/ltximg/org-ltximg_20120fd1e8cd49ab0dab3ef97353929c15f4113a.png differ diff --git a/tesi/ltximg/org-ltximg_25279e548f036c71f2640c10d3ac4556f571c8a3.png b/tesi/ltximg/org-ltximg_25279e548f036c71f2640c10d3ac4556f571c8a3.png new file mode 100644 index 0000000..4735de9 Binary files /dev/null and b/tesi/ltximg/org-ltximg_25279e548f036c71f2640c10d3ac4556f571c8a3.png differ diff --git a/tesi/ltximg/org-ltximg_38b96ab92fcbc42081a14294cafc9655d64124a1.png b/tesi/ltximg/org-ltximg_38b96ab92fcbc42081a14294cafc9655d64124a1.png new file mode 100644 index 0000000..0a775cc Binary files /dev/null and b/tesi/ltximg/org-ltximg_38b96ab92fcbc42081a14294cafc9655d64124a1.png differ diff --git a/tesi/ltximg/org-ltximg_41cddde4a95b736a274897266cb27c5b8a348b6f.png b/tesi/ltximg/org-ltximg_41cddde4a95b736a274897266cb27c5b8a348b6f.png new file mode 100644 index 0000000..aa26fbb Binary files /dev/null and b/tesi/ltximg/org-ltximg_41cddde4a95b736a274897266cb27c5b8a348b6f.png differ diff --git a/tesi/ltximg/org-ltximg_5c6a52e070f6e7a9d353e2fb281d3431b02bdb3c.png b/tesi/ltximg/org-ltximg_5c6a52e070f6e7a9d353e2fb281d3431b02bdb3c.png new file mode 100644 index 0000000..a624488 Binary files /dev/null and b/tesi/ltximg/org-ltximg_5c6a52e070f6e7a9d353e2fb281d3431b02bdb3c.png differ diff --git a/tesi/ltximg/org-ltximg_72f6cd40efd8589318c49e230274945c079c4ca8.png b/tesi/ltximg/org-ltximg_72f6cd40efd8589318c49e230274945c079c4ca8.png new file mode 100644 index 0000000..79c1301 Binary files /dev/null and b/tesi/ltximg/org-ltximg_72f6cd40efd8589318c49e230274945c079c4ca8.png differ diff --git a/tesi/ltximg/org-ltximg_8c2675337cc8345e6e71ecbfd98a2bd044cb53a2.png b/tesi/ltximg/org-ltximg_8c2675337cc8345e6e71ecbfd98a2bd044cb53a2.png new file mode 100644 index 0000000..ebbd81e Binary files /dev/null and b/tesi/ltximg/org-ltximg_8c2675337cc8345e6e71ecbfd98a2bd044cb53a2.png differ diff --git a/tesi/ltximg/org-ltximg_8e82b4110fb7414eb8af69a9211cfb2808fe4dd5.png b/tesi/ltximg/org-ltximg_8e82b4110fb7414eb8af69a9211cfb2808fe4dd5.png new file mode 100644 index 0000000..433abb1 Binary files /dev/null and b/tesi/ltximg/org-ltximg_8e82b4110fb7414eb8af69a9211cfb2808fe4dd5.png differ diff --git a/tesi/ltximg/org-ltximg_96705f10cbe564234adb81cafa072109c3faf2f5.png b/tesi/ltximg/org-ltximg_96705f10cbe564234adb81cafa072109c3faf2f5.png new file mode 100644 index 0000000..f96dbdf Binary files /dev/null and b/tesi/ltximg/org-ltximg_96705f10cbe564234adb81cafa072109c3faf2f5.png differ diff --git a/tesi/ltximg/org-ltximg_a07c518e2def2cbaf55d84c945bd0b86d59e7037.png b/tesi/ltximg/org-ltximg_a07c518e2def2cbaf55d84c945bd0b86d59e7037.png new file mode 100644 index 0000000..7875155 Binary files /dev/null and b/tesi/ltximg/org-ltximg_a07c518e2def2cbaf55d84c945bd0b86d59e7037.png differ diff --git a/tesi/ltximg/org-ltximg_a4786361c751a1a74c01c332e65e4854d7be80e6.png b/tesi/ltximg/org-ltximg_a4786361c751a1a74c01c332e65e4854d7be80e6.png new file mode 100644 index 0000000..c433d52 Binary files /dev/null and b/tesi/ltximg/org-ltximg_a4786361c751a1a74c01c332e65e4854d7be80e6.png differ diff --git a/tesi/ltximg/org-ltximg_bea68b35299cd5b8f2f8555b5b61d0f0803f6778.png b/tesi/ltximg/org-ltximg_bea68b35299cd5b8f2f8555b5b61d0f0803f6778.png new file mode 100644 index 0000000..bfd72f3 Binary files /dev/null and b/tesi/ltximg/org-ltximg_bea68b35299cd5b8f2f8555b5b61d0f0803f6778.png differ diff --git a/tesi/ltximg/org-ltximg_c356f2a20f6be4475ef3496e1a2eb5e99cd0c727.png b/tesi/ltximg/org-ltximg_c356f2a20f6be4475ef3496e1a2eb5e99cd0c727.png new file mode 100644 index 0000000..46b742c Binary files /dev/null and b/tesi/ltximg/org-ltximg_c356f2a20f6be4475ef3496e1a2eb5e99cd0c727.png differ diff --git a/tesi/ltximg/org-ltximg_ca02030f255196914ab3a21c0b5eb83072e92d47.png b/tesi/ltximg/org-ltximg_ca02030f255196914ab3a21c0b5eb83072e92d47.png new file mode 100644 index 0000000..24ab601 Binary files /dev/null and b/tesi/ltximg/org-ltximg_ca02030f255196914ab3a21c0b5eb83072e92d47.png differ diff --git a/tesi/ltximg/org-ltximg_cc429dea9befffee656ac9fc36b1df8509d3c7ff.png b/tesi/ltximg/org-ltximg_cc429dea9befffee656ac9fc36b1df8509d3c7ff.png new file mode 100644 index 0000000..019d01b Binary files /dev/null and b/tesi/ltximg/org-ltximg_cc429dea9befffee656ac9fc36b1df8509d3c7ff.png differ diff --git a/tesi/ltximg/org-ltximg_d3116a10855bae8a6d0cb304a27220822ddaedb4.png b/tesi/ltximg/org-ltximg_d3116a10855bae8a6d0cb304a27220822ddaedb4.png new file mode 100644 index 0000000..0027ad4 Binary files /dev/null and b/tesi/ltximg/org-ltximg_d3116a10855bae8a6d0cb304a27220822ddaedb4.png differ diff --git a/tesi/ltximg/org-ltximg_ee449751cf9a5061cafa5f18d30c08dbe8c20a11.png b/tesi/ltximg/org-ltximg_ee449751cf9a5061cafa5f18d30c08dbe8c20a11.png new file mode 100644 index 0000000..aa26fbb Binary files /dev/null and b/tesi/ltximg/org-ltximg_ee449751cf9a5061cafa5f18d30c08dbe8c20a11.png differ diff --git a/tesi/ltximg/org-ltximg_f243bcd039f21e4dbb99e46d60f3f9cf9f5c1311.png b/tesi/ltximg/org-ltximg_f243bcd039f21e4dbb99e46d60f3f9cf9f5c1311.png new file mode 100644 index 0000000..b05f23b Binary files /dev/null and b/tesi/ltximg/org-ltximg_f243bcd039f21e4dbb99e46d60f3f9cf9f5c1311.png differ diff --git a/tesi/tesi_unicode.org b/tesi/tesi_unicode.org index c44dfc9..1e8ca0d 100644 --- a/tesi/tesi_unicode.org +++ b/tesi/tesi_unicode.org @@ -1879,7 +1879,7 @@ for content equality. {\EquivTEX S \Failure \Failure \emptyqueue} \\ \infer - {\trel {t_S} {t_T}} + {\progrel {t_S} {t_T}} {\EquivTEX S {\Leaf {t_S}} {\Leaf {t_T}} \emptyqueue} \end{mathpar} @@ -1966,24 +1966,24 @@ is empty. {D_S} {\Guard {e_T} {D_0} {D_1}} {(e_S = b), G}} \end{mathpar} -Our equivalence-checking algorithm $\EquivTEX S {C_S} {C_T} G$ is +Our equivalence-checking algorithm is a exactly decision procedure for the provability of the judgment -$(\EquivTEX S {C_S} {C_T} G)$, defined by the previous inference rules. +$\EquivTEX S {C_S} {C_T}$, defined by the previous inference rules. Running a program tₛ or its translation 〚tₛ〛 against an input vₛ produces as a result /r/ in the following way: -| ( 〚tₛ〛ₛ(vₛ) ≡ Cₛ(vₛ) ) → r +| ( 〚tₛ〛ₛ(vₛ) ≡ Dₛ(vₛ) ) → r | tₛ(vₛ) → r Likewise -| ( 〚tₜ〛ₜ(vₜ) ≡ Cₜ(vₜ) ) → r +| ( 〚tₜ〛ₜ(vₜ) ≡ Dₜ(vₜ) ) → r | tₜ(vₜ) → r | result r ::= guard list * (Match blackbox \vert{} NoMatch \vert{} Absurd) | guard ::= blackbox. Having defined equivalence between two inputs of which one is expressed in the source language and the other in the target language, -vₛ ≃ vₜ, we can define the equivalence between a couple of programs or +$\vrel {v_S} {v_T}$, we can define the equivalence between a couple of programs or a couple of decision trees -| tₛ ≃ tₜ := ∀vₛ≃vₜ, tₛ(vₛ) = tₜ(vₜ) -| Cₛ ≃ Cₜ := ∀vₛ≃vₜ, Cₛ(vₛ) = Cₜ(vₜ) +| $\progrel {t_S} {t_T} := \forall \vrel {v_S} {v_T}, t_S(v_S) = t_T(v_T)$ +| $D_S \approx D_T := \forall \vrel {v_S} {v_T}, D_S(v_S) = D_T(v_T)$ The result of the proposed equivalence algorithm is /Yes/ or /No(vₛ, vₜ)/. In particular, in the negative case, vₛ and vₜ are a couple of possible counter examples for which the decision trees produce a @@ -1991,19 +1991,19 @@ different result. \\ In the presence of guards we can say that two results are equivalent modulo the guards queue, written /r₁ ≃gs r₂/, when: -| (gs₁, r₁) ≃gs (gs₂, r₂) ⇔ (gs₁, r₁) = (gs₂ ++ gs, r₂) -We say that Cₜ covers the input space /S/, written -/covers(Cₜ, S)/ when every value vₛ∈S is a valid input to the -decision tree Cₜ. (TODO: rephrase) +| (gs₁, r₁) ≃_{gs} (gs₂, r₂) ⇔ (gs₁, r₁) = (gs₂ +++ gs, r₂) +We say that Dₜ covers the input space /S/, written +/covers(Dₜ, S)/ when every value vₛ∈S is a valid input to the +decision tree Dₜ. (TODO: rephrase) Given an input space /S/ and a couple of decision trees, where -the target decision tree Cₜ covers the input space /S/ we can define equivalence: -| equiv(S, Cₛ, Cₜ, gs) = Yes ∧ covers(Cₜ, S) → ∀vₛ≃vₜ ∈ S, Cₛ(vₛ) ≃gs Cₜ(vₜ) +the target decision tree Dₜ covers the input space /S/ we can define equivalence: +| $equiv(S, C_S, C_T, gs) = Yes \wedge covers(C_T, S) \to \forall \vrel {v_S} {v_T} \in S, C_S(v_S) \simeq_{gs} C_T(v_T)$ Similarly we say that a couple of decision trees in the presence of an input space /S/ are /not/ equivalent in the following way: -| equiv(S, Cₛ, Cₜ, gs) = No(vₛ,vₜ) ∧ covers(Cₜ, S) → vₛ≃vₜ ∈ S ∧ Cₛ(vₛ) ≠gs Cₜ(vₜ) +| $equiv(S, C_S, C_T, gs) = No(v_S, v_T) \wedge covers(C_T, S) \to \vrel {v_S} {v_T} \in S \wedge C_S(v_S) \ne_{gs} C_T(v_T)$ Corollary: For a full input space /S/, that is the universe of the target program: -| equiv(S, 〚tₛ〛ₛ, 〚tₜ〛ₜ, ∅) = Yes ⇔ tₛ ≃ tₜ +| $equiv(S, \llbracket t_S \rrbracket{_S}, \llbracket t_T \rrbracket{_T}, \emptyset) = Yes \Leftrightarrow \progrel {t_S} {t_T}$ \begin{comment} @@ -2012,35 +2012,35 @@ TODO: put ^i∈I where needed \subsubsection{The trimming lemma} The trimming lemma allows to reduce the size of a decision tree given an accessor /a/ → π relation (TODO: expand) -| ∀vₜ ∈ (a→π), Cₜ(vₜ) = C_{t/a→π}(vₜ) +| ∀vₜ ∈ (a→π), Dₜ(vₜ) = D_{t/a→π}(vₜ) We prove this by induction on Cₜ: -- Cₜ = Leaf_{bb}: when the decision tree is a leaf terminal, the result of trimming on a Leaf is the Leaf itself +- Dₜ = Leaf_{bb}: when the decision tree is a leaf terminal, the result of trimming on a Leaf is the Leaf itself | Leaf_{bb/a→π}(v) = Leaf_{bb}(v) - The same applies to Failure terminal | Failure_{/a→π}(v) = Failure(v) -- When Cₜ = Switch(b, (π→Cᵢ)ⁱ)_{/a→π} then we look at the accessor - /a/ of the subtree Cᵢ and we define πᵢ' = πᵢ if a≠b else πᵢ∩π Trimming +- When Dₜ = Switch(b, (π→Dᵢ)ⁱ)_{/a→π} then we look at the accessor + /a/ of the subtree Dᵢ and we define πᵢ' = πᵢ if a≠b else πᵢ∩π Trimming a switch node yields the following result: - | Switch(b, (π→Cᵢ)^{i∈I})_{/a→π} := Switch(b, (π'ᵢ→C_{i/a→π})^{i∈I}) + | Switch(b, (π→Dᵢ)^{i∈I})_{/a→π} := Switch(b, (π'ᵢ→D_{i/a→π})^{i∈I}) \begin{comment} TODO: understand how to properly align lists check that every list is aligned \end{comment} For the trimming lemma we have to prove that running the value vₜ against -the decision tree Cₜ is the same as running vₜ against the tree -C_{trim} that is the result of the trimming operation on Cₜ -| Cₜ(vₜ) = C_{trim}(vₜ) = Switch(b, (πᵢ'→C_{i/a→π})^{i∈I})(vₜ) +the decision tree Dₜ is the same as running vₜ against the tree +D_{trim} that is the result of the trimming operation on Dₜ +| Dₜ(vₜ) = D_{trim}(vₜ) = Switch(b, (πᵢ'→D_{i/a→π})^{i∈I})(vₜ) We can reason by first noting that when vₜ∉(b→πᵢ)ⁱ the node must be a Failure node. In the case where ∃k \vert{} vₜ∈(b→πₖ) then we can prove that -| C_{k/a→π}(vₜ) = Switch(b, (πᵢ'→C_{i/a→π})^{i∈I})(vₜ) +| D_{k/a→π}(vₜ) = Switch(b, (πᵢ'→D_{i/a→π})^{i∈I})(vₜ) because when a ≠ b then πₖ'= πₖ and this means that vₜ∈πₖ' while when a = b then πₖ'=(πₖ∩π) and vₜ∈πₖ' because: - by the hypothesis, vₜ∈π - we are in the case where vₜ∈πₖ So vₜ ∈ πₖ' and by induction -| Cₖ(vₜ) = C_{k/a→π}(vₜ) -We also know that ∀vₜ∈(b→πₖ) → Cₜ(vₜ) = Cₖ(vₜ) +| Dₖ(vₜ) = D_{k/a→π}(vₜ) +We also know that ∀vₜ∈(b→πₖ) → Dₜ(vₜ) = Dₖ(vₜ) By putting together the last two steps, we have proven the trimming lemma. @@ -2056,21 +2056,21 @@ Covering lemma: \subsubsection{Equivalence checking} The equivalence checking algorithm takes as parameters an input space -/S/, a source decision tree /Cₛ/ and a target decision tree /Cₜ/: -| equiv(S, Cₛ, Cₜ) → Yes \vert{} No(vₛ, vₜ) +/S/, a source decision tree /Dₛ/ and a target decision tree /Dₜ/: +| equiv(S, Dₛ, Dₜ) → Yes \vert{} No(vₛ, vₜ) \\ -When the algorithm returns Yes and the input space is covered by /Cₛ/ +When the algorithm returns Yes and the input space is covered by /Dₛ/ we can say that the couple of decision trees are the same for every couple of source value /vₛ/ and target value /vₜ/ that are equivalent. \begin{comment} Define "covered" Is it correct to say the same? How to correctly distinguish in words ≃ and = ? \end{comment} -| equiv(S, Cₛ, Cₜ) = Yes and cover(Cₜ, S) → ∀ vₛ ≃ vₜ∈S ∧ Cₛ(vₛ) = Cₜ(vₜ) +| equiv(S, Dₛ, Dₜ) = Yes and cover(Dₜ, S) → ∀ vₛ ≃ vₜ∈S ∧ Dₛ(vₛ) = Dₜ(vₜ) In the case where the algorithm returns No we have at least a couple of counter example values vₛ and vₜ for which the two decision trees outputs a different result. -| equiv(S, Cₛ, Cₜ) = No(vₛ,vₜ) and cover(Cₜ, S) → ∀ vₛ ≃ vₜ∈S ∧ Cₛ(vₛ) ≠ Cₜ(vₜ) +| equiv(S, Dₛ, Cₜ) = No(vₛ,vₜ) and cover(Dₜ, S) → ∀ vₛ ≃ vₜ∈S ∧ Dₛ(vₛ) ≠ Dₜ(vₜ) We define the following | Forall(Yes) = Yes | Forall(Yes::l) = Forall(l) @@ -2092,9 +2092,9 @@ I start numbering from zero to leave the numbers as they were on the blackboard, I think the unreachable case should go at the end. \end{comment} 0. in case of unreachable: -| Cₛ(vₛ) = Absurd(Unreachable) ≠ Cₜ(vₜ) ∀vₛ,vₜ +| Dₛ(vₛ) = Absurd(Unreachable) ≠ Dₜ(vₜ) ∀vₛ,vₜ 1. In the case of an empty input space - | equiv(∅, Cₛ, Cₜ) := Yes + | equiv(∅, Dₛ, Dₜ) := Yes and that is trivial to prove because there is no pair of values (vₛ, vₜ) that could be tested against the decision trees. In the other subcases S is always non-empty. @@ -2102,48 +2102,46 @@ I think the unreachable case should go at the end. |equiv(S, Failure, Failure) := Yes Given that ∀v, Failure(v) = Failure, the statement holds. 3. When we have a Leaf or a Failure at the left side: - | equiv(S, Failure as Cₛ, Switch(a, (πᵢ → Cₜᵢ)^{i∈I})) := Forall(equiv( S∩a→π(kᵢ)), Cₛ, Cₜᵢ)^{i∈I}) - | equiv(S, Leaf bbₛ as Cₛ, Switch(a, (πᵢ → Cₜᵢ)^{i∈I})) := Forall(equiv( S∩a→π(kᵢ)), Cₛ, Cₜᵢ)^{i∈I}) + | equiv(S, Failure as Dₛ, Switch(a, (πᵢ → Dₜᵢ)^{i∈I})) := Forall(equiv( S∩a→π(kᵢ)), Dₛ, Dₜᵢ)^{i∈I}) + | equiv(S, Leaf bbₛ as Dₛ, Switch(a, (πᵢ → Dₜᵢ)^{i∈I})) := Forall(equiv( S∩a→π(kᵢ)), Dₛ, Dₜᵢ)^{i∈I}) Our algorithm either returns Yes for every sub-input space Sᵢ := S∩(a→π(kᵢ)) and subtree Cₜᵢ - | equiv(Sᵢ, Cₛ, Cₜᵢ) = Yes ∀i - or we have a counter example vₛ, vₜ for which - | vₛ≃vₜ∈Sₖ ∧ cₛ(vₛ) ≠ Cₜₖ(vₜ) - then because - | vₜ∈(a→πₖ) → Cₜ(vₜ) = Cₜₖ(vₜ) , - | vₛ≃vₜ∈S ∧ Cₛ(vₛ)≠Cₜ(vₜ) - we can say that + | equiv(Sᵢ, Dₛ, Dₜᵢ) = Yes ∀i + or we have a counter example v_S, v_T for which + | $\vrel {v_S} {v_T \in S_k} \wedge D_S(v_S) \ne D_{Tk}(v_T)$ + then because $v_T \in (a \to \pi_k) \to D_T(v_T) = D_{Tk}(v_T)$ and $\vrel v_S {v_T \in S} \wedge D_S(v_S) \ne D_T(v_T)$ we can say that | equiv(Sᵢ, Cₛ, Cₜᵢ) = No(vₛ, vₜ) for some minimal k∈I 4. When we have a Switch on the right we define π_{fallback} as the domain of values not covered but the union of the constructors kᵢ | $\pi_{fallback} = \neg\bigcup\limits_{i\in I}\pi(k_i)$ Our algorithm proceeds by trimming - | equiv(S, Switch(a, (kᵢ → Cₛᵢ)^{i∈I}, C_{sf}), Cₜ) := - | Forall(equiv( S∩(a→π(kᵢ)^{i∈I}), Cₛᵢ, C_{t/a→π(kᵢ)})^{i∈I} +++ equiv(S∩(a→πₙ), Cₛ, C_{a→π_{fallback}})) + | equiv(S, Switch(a, (kᵢ → Dₛᵢ)^{i∈I}, D_{sf}), Dₜ) := + | Forall(equiv( S∩(a→π(kᵢ)^{i∈I}), Dₛᵢ, D_{t/a→π(kᵢ)})^{i∈I} +++ equiv(S∩(a→πₙ), Dₛ, D_{a→π_{fallback}})) The statement still holds and we show this by first analyzing the /Yes/ case: - | Forall(equiv( S∩(a→π(kᵢ)^{i∈I}), Cₛᵢ, C_{t/a→π(kᵢ)})^{i∈I} = Yes + | Forall(equiv( S∩(a→π(kᵢ)^{i∈I}), Dₛᵢ, D_{t/a→π(kᵢ)})^{i∈I} = Yes The constructor k is either included in the set of constructors kᵢ: - | k \vert k∈(kᵢ)ⁱ ∧ Cₛ(vₛ) = Cₛᵢ(vₛ) + | k \vert k∈(kᵢ)ⁱ ∧ Dₛ(vₛ) = Dₛᵢ(vₛ) We also know that - | (1) Cₛᵢ(vₛ) = C_{t/a→πᵢ}(vₜ) - | (2) C_{T/a→πᵢ}(vₜ) = Cₜ(vₜ) + | (1) Dₛᵢ(vₛ) = D_{t/a→πᵢ}(vₜ) + | (2) D_{T/a→πᵢ}(vₜ) = Dₜ(vₜ) (1) is true by induction and (2) is a consequence of the trimming lemma. Putting everything together: - | Cₛ(vₛ) = Cₛᵢ(vₛ) = C_{T/a→πᵢ}(vₜ) = Cₜ(vₜ) + | Dₛ(vₛ) = Dₛᵢ(vₛ) = D_{T/a→πᵢ}(vₜ) = Dₜ(vₜ) When the k∉(kᵢ)ⁱ [TODO] The auxiliary Forall function returns /No(vₛ, vₜ)/ when, for a minimum k, - | equiv(Sₖ, Cₛₖ, C_{T/a→πₖ} = No(vₛ, vₜ) + | equiv(Sₖ, Dₛₖ, D_{T/a→πₖ} = No(vₛ, vₜ) Then we can say that - | Cₛₖ(vₛ) ≠ C_{t/a→πₖ}(vₜ) + | Dₛₖ(vₛ) ≠ D_{t/a→πₖ}(vₜ) that is enough for proving that - | Cₛₖ(vₛ) ≠ (C_{t/a→πₖ}(vₜ) = Cₜ(vₜ)) + | Dₛₖ(vₛ) ≠ (D_{t/a→πₖ}(vₜ) = Dₜ(vₜ)) * Examples In this section we discuss some examples given as input and output of -the prototype tool. +the prototype tool. Source and target files are taken from the +internship git repository\cite{internship}. ;; include_file example0.ml We can see from this first source file the usage of the /observe/ @@ -2154,6 +2152,23 @@ The prototype tool states that the compilation was successful and the two programs are equivalent. ;; include_file example0.trace +The following example shows how the prototype handles ADT. +;; include_file example3.ml +;; include_file example3.lambda +;; include_file example3.trace +This trivial pattern matching code shows how guards are handled. +;; include_file guards2.ml +;; include_file guards2.lambda +;; include_file guards2.trace +The following source code shows the usage of the OCaml refutation +clause. +;; include_file example9.ml +;; include_file example9.lambda +;; include_file example9.trace +In this example the tool correctly handles /Failure/ nodes on both decision trees. +;; include_file example9bis.ml +;; include_file example9bis.lambda +;; include_file example9bis.trace \begin{thebibliography}{9} \bibitem{cpp_pat} @@ -2240,4 +2255,8 @@ https://github.com/janestreet/ocaml-compiler-libs \bibitem{menhir} Régis-Gianas, François Pottier Yann. \textit{Menhir Reference Manual}. + +\bibitem{internship} +https://github.com/FraMecca/inria-internship + \end{thebibliography} diff --git a/tesi/traces/example0.trace b/tesi/traces/example0.trace index 1f0d6da..cd860ae 100644 --- a/tesi/traces/example0.trace +++ b/tesi/traces/example0.trace @@ -1,4 +1,4 @@ -Target program constraint tree +Target program decision tree Switch ({ var=AcAdd(-2 AcRoot=param/82); dom=Int [-inf; -1] [3; +inf] v Tag _; }) = Leaf=VConstant:5 Switch ({ var=AcAdd(-2 AcRoot=param/82); dom=Int [0; 2]; }) = @@ -12,7 +12,7 @@ Switch ({ var=AcAdd(-2 AcRoot=param/82); dom=Int [0; 2]; }) = Fallback=None -Source program constraint tree +Source program decision tree Switch AcRoot:{ Int 3 -> Leaf='Int 3 ' diff --git a/tesi/traces/example3.lambda b/tesi/traces/example3.lambda new file mode 100644 index 0000000..fee7a34 --- /dev/null +++ b/tesi/traces/example3.lambda @@ -0,0 +1,18 @@ +(setglobal Example3! + (let + (a/85 = + (function t/86 + (switch* t/86 + case int 0: (observe 3) + case tag 0: + (let (*match*/90 =a (field 0 t/86)) + (catch + (if (!= *match*/90 1) + (if (!= *match*/90 2) (exit 1) (apply (observe 1) 2)) + (apply (observe 1) 1)) + with (1) (apply (observe 1) 0a))) + case tag 1: + (let (*match*/91 =a (field 0 t/86)) + (if (!= *match*/91 0) (apply (observe 2) 1a) + (apply (observe 2) 0a)))))) + (makeblock 0 a/85))) diff --git a/tesi/traces/example3.ml b/tesi/traces/example3.ml new file mode 100644 index 0000000..63dbca1 --- /dev/null +++ b/tesi/traces/example3.ml @@ -0,0 +1,11 @@ +external observe : 'a -> 'b = "observe" + +type t = K1 of int | K2 of bool | K3 + +let a = fun t -> match t with + | K1 1 -> observe 1 1 + | K1 2 -> observe 1 2 + | K1 _ -> observe 1 () + | K2 true -> observe 2 true + | K2 false -> observe 2 false + | K3 -> observe 3 diff --git a/tesi/traces/example3.trace b/tesi/traces/example3.trace new file mode 100644 index 0000000..3a177bc --- /dev/null +++ b/tesi/traces/example3.trace @@ -0,0 +1,46 @@ +Target program decision tree +Switch ({ var=AcRoot=t/86; dom=Int 0; }) = + Leaf=VConstant:3 +Switch ({ var=AcRoot=t/86; dom=Tag 0; }) = + Switch ({ var=AcField(0 AcRoot=t/86); dom=Int [-inf; 0] [2; +inf] v Tag _; }) = + Switch ({ var=AcField(0 AcRoot=t/86); dom=Int [-inf; 1] [3; +inf] v Tag _; }) = + Leaf=VConstant:1, VConstant:0 + Switch ({ var=AcField(0 AcRoot=t/86); dom=Int 2; }) = + Leaf=VConstant:1, VConstant:2 + Fallback=None + Switch ({ var=AcField(0 AcRoot=t/86); dom=Int 1; }) = + Leaf=VConstant:1, VConstant:1 + Fallback=None +Switch ({ var=AcRoot=t/86; dom=Tag 1; }) = + Switch ({ var=AcField(0 AcRoot=t/86); dom=Int [-inf; -1] [1; +inf] v Tag _; }) = + Leaf=VConstant:2, VConstant:1 + Switch ({ var=AcField(0 AcRoot=t/86); dom=Int 0; }) = + Leaf=VConstant:2, VConstant:0 + Fallback=None +Fallback=None + +Source program decision tree +Switch AcRoot:{ + Variant K2 -> + Switch AcRoot.0:{ + Bool false -> + Leaf='Int 2 Bool false ' + + Bool true -> + Leaf='Int 2 Bool true ' + } Fallback: Unreachable + + Variant K1 -> + Switch AcRoot.0:{ + Int 2 -> + Leaf='Int 1 Int 2 ' + + Int 1 -> + Leaf='Int 1 Int 1 ' + } Fallback: Leaf='Int 1 Unit ' + + Variant K3 -> + Leaf='Int 3 ' +} Fallback: Unreachable + +The two programs are equivalent. \ No newline at end of file diff --git a/tesi/traces/example6.lambda b/tesi/traces/example6.lambda new file mode 100644 index 0000000..ce901f5 --- /dev/null +++ b/tesi/traces/example6.lambda @@ -0,0 +1,70 @@ +(setglobal Example6! + (let + (mm/81 = + (function x/89 + (catch + (if x/89 + (let (*match*/92 =a (field 0 x/89)) + (if *match*/92 + (let + (x/83 =a (field 0 *match*/92) + x/86 =a (field 0 x/83) + *match*/93 =a (field 0 x/86)) + (catch + (if (!= *match*/93 1) (exit 2) + (let (*match*/94 =a (field 1 x/86)) + (if (!= *match*/94 2) (exit 2) + (let (x/82 =a (field 1 x/83)) + (catch + (if (!= x/82 2) (exit 3) + (let (*match*/95 =a (field 1 *match*/92)) + (if *match*/95 (exit 1) + (let (*match*/96 =a (field 1 x/89)) + (catch + (if *match*/96 (exit 4) + (observe + [0: [0: [0: [0: 1 2] 2] 0a] 0a])) + with (4) + (observe [0: [0: [0: 1 2] 2] 0a])))))) + with (3) + (let (*match*/97 =a (field 1 *match*/92)) + (if *match*/97 (exit 1) + (let (*match*/98 =a (field 1 x/89)) + (observe + (makeblock 0 + (makeblock 0 (*,int) [0: 1 2] x/82) + 0a)))))))))) + with (2) + (let (*match*/100 =a (field 1 *match*/92)) + (if *match*/100 (exit 1) + (let + (z/88 =a (field 1 x/89) + y/87 =a (field 1 x/83) + *match*/99 =a (field 1 x/86)) + (catch + (if z/88 + (let (*match*/101 =a (field 0 z/88)) + (if *match*/101 + (let + (*match*/102 =a (field 1 *match*/101)) + (if *match*/102 (exit 5) + (let (*match*/103 =a (field 1 z/88)) + (if *match*/103 (exit 5) + (let + (x/84 =a x/83 + y/85 =a (field 0 *match*/101)) + (observe + (makeblock 0 + (makeblock 0 x/84 y/85) 0a))))))) + (exit 5))) + (observe (makeblock 0 x/83 0a))) + with (5) + (observe + (makeblock 0 + (makeblock 0 (makeblock 0 (*,int) x/86 y/87) + z/88) + 0a)))))))) + (exit 1))) + (exit 1)) + with (1) (observe x/89)))) + (makeblock 0 mm/81))) diff --git a/tesi/traces/example6.ml b/tesi/traces/example6.ml new file mode 100644 index 0000000..6044120 --- /dev/null +++ b/tesi/traces/example6.ml @@ -0,0 +1,11 @@ +[@@@warning "-20"] +external observe : 'a -> 'b = "observe" + +let mm = function + | [(1, 2), 2]::[] -> observe ([(1, 2), 2]::[]) + | [(1, 2), 2]::_ -> observe [(1, 2), 2] + | [(1, 2), x]::_ -> observe [(1, 2), x] + | [x]::[] -> observe [x] + | [x]::[y]::[] -> observe [x, y] + | [x, y]::z -> observe [(x, y), z] + | x -> observe x diff --git a/tesi/traces/example9.lambda b/tesi/traces/example9.lambda new file mode 100644 index 0000000..96c593c --- /dev/null +++ b/tesi/traces/example9.lambda @@ -0,0 +1,5 @@ +(setglobal Example9! + (let + (test/81 = + (function param/82 (if (!= param/82 0) (observe 0) (observe 1)))) + (makeblock 0 test/81))) diff --git a/tesi/traces/example9.ml b/tesi/traces/example9.ml new file mode 100644 index 0000000..7b163ea --- /dev/null +++ b/tesi/traces/example9.ml @@ -0,0 +1,9 @@ +[@@@warning "-20"] +external observe : 'a -> 'b = "observe" + +let test = function + | true -> observe 0 + | false -> observe 1 + | _ -> . + (* Unreachable; if this annotation was incorrect, + the OCaml compiler would error at pattern-checking-time *) diff --git a/tesi/traces/example9.trace b/tesi/traces/example9.trace new file mode 100644 index 0000000..78619ed --- /dev/null +++ b/tesi/traces/example9.trace @@ -0,0 +1,18 @@ +Target program decision tree +Switch ({ var=AcRoot=param/82; dom=Int [-inf; -1] [1; +inf] v Tag _; }) = + Leaf=VConstant:0 +Switch ({ var=AcRoot=param/82; dom=Int 0; }) = + Leaf=VConstant:1 +Fallback=None + + +Source program decision tree +Switch AcRoot:{ + Bool false -> + Leaf='Int 1 ' + + Bool true -> + Leaf='Int 0 ' +} Fallback: Unreachable + +The two programs are equivalent. \ No newline at end of file diff --git a/tesi/traces/example9bis.lambda b/tesi/traces/example9bis.lambda new file mode 100644 index 0000000..5203342 --- /dev/null +++ b/tesi/traces/example9bis.lambda @@ -0,0 +1,9 @@ +(setglobal Example9bis! + (let + (test/81 = + (function param/82 + (catch (if (!= param/82 0) (observe 0) (exit 1)) with (1) + (raise + (makeblock 0 (global Match_failure/18!) + [0: "example9bis.ml" 4 11]))))) + (makeblock 0 test/81))) diff --git a/tesi/traces/example9bis.ml b/tesi/traces/example9bis.ml new file mode 100644 index 0000000..adf0901 --- /dev/null +++ b/tesi/traces/example9bis.ml @@ -0,0 +1,6 @@ +[@@@warning "-20"] +external observe : 'a -> 'b = "observe" + +let test = function + | true -> observe 0 + (* we expect a Match_failure node for 'false' in the lambda representation *) diff --git a/tesi/traces/example9bis.trace b/tesi/traces/example9bis.trace new file mode 100644 index 0000000..7afb94d --- /dev/null +++ b/tesi/traces/example9bis.trace @@ -0,0 +1,15 @@ +Target program decision tree +Switch ({ var=AcRoot=param/82; dom=Int [-inf; -1] [1; +inf] v Tag _; }) = + Leaf=VConstant:0 +Switch ({ var=AcRoot=param/82; dom=Int 0; }) = + Failure + Fallback=None + + +Source program decision tree +Switch AcRoot:{ + Bool true -> + Leaf='Int 0 ' +} Fallback: Failure + +The two programs are equivalent. diff --git a/tesi/traces/guards2.lambda b/tesi/traces/guards2.lambda new file mode 100644 index 0000000..2436972 --- /dev/null +++ b/tesi/traces/guards2.lambda @@ -0,0 +1,7 @@ +(setglobal Guards2! + (let + (ff/82 = + (function x/83 + (if (guard 0a) (observe 1) + (if (guard 1) (observe 2) (observe 3))))) + (makeblock 0 ff/82))) diff --git a/tesi/traces/guards2.ml b/tesi/traces/guards2.ml new file mode 100644 index 0000000..452e39e --- /dev/null +++ b/tesi/traces/guards2.ml @@ -0,0 +1,8 @@ +[@@@warning "-20"] +external observe : 'a -> 'b = "observe" +external guard : 'a -> 'b = "guard" + +let ff = function + | x when guard () -> observe 1 + | _ when guard 1 -> observe 2 + | _ -> observe 3 diff --git a/tesi/traces/guards2.trace b/tesi/traces/guards2.trace new file mode 100644 index 0000000..6b774fa --- /dev/null +++ b/tesi/traces/guards2.trace @@ -0,0 +1,24 @@ +Target program decision tree +Guard (VConstant:0): +guard(true) = + Leaf=VConstant:1 +guard(false) = + Guard (VConstant:1): + guard(true) = + Leaf=VConstant:2 + guard(false) = + Leaf=VConstant:3 + +Source program decision tree +Switch AcRoot:{ +} Fallback: Guard (Unit ) = + guard(true) = + Leaf='Int 1 ' + guard(false) = + Guard (Int 1 ) = + guard(true) = + Leaf='Int 2 ' + guard(false) = + Leaf='Int 3 ' + +The two programs are equivalent.