"Insightful observation" doesn't quite do it justice ;) There's a whole discipline in discrete math dealing with the possibilities and limitations of equational theories and reasoning. And it could be said their limitations gave rise to the various constraint formalisms that were introduced in the 80s and 90s as Prolog extensions and sometimes (syntactic) generalizations.
Well then, please elaborate because I know nothing of the discipline you describe and it certainly sounds interesting (though it also sounds a little fussy).
I'm not going to summarize classic equational reasoning (with it's deep connection to algebraic geometry and whatnot) here in a single HN post ;) I can point you to some classic works/authors in the field, though (and I'm sure some fellow HNers can provide some more): Gauss, Knuth, Bendix, Gröbner, Buchberger, Bachmaier, Euclid, Ganzinger, Davis, Putnam, Robinson, and Colmerauer for Prolog 2. There are also category theory papers relevant to reasoning about data structures, and of course Damas, Hindley, Miller for type theories. The way is the goal here.
> I'm not going to summarize classic equational reasoning (with it's deep connection to algebraic geometry and whatnot) here in a single HN post ;)
Aw :(
Alright, I'll just chase down some of the references you say. I was going to check out Prolog 2 anyway, after browsing the wikipedia article on Colmerauer a few days ago and seeing a reference to his later work there.
To be a bit more concrete than the grandparent's name soup, I liked this handbook article about unification in theories: Franz Baader and Jörg Siekmann. Unification Theory. In D.M. Gabbay, C.J. Hogger, and J.A. Robinson, editors, Handbook of Logic in Artificial Intelligence and Logic Programming, pages 41-125. Oxford University Press, Oxford, UK, 1994.
Comments
"Insightful observation" doesn't quite do it justice ;) There's a whole discipline in discrete math dealing with the possibilities and limitations of equational theories and reasoning. And it could be said their limitations gave rise to the various constraint formalisms that were introduced in the 80s and 90s as Prolog extensions and sometimes (syntactic) generalizations.
Well then, please elaborate because I know nothing of the discipline you describe and it certainly sounds interesting (though it also sounds a little fussy).
I'm not going to summarize classic equational reasoning (with it's deep connection to algebraic geometry and whatnot) here in a single HN post ;) I can point you to some classic works/authors in the field, though (and I'm sure some fellow HNers can provide some more): Gauss, Knuth, Bendix, Gröbner, Buchberger, Bachmaier, Euclid, Ganzinger, Davis, Putnam, Robinson, and Colmerauer for Prolog 2. There are also category theory papers relevant to reasoning about data structures, and of course Damas, Hindley, Miller for type theories. The way is the goal here.
Aw :(
Alright, I'll just chase down some of the references you say. I was going to check out Prolog 2 anyway, after browsing the wikipedia article on Colmerauer a few days ago and seeing a reference to his later work there.
To be a bit more concrete than the grandparent's name soup, I liked this handbook article about unification in theories: Franz Baader and Jörg Siekmann. Unification Theory. In D.M. Gabbay, C.J. Hogger, and J.A. Robinson, editors, Handbook of Logic in Artificial Intelligence and Logic Programming, pages 41-125. Oxford University Press, Oxford, UK, 1994.
This seems to be a newer version with similar contents but different authors: http://www.cs.bu.edu/~snyder/publications/UnifChapter.pdf
This is specific to unification and not to broader equational reasoning.
Thanks.