On the Sequential Nature of Unification
The problem of unification of terms is log-space complete for P. In deriving this lower bound no use is made of the potentially concise representation of terms by directed acyclic graphs. In addition, the problem remains complete even if infinite substitutions are allowed. A consequence of this resu...
| Main Authors: | , , |
|---|---|
| Published: |
2023
|
| Online Access: | https://hdl.handle.net/1721.1/149067 |
| _version_ | 1811085983107514368 |
|---|---|
| author | Dwork, Cynthia Kanellakis, Paris C. Mitchell, John C. |
| author_facet | Dwork, Cynthia Kanellakis, Paris C. Mitchell, John C. |
| author_sort | Dwork, Cynthia |
| collection | MIT |
| description | The problem of unification of terms is log-space complete for P. In deriving this lower bound no use is made of the potentially concise representation of terms by directed acyclic graphs. In addition, the problem remains complete even if infinite substitutions are allowed. A consequence of this result is that parallelism cannot significantly improve on the best sequential solutions for unification. The "dual" problem of computing the congruence closure of an equivalence relation is also log-space complete for P. However, we show that for the problem of term matching, an important subcase of unification, there is a good parallel algorithm using O(log^2 n) time and n^O(1) processors on a PRAM. For the O(log^2 n) parallel time upper bound we assume that the terms are presented by directed acyclic graphs; if the longer string representation is used we obtain an O(log n) parallel time bound. |
| first_indexed | 2024-09-23T13:19:02Z |
| id | mit-1721.1/149067 |
| institution | Massachusetts Institute of Technology |
| last_indexed | 2024-09-23T13:19:02Z |
| publishDate | 2023 |
| record_format | dspace |
| spelling | mit-1721.1/1490672023-03-30T03:39:34Z On the Sequential Nature of Unification Dwork, Cynthia Kanellakis, Paris C. Mitchell, John C. The problem of unification of terms is log-space complete for P. In deriving this lower bound no use is made of the potentially concise representation of terms by directed acyclic graphs. In addition, the problem remains complete even if infinite substitutions are allowed. A consequence of this result is that parallelism cannot significantly improve on the best sequential solutions for unification. The "dual" problem of computing the congruence closure of an equivalence relation is also log-space complete for P. However, we show that for the problem of term matching, an important subcase of unification, there is a good parallel algorithm using O(log^2 n) time and n^O(1) processors on a PRAM. For the O(log^2 n) parallel time upper bound we assume that the terms are presented by directed acyclic graphs; if the longer string representation is used we obtain an O(log n) parallel time bound. 2023-03-29T14:24:22Z 2023-03-29T14:24:22Z 1984-03 https://hdl.handle.net/1721.1/149067 13340605 MIT-LCS-TM-257 application/pdf |
| spellingShingle | Dwork, Cynthia Kanellakis, Paris C. Mitchell, John C. On the Sequential Nature of Unification |
| title | On the Sequential Nature of Unification |
| title_full | On the Sequential Nature of Unification |
| title_fullStr | On the Sequential Nature of Unification |
| title_full_unstemmed | On the Sequential Nature of Unification |
| title_short | On the Sequential Nature of Unification |
| title_sort | on the sequential nature of unification |
| url | https://hdl.handle.net/1721.1/149067 |
| work_keys_str_mv | AT dworkcynthia onthesequentialnatureofunification AT kanellakisparisc onthesequentialnatureofunification AT mitchelljohnc onthesequentialnatureofunification |