s/constraint/decision/g

tesi/tesi_unicode.org

@@ -888,19 +888,19 @@ expressed in the source language and the other in the target language
   vₛ ≃ vₜ    (TODO define, this talks about the representation of source values in the target)
 
 we can define the equivalence between a couple of programs or a couple
-ofconstraint trees 
+of decision trees 
 | tₛ ≃ tₜ := ∀vₛ≃vₜ, tₛ(vₛ) = tₜ(vₜ)
 | Cₛ ≃ Cₜ := ∀vₛ≃vₜ, Cₛ(vₛ) = Cₜ(vₜ)
 
 The proposed equivalence algorithm that works on a couple of
-constraint trees is returns either /Yes/ or /No(vₛ, vₜ)/ where vₛ and
+decision trees is returns either /Yes/ or /No(vₛ, vₜ)/ where vₛ and
 vₜ are a couple of possible counter examples for which the constraint
 trees produce a different result.
 
 ** Statements
-Theorem. We say that a translation of a source program to a constraint tree
+Theorem. We say that a translation of a source program to a decision tree
 is correct when for every possible input, the source program and its
-respective constraint tree produces the same result
+respective decision tree produces the same result
 
 | ∀vₛ, tₛ(vₛ) = 〚tₛ〛ₛ(vₛ)
 
@@ -915,15 +915,15 @@ equivalent modulo the guards queue, written /r₁ ≃gs r₂/, when:
 
 Definition: we say that Cₜ covers the input space /S/, written
 /covers(Cₜ, S) when every value vₛ∈S is a valid input to the
-constraint tree Cₜ. (TODO: rephrase)
+decision tree Cₜ. (TODO: rephrase)
 
-Theorem: Given an input space /S/ and a couple of constraint trees, where
-the target constraint tree Cₜ covers the input space /S/, we say that
-the two constraint trees are equivalent when:
+Theorem: Given an input space /S/ and a couple of decision trees, where
+the target decision tree Cₜ covers the input space /S/, we say that
+the two decision trees are equivalent when:
 
 | (equiv S Cₛ Cₜ gs = Yes) ∧ covers(Cₜ, S) ⇒ ∀vₛ≃vₜ ∈ S, Cₛ(vₛ) ≃gs Cₜ(vₜ)
 
-Similarly we say that a couple of constraint trees in the presence of
+Similarly we say that a couple of decision trees in the presence of
 an input space /S/ are /not/ equivalent when:
 
 | (equiv S Cₛ Cₜ gs = No(vₛ,vₜ) ∧ covers(Cₜ, S) ⇒ vₛ≃vₜ ∈ S ∧ Cₛ(vₛ) ≠gs Cₜ(vₜ)
@@ -934,7 +934,7 @@ target program we say:
 | (equiv S [|tₛ|]ₛ [|tₜ|]ₜ ∅ = Yes)  ⇔  tₛ ≃ tₜ
 
 
-*** Proof of the correctness of the translation from source programs to source constraint trees
+*** Proof of the correctness of the translation from source programs to source decision trees
 
 We define a source term tₛ as a collection of patterns pointing to blackboxes
 | tₛ ::= (p → bb)^{i∈I}
@@ -943,7 +943,7 @@ A pattern is defined as either a constructor pattern, an or pattern or
 a constant pattern
 | p ::= | K(pᵢ)ⁱ, i ∈ I | (p|q) | n ∈ ℕ
 
-A constraint tree is defined as either a Leaf, a Failure terminal or
+A decision tree is defined as either a Leaf, a Failure terminal or
 an intermediate node with different children sharing the same accessor /a/
 and an optional fallback.
 Failure is emitted only when the patterns don't cover the whole set of
@@ -964,14 +964,14 @@ We define the decomposition matrix /mₛ/ as
 Correggi prendendo in considerazione l'accessor
 \end{comment}
 
-We define the constraint tree of source programs
+We define the decision tree of source programs
   [|tₛ|]
-in terms of the constraint tree of pattern matrices
+in terms of the decision tree of pattern matrices
   [|mₛ|]
 by the following:
   〚((pᵢ → bbᵢ)^{i∈I}〛 := 〚(Root), (pᵢ → bbᵢ)^{i∈I} 〛 # i ∈ I
 
-Constraint tree computed from pattern matrices respect the following invariant:
+decision tree computed from pattern matrices respect the following invariant:
 | ∀v (vᵢ)^{i∈I} = v(aᵢ)^{i∈I} → 〚m〛(v) = m(vᵢ)^{i∈I} for m = ((aᵢ)^{i∈I}, (rᵢ)^{i∈I})
 where 
 | v(Here) = v
@@ -985,7 +985,7 @@ analysys.
 
 Base cases:
 1. [| ∅, (∅ → bbᵢ)ⁱ |] := Leaf bbᵢ where i := min(I), that is a
-   constraint tree [|ms|] defined by an empty accessor and empty
+   decision tree [|ms|] defined by an empty accessor and empty
    patterns pointing to blackboxes /bbᵢ/. This respects the invariant
    because a decomposition matrix in the case of empty rows returns
    the first expression and we known that (Leaf bb)(v) := Match bb
@@ -1003,11 +1003,11 @@ We define
 ** Proof of equivalence checking
 
 The equivalence checking algorithm takes as parameters an input space
-/S/, a source constraint tree /Cₛ/ and a target constraint tree /Cₜ/:
+/S/, a source decision tree /Cₛ/ and a target decision tree /Cₜ/:
 | equiv(S, Cₛ, Cₜ) → Yes | No(vₛ, vₜ)
 
 When the algorithm returns Yes and the input space is covered by /Cₛ/
-we can say that the couple of constraint trees are the same for
+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"
@@ -1015,7 +1015,7 @@ 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ₜ)
 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 constraint trees
+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ₜ)
 
@@ -1043,9 +1043,9 @@ In the other subcases S is always non-empty.
 2. equiv(S, Failure, Failure) := Yes
    the statement holds because of equality between Failure nodes in
    the case of every possible value /v/.
-3. The result of the subcase where we have a source constraint tree
+3. The result of the subcase where we have a source decision tree
    /Cₛ/ that is either a Leaf terminal or a Failure terminal and a
-   target constraint tree defined by an accessor /a/ and a positive
+   target decision tree defined by an accessor /a/ and a positive
    number of couples constraint πᵢ and children nodes Cₜᵢ. The output
    the output of the algorithm is:
    | equiv(S, (Leaf bbₛ|Failure) as Cₛ, Node(a, (πᵢ → Cₜᵢ)ⁱ)) :=  Forall(equiv( S∩a→π(kᵢ)), Cₛ, Cₜᵢ)ⁱ)