In other news I found a 1986 paper by Alexander Herold and Jörg H. Siekmann in the Journal of Automated Reasoning titled "Unification in Abelian Semigroups" that puts to rest a minor conjecture I had made that I had sincerely hoped to be true — sadly it isn't. ACU-unification (that is, equational unification where the theory is associativity and commutativity of some binary symbol *, plus unit laws for some unit element e) with constants isn't unitary, (i.e. doesn't have most general unifiers) but merely finitary (has finite complete sets of unifiers). So everything is still well and good for typechecking in my little substructural hybrid LF variant being decidable, but term reconstruction at the world level is going to be incomplete just as it is for the rest of term reconstruction. Not at all a disaster, but I thought I had convinced myself that MGUs existed, which would have been nice.
In other news I found a 1986 paper by Alexander Herold and Jörg H. Siekmann in the Journal of Automated Reasoning titled "Unification in Abelian Semigroups" that puts to rest a minor conjecture I had made that I had sincerely hoped to be true — sadly it isn't. ACU-unification (that is, equational unification where the theory is associativity and commutativity of some binary symbol *, plus unit laws for some unit element e) with constants isn't unitary, (i.e. doesn't have most general unifiers) but merely finitary (has finite complete sets of unifiers). So everything is still well and good for typechecking in my little substructural hybrid LF variant being decidable, but term reconstruction at the world level is going to be incomplete just as it is for the rest of term reconstruction. Not at all a disaster, but I thought I had convinced myself that MGUs existed, which would have been nice.
-
(no subject)
Guy from Seattle team we've been working with showed up today at work; no matter how much I'm generally comfortable working with remote teams (and I…
-
(no subject)
Something that's bugged me for a long time is this: How many paths, starting at the origin, taking N steps either up, down, left or right, end up at…
-
(no subject)
Slept terrrrrribly last night, don't know why. Woke up about 1-2am, and felt an increasing hard-to-break cycle of anxiety, stomach feeling like crap,…
- Post a new comment
- 8 comments
- Post a new comment
- 8 comments