3 ms·

"Insightful observation" doesn't quite do it justice ;) There's a whole discipline in discrete math dealing with the possibilities and limitations of equational

"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.

YeGoblynQueenne 6y ago
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).
- tannhaeuser 6y ago
  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.
  - YeGoblynQueenne 6y ago
    >> 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.
    - tom_mellior 6y ago
      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 http://www.cs.bu.edu/~snyder/publications/UnifChapter.pdf This is specific to unification and not to broader equational reasoning.
      - YeGoblynQueenne 6y ago
        Thanks.

YeGoblynQueenne 6y ago

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).

tannhaeuser 6y ago
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.
- YeGoblynQueenne 6y ago
  >> 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.
  - tom_mellior 6y ago
    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 http://www.cs.bu.edu/~snyder/publications/UnifChapter.pdf This is specific to unification and not to broader equational reasoning.
    - YeGoblynQueenne 6y ago
      Thanks.