Difference between revisions of "SCI/Specifications/SCI in action/Parser"

Jump to navigation Jump to search
→‎Matching the trees: Changed to use <math>, made SCI-AUGMENT algorithm readable.
(→‎The Parse tree: Started to convert things to <math>; clarified some parts of the text)
(→‎Matching the trees: Changed to use <math>, made SCI-AUGMENT algorithm readable.)
Line 545: Line 545:


==Matching the trees==
==Matching the trees==
The exact algorithm used to compare <i>T</i><sub>&pi;</sub> to <i>T</i><sub>&Sigma;</sub> is not known yet. The one described here is based on the approximation used in FreeSCI, which is very similar to the original SCI one.
The exact algorithm used to compare <math>T_\pi</math> to <math>T_\Sigma</math> is not known yet. The one described here is based on the approximation used in FreeSCI, which is very similar to the original SCI one.


First, we need to describe a set of functions for traversing the nodes of <i>T</i><sub>&Sigma;</sub> and <i>T</i><sub>&pi;</sub> , and doing some work. They will be operating on the sets &#8469; (all non-negative integral numbers), &#120121; (Booleans), and <i>NODE</i> (which we defined earlier).
First, we need to describe a set of functions for traversing the nodes of <math>T_\Sigma</math> and <math>T_\pi</math>, and doing some work. They will be operating on the sets <math>\mathbb{N}</math> (all non-negative integral numbers), <math>\mathbb{B}</math> (Booleans), and <math>\mathrm{Node}</math> (which we defined earlier).
<br>
first: Node &rarr; S first((s, v, n<sub>0</sub>, n<sub>1</sub> &hellip; n<sub>i</sub>)) := s<br>


second : Node &rarr; V second((s, v, n<sub>0</sub>, n<sub>1</sub> &hellip; n<sub>i</sub>)) := v<br>
<math>
\newcommand{\tuple}[1]{\langle #1 \rangle}
\newcommand{\nat}{\mathbb{N}}
\newcommand{\bool}{\mathbb{B}}
\newcommand{\Btt}{\textrm{tt}}
\newcommand{\Bff}{\textrm{ff}}
\newcommand{\Node}{\mathrm{Node}}
\begin{align*}
\textrm{first}: & \Node \to S \\
\textrm{first}: & \tuple{s, v, n_{0}, n_{1} \ldots n_{i}} \mapsto s \\
\\
\textrm{second}: & \Node \to V \\
\textrm{second}: & \tuple{s, v, n_{0}, n_{1} \ldots n_{i}} \mapsto v \\
\\
\textrm{word}: & \Node \to \Gamma \\
\textrm{word}: & \tuple{s, v, \gamma} \mapsto \gamma \\
\\
\textrm{children}: & \Node \to \Node* \\
\textrm{children}: & \tuple{s, v, n_{0}, n_{1} \ldots n_{i}} \mapsto \{ m\in \Node \mid m\in\{ n_{0}, n_{1} \ldots n_{i} \} \} \\
\\
\textrm{all-children}: & \Node \to \Node* \\
\textrm{all-children}: & n \mapsto \textrm{children}(n) \cup \{ m \mid \exists l \in\textrm{all-children}(n) . m\in l \} \\
\\
\textrm{is-word} : & \Node \to \bool \\
\textrm{is-word} : & \tuple{s, v, n_{0}, n_{1} \ldots n_{i}} \mapsto \Btt \iff (i = 0) \land n_{0} \in \Gamma \\
\textrm{verify-sentence-part-elements}: & \Node \times \Node \to \bool \\
\textrm{verify-sentence-part-elements}: & \tuple{n_{p}, n_{s}} \mapsto \Btt \iff (\textrm{first}(n_{s} = 152) \land \\
& ((\forall m \in \Node.\textrm{verify-sentence-part-elements}(m, n_{s}) \iff \\
& \{ w \mid \exists t \in \textrm{all-children}(m).w = \textrm{word}(t)\} = \emptyset) \lor \\
& \exists m \in \textrm{children}(n_{s}).\textrm{verify-sentence-part-elements}(m, n_{s})) ) \lor \\
& ((\textrm{second}(n_{s}) = 153) \land (\exists m.m \in \textrm{children}(n_{s}).(\exists o \in \textrm{all-children}(n_{s}).\\
& (\textrm{first}(o) = \textrm{first}(n_{p})) \land \textrm{word}(o) = \textrm{word}(m))) ) \lor \\
& ((\textrm{second}(n_{s}) \in \{144, 14c\}) \land
(\exists m \in \textrm{children}(n_{s}).\textrm{verify-sentence-part}(m, n_{s}))) \\
\\
\textrm{verify-sentence-part}: & \Node \times \Node \to \bool \\
\textrm{verify-sentence-part}: & \tuple{n_{p}, n_{s}} \mapsto \Btt \iff \forall n \in \textrm{children}(n_{s}):\exists m\in\textrm{children}(n_{p}). \\
& (\textrm{first}(m) = \textrm{first}(n)) \land \textrm{verify-sentence-part-elements}(n, m) \\
\\
\textrm{verify-sentence-part-brackets}: & \Node \times \Node \to \bool \\
\textrm{verify-sentence-part-brackets}: & \tuple{n_{p}, n_{s}} \mapsto \Btt \iff
(\textrm{first}(n_{p}) = 152 \land
(\forall m\in \Node. (\textrm{first}(m) = \textrm{first}(n_{s})) \land\\
& (\textrm{second}(m) = \textrm{second}(n_{s})). \textrm{verify-sentence-part}(n_{p}, m) \iff\\
& \{ w \mid \exists t \in \textrm{all-children}(m).w = \textrm{word}(t)\} = \emptyset)) \lor \\
& ((\textrm{first}(n_{p}) \in \{141, 142, 143\}) \land
    \textrm{verify-sentence-part}(n_{p}, n_{s})) \\
\end{align*}
</math>


word : Node &rarr; &Gamma word((s, v, γ)) := &gamma;<br>
With these functions, we can now define an algorithm for augmenting <math>T_\pi</math> and <math>T_\Sigma</math>:


children : Node &rarr; Node∗ children((s, v, n<sub>0</sub>, n<sub>1</sub> &hellip; n<sub>i</sub>)) := { m | &forall;m.m&isin;{ n<sub>0</sub>, n<sub>1</sub> &hellip; n<sub>i</sub> } &and; m&isin;Node }<br>
  Algorithm SCI-AUGMENT:
  matched := tt
  claim_on_match := tt
  FOREACH n &isin; root(<math>T_\Sigma</math>)
    IF ((first(n) = 14b) &and; (second(n) = f900)) THEN
      claim_on_match := ff
    ELSE IF &not;verify_sentence_part_brackets(n, root(<math>T_\pi</math>)) THEN
      matched := ff
    ENDIF
  ENDFOREACH


all_children : Node &rarr; Node∗ all_children(n) := children(n) &cup; { m | &exist;l.l&isin;all_children(n).m&isin;l }<br>
Augmenting succeeded if matched = tt; in this case, <math>T_\pi</math> is one of the trees accepted by the description provided by <math>T_\Sigma</math>. In this case, Said() will return 1. It will also claim the event previously provided to Parse(), unless claim_on_match = ff.
 
is_word : Node &rarr; B is_word((s, v, n<sub>0</sub>, n<sub>1</sub> &hellip; n<sub>i</sub>) = tt &hArr; (i = 0) &and; n<sub>0</sub> &isin; &Gamma<br>
 
contains_word : Node &times; S &times; &Gamma &rarr; B contains_word(n, s, &gamma;) = tt &gamma; = 0xfff<ref>This is the so-called "anyword". Words with a word group of 0xfff match any other word.</ref> ∨ (&hArr; &exist;m.m&isin;all_children(n).(s = second(m)) &and; (is_word(m) &and; (word(m) = &gamma;)))<br>
 
verify_sentence_part_elements : Node &times; Node &rarr; B verify_sentence_part_elements(n<sub>p</sub>, n<sub>s</sub>) = tt &hArr; (first(n<sub>s</sub> = 152) &and; ((&forall;m.m &isin; Node.verify_sentence_part_elements(m, n<sub>s</sub>) &hArr; { w | &exist;t.t &isin; all_children(m).w = word(t)} = &empty;) &or; &exist;m &isin;<br>
children(n<sub>s</sub>).verify_sentence_part_elements(m, n<sub>s</sub>)) ) &or; ((second(n<sub>s</sub>) = 153) &and; (&exist;m.m &isin; children(n<sub>s</sub>).(&exist;o &isin; all_children(n<sub>s</sub>).(first(o) = first(n<sub>p</sub>)) &and; word(o) = word(m))) ) &or; ((second(n<sub>s</sub>) &isin; {144, 14c}) &and; (&exist;m.m &isin; children(n<sub>s</sub>).verify_sentence_part(m, n<sub>s</sub>)))<br>
 
verify_sentence_part : Node &times; Node &rarr; B<br>
verify_sentence_part(n<sub>p</sub>, n<sub>s</sub>) = tt &hArr; &forall;n.n &isin; children(n<sub>s</sub>):&exist;m.m&isin;children(n<sub>p</sub>).(first(m) = first(n)) &and; verify_sentence_part_elements(n, m)<br>
 
verify_sentence_part_brackets : Node &times; Node &rarr; B verify_sentence_part_brackets(n<sub>p</sub>, n<sub>s</sub>) = tt &hArr; (first(n<sub>p</sub>) = 152 &and; (&forall;m.m&isin;Node.(first(m) = first(n<sub>s</sub>)) &and; (second(m) = second(n<sub>s</sub>)). verify_sentence_part(n<sub>p</sub>, m) &hArr; { w | &exist;t.t &isin; all_children(m).w = word(t)} = &empty;)) &or; ((first(n<sub>p</sub>) &isin; {141, 142, 143}) &and; verify_sentence_part(n<sub>p</sub>, n<sub>s</sub>))<br>
 
With these functions, we can now define an algorithm for augmenting T<sub>&pi;</sub> and T<sub>&Sigma;</sub> :
 
Algorithm SCI-AUGMENT matched := tt claim_on_match := tt FOREACH n &isin; root(T<sub>&Sigma;</sub>) IF ((first(n) = 14b) &and; (second(n) = f900)) THEN claim_on_match := ff ELSE IF &not;verify_sentence_part_brackets(n, root(T<sub>&pi;</sub>)) THEN matched := ff HCAEROF
 
Augmenting succeeded if matched = tt; in this case, T<sub>&pi</sub> is one of the trees accepted by the description provided by T<sub>&Sigma</sub>. In this case, Said() will return 1. It will also claim the event previously provided to Parse(), unless claim_on_match = ff.


==Notes==
==Notes==
<references/>
<references/>
1,079

edits

Navigation menu