bparodi/UniTO
1
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

latex symbols and python

Browse source
This commit is contained in:
Francesco Mecca 2020-04-02 14:14:39 +02:00
parent af1e069b6c
commit b433663bdd
3 changed files with 12 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
tesi/conv.py
View file

@ -3,10 +3,12 @@ import re
from sys import argv from sys import argv
allsymbols = json.load(open('./unicode-latex.json')) allsymbols = json.load(open('./unicode-latex.json'))
mysymbols = ['≡', '≠', '≼', '→', '←', '⊀', '⋠', '≺', '∀', '∈', 'ε','₀', '₂', '₁', '₃', 'ₐ', 'ₖ', 'ₘ', 'ₙ', 'ᵢ', 'ⁱ', '⋮'] mysymbols = ['≡', '≠', '≼', '→', '←', '⊀', '⋠', '≺', '∀', '∈', 'ε','₀', '₂', '₁', '₃', 'ₐ', 'ₖ', 'ₘ', 'ₙ', 'ᵢ', 'ⁱ', '⋮', 'ₛ', 'ₜ', '≃', '⇔', '∧', '∅', 'ℕ', 'ⱼ', 'ʲ', '⊥', 'π']
extrasymbols = {'〚': '\llbracket', '〛': '\rrbracket'}
symbols = {s: allsymbols[s] for s in mysymbols} symbols = {s: allsymbols[s] for s in mysymbols}
mathsymbols = {s: '$'+allsymbols[s]+'$' for s in symbols} symbols.update(extrasymbols)
mathsymbols = {s: '$'+v+'$' for s, v in symbols.items()}
def read_by_char(fname): def read_by_char(fname):
# Yield character and True/False if inside mathmode block # Yield character and True/False if inside mathmode block

BIN
tesi/tesi.pdf
View file

Binary file not shown.

16
tesi/tesi_unicode.org
View file

@ -921,17 +921,17 @@ 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 target decision tree Cₜ covers the input space /S/, we say that
the two decision trees are equivalent when: the two decision trees are equivalent when:
| (equiv S Cₛ Cₜ gs = Yes) ∧ covers(Cₜ, S) ⇒ ∀vₛ≃vₜ ∈ S, Cₛ(vₛ) ≃gs Cₜ(vₜ) | equiv(S, Cₛ, Cₜ, gs) = Yes ∧ covers(Cₜ, S) → ∀vₛ≃vₜ ∈ S, Cₛ(vₛ) ≃gs Cₜ(vₜ)
Similarly we say that a couple of decision 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: 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ₜ) | equiv(S, Cₛ, Cₜ, gs) = No(vₛ,vₜ) ∧ covers(Cₜ, S) → vₛ≃vₜ ∈ S ∧ Cₛ(vₛ) ≠gs Cₜ(vₜ)
Corollary: For a full input space /S/, that is the universe of the Corollary: For a full input space /S/, that is the universe of the
target program we say: target program we say:
| (equiv S [|tₛ|]ₛ [|tₜ|]ₜ ∅ = Yes) ⇔ tₛ ≃ tₜ | equiv(S, 〚tₛ〛ₛ, 〚tₜ〛ₜ, ∅) = Yes ⇔ tₛ ≃ tₜ
*** Proof of the correctness of the translation from source programs to source decision trees *** Proof of the correctness of the translation from source programs to source decision trees
@ -1011,13 +1011,13 @@ 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. every couple of source value /vₛ/ and target value /vₜ/ that are equivalent.
\begin{comment} \begin{comment}
Define "covered" Define "covered"
Is it correct to say the same? How to correctly distinguish in words ≊ and = ? Is it correct to say the same? How to correctly distinguish in words ≃ and = ?
\end{comment} \end{comment}
| equiv(S, Cₛ, Cₜ) = Yes and cover(Cₜ, S) → ∀ vₛ ≊ vₜ∈S ∧ Cₛ(vₛ) = Cₜ(vₜ) | 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 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 of counter example values vₛ and vₜ for which the two decision trees
outputs a different result. outputs a different result.
| equiv(S, Cₛ, Cₜ) = No(vₛ,vₜ) and cover(Cₜ, S) → ∀ vₛ ≊ vₜ∈S ∧ Cₛ(vₛ) ≠ Cₜ(vₜ) | equiv(S, Cₛ, Cₜ) = No(vₛ,vₜ) and cover(Cₜ, S) → ∀ vₛ ≃ vₜ∈S ∧ Cₛ(vₛ) ≠ Cₜ(vₜ)
We define the following We define the following
| Forall(Yes) = Yes | Forall(Yes) = Yes
@ -1054,10 +1054,10 @@ In the other subcases S is always non-empty.
subtree Cₜᵢ subtree Cₜᵢ
| equiv(Sᵢ, Cₛ, Cₜᵢ) = Yes ∀i | equiv(Sᵢ, Cₛ, Cₜᵢ) = Yes ∀i
or we have a counter example vₛ, vₜ for which or we have a counter example vₛ, vₜ for which
| vₛ≊vₜ∈Sₖ ∧ cₛ(vₛ) ≠ Cₜₖ(vₜ) | vₛ≃vₜ∈Sₖ ∧ cₛ(vₛ) ≠ Cₜₖ(vₜ)
then because then because
| vₜ∈(a→πₖ) ⇒ Cₜ(vₜ) = Cₜₖ(vₜ) | vₜ∈(a→πₖ) ⇒ Cₜ(vₜ) = Cₜₖ(vₜ)
then then
| vₛ≊vₜ∈S ∧ Cₛ(vₛ)≠Cₜ(vₜ) | vₛ≃vₜ∈S ∧ Cₛ(vₛ)≠Cₜ(vₜ)
and the result of the algorithm is and the result of the algorithm is
| equiv(Sᵢ, Cₛ, Cₜᵢ) = No(vₛ, vₜ) for some minimal k∈I | equiv(Sᵢ, Cₛ, Cₜᵢ) = No(vₛ, vₜ) for some minimal k∈I