A note on occur-check (extended report)
Fuente:
arXiv
Saved in:
| Main Author: | |
|---|---|
| Format: | Preprint |
| Published: |
2022
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866909747993640960 |
|---|---|
| author | Drabent, Włodzimierz |
| author_facet | Drabent, Włodzimierz |
| contents | We weaken the notion of "not subject to occur-check" (NSTO), on which most known results on avoiding the occur-check in logic programming are based. NSTO means that unification is performed only on such pairs of atoms for which the occur-check never succeeds in any run of a nondeterministic unification algorithm. Here we show that "any run" can be weakened to "some run". We present some related sufficient conditions under which the occur-check may be safely omitted. We show examples for which the proposed approach provides more general results than the approaches based on well-moded and nicely moded programs (this includes cases to which the latter approaches are inapplicable). We additionally present a sufficient condition based on NSTO, working for arbitrary selection rules. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2204_05379 |
| institution | arXiv |
| publishDate | 2022 |
| record_format | arxiv |
| spellingShingle | A note on occur-check (extended report) Drabent, Włodzimierz Logic in Computer Science Programming Languages 68N17 03B10 D.1.6; F.3.3; F.4.1; F.3.1 We weaken the notion of "not subject to occur-check" (NSTO), on which most known results on avoiding the occur-check in logic programming are based. NSTO means that unification is performed only on such pairs of atoms for which the occur-check never succeeds in any run of a nondeterministic unification algorithm. Here we show that "any run" can be weakened to "some run". We present some related sufficient conditions under which the occur-check may be safely omitted. We show examples for which the proposed approach provides more general results than the approaches based on well-moded and nicely moded programs (this includes cases to which the latter approaches are inapplicable). We additionally present a sufficient condition based on NSTO, working for arbitrary selection rules. |
| title | A note on occur-check (extended report) |
| topic | Logic in Computer Science Programming Languages 68N17 03B10 D.1.6; F.3.3; F.4.1; F.3.1 |
| url | https://arxiv.org/abs/2204.05379 |