Abstract | ||
---|---|---|
In the A-calculus, there is a standard notion of what terms should be considered to be "undefined": the unsolvable terms. There are various equivalent characterisations of this property of terms. We attempt to find a similar notion for orthogonal term rewrite systems. We find that in general the properties of terms analogous to the various characterisations of solvabil- ity differ. We give two axioms that a notion of undefinedness should satisfy, and explore some of their consequences. The axioms lead to a concept analogous to the BShm trees of the A-calculus. Each term has a unique B5hm tree, and the set of such trees forms a domain which provides a denotational semantics for the rewrite system. We consider several particular notions of undefinedness satisfying the axioms, and compare them. |
Year | DOI | Venue |
---|---|---|
1994 | 10.1007/3-540-57887-0_114 | TACS |
Keywords | Field | DocType |
syntactic definitions,satisfiability | Algebra,Computer science,Algorithm,Syntax | Conference |
ISBN | Citations | PageRank |
3-540-57887-0 | 12 | 1.03 |
References | Authors | |
3 | 5 |
Name | Order | Citations | PageRank |
---|---|---|---|
Zena M. Ariola | 1 | 482 | 38.61 |
Richard Kennaway | 2 | 435 | 47.65 |
Jan Willem Kop | 3 | 12 | 1.03 |
M. Ronan Sleep | 4 | 178 | 31.24 |
Fer-Jan de Vries | 5 | 244 | 21.67 |