Open main menu

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

Merging of the SCI documentation. Work in progress.
(→‎Semantics: Fixed some pseudo code)
(Merging of the SCI documentation. Work in progress.)
Line 548: Line 548:
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 <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.


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 <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).
<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>
 
word : Node &rarr; &Gamma word((s, v, γ)) := &gamma;<br>
 
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>
 
all_children : Node &rarr; Node∗ all_children(n) := children(n) &cup; { m | &exist;l.l&isin;all_children(n).m&isin;l }<br>
 
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/>
245

edits