236
edits
Difference between revisions of "SCI/Specifications/SCI in action/Parser"
SCI/Specifications/SCI in action/Parser (view source)
Revision as of 14:31, 19 January 2009
, 14:31, 19 January 2009Merging 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>π</sub> to <i>T</i><sub>Σ</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>π</sub> to <i>T</i><sub>Σ</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>Σ</sub> and <i>T</i><sub>π</sub> , and doing some work. They will be operating on the sets ℕ (all non-negative integral numbers), 𝔹 (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>Σ</sub> and <i>T</i><sub>π</sub> , and doing some work. They will be operating on the sets ℕ (all non-negative integral numbers), 𝔹 (Booleans), and <i>NODE</i> (which we defined earlier). | ||
<br> | |||
first: Node → S first((s, v, n<sub>0</sub>, n<sub>1</sub> … n<sub>i</sub>)) := s<br> | |||
second : Node → V second((s, v, n<sub>0</sub>, n<sub>1</sub> … n<sub>i</sub>)) := v<br> | |||
word : Node → &Gamma word((s, v, γ)) := γ<br> | |||
children : Node → Node∗ children((s, v, n<sub>0</sub>, n<sub>1</sub> … n<sub>i</sub>)) := { m | ∀m.m∈{ n<sub>0</sub>, n<sub>1</sub> … n<sub>i</sub> } ∧ m∈Node }<br> | |||
all_children : Node → Node∗ all_children(n) := children(n) ∪ { m | ∃l.l∈all_children(n).m∈l }<br> | |||
is_word : Node → B is_word((s, v, n<sub>0</sub>, n<sub>1</sub> … n<sub>i</sub>) = tt ⇔ (i = 0) ∧ n<sub>0</sub> ∈ &Gamma<br> | |||
contains_word : Node × S × &Gamma → B contains_word(n, s, γ) = tt γ = 0xfff<ref>This is the so-called "anyword". Words with a word group of 0xfff match any other word.</ref> ∨ (⇔ ∃m.m∈all_children(n).(s = second(m)) ∧ (is_word(m) ∧ (word(m) = γ)))<br> | |||
verify_sentence_part_elements : Node × Node → B verify_sentence_part_elements(n<sub>p</sub>, n<sub>s</sub>) = tt ⇔ (first(n<sub>s</sub> = 152) ∧ ((∀m.m ∈ Node.verify_sentence_part_elements(m, n<sub>s</sub>) ⇔ { w | ∃t.t ∈ all_children(m).w = word(t)} = ∅) ∨ ∃m ∈<br> | |||
children(n<sub>s</sub>).verify_sentence_part_elements(m, n<sub>s</sub>)) ) ∨ ((second(n<sub>s</sub>) = 153) ∧ (∃m.m ∈ children(n<sub>s</sub>).(∃o ∈ all_children(n<sub>s</sub>).(first(o) = first(n<sub>p</sub>)) ∧ word(o) = word(m))) ) ∨ ((second(n<sub>s</sub>) ∈ {144, 14c}) ∧ (∃m.m ∈ children(n<sub>s</sub>).verify_sentence_part(m, n<sub>s</sub>)))<br> | |||
verify_sentence_part : Node × Node → B<br> | |||
verify_sentence_part(n<sub>p</sub>, n<sub>s</sub>) = tt ⇔ ∀n.n ∈ children(n<sub>s</sub>):∃m.m∈children(n<sub>p</sub>).(first(m) = first(n)) ∧ verify_sentence_part_elements(n, m)<br> | |||
verify_sentence_part_brackets : Node × Node → B verify_sentence_part_brackets(n<sub>p</sub>, n<sub>s</sub>) = tt ⇔ (first(n<sub>p</sub>) = 152 ∧ (∀m.m∈Node.(first(m) = first(n<sub>s</sub>)) ∧ (second(m) = second(n<sub>s</sub>)). verify_sentence_part(n<sub>p</sub>, m) ⇔ { w | ∃t.t ∈ all_children(m).w = word(t)} = ∅)) ∨ ((first(n<sub>p</sub>) ∈ {141, 142, 143}) ∧ 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>π</sub> and T<sub>Σ</sub> : | |||
Algorithm SCI-AUGMENT matched := tt claim_on_match := tt FOREACH n ∈ root(T<sub>Σ</sub>) IF ((first(n) = 14b) ∧ (second(n) = f900)) THEN claim_on_match := ff ELSE IF ¬verify_sentence_part_brackets(n, root(T<sub>π</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/> | ||