> The key observation to me was that the traditional Datalog/Prolog way of
unifying is through syntactic equality, which is a bit too simple to express
the kind of equality needed in Rust and elsewhere.
I was surprised by this comment because Horn logic, although syntactically
restricted, has Universal Turing Machine expressivity and it's difficult to
see what Rust needs to do that needs more expressive power than a UTM(!).
Reading the post I understand that the author is speaking about unification in
particular, not Horn clauses and resolution, where unification is typically
used, however there is still a subtle error, which is the identificatin of
unification as "syntactic equality". While unification can be used to decide
whether two terms are syntacticall equal, in the sense that if they are, they
will unify, unification on its own is not syntactic equality.
First of all, say that T₁ = f(χ) and T₂ = f(α) are two terms. Note that χ is a
variable and α is a constant. Clearly T₁ ≠ T₂ and that is true for "syntactic"
equality, because χ ≠ α.
Now suppose that θ = {χ/α} is a substitution of the variables in {T₁,T₂}.
Now, θT₁ = Τ₂. Read θT₁ as "T₁ with θ applied". In other words, T₁ is equal to
T₂ _if_ χ is substituted with α. A unification algorithm (normally, Robinson's
unification algorithm) is used to establish that two terms are equal given a
substitution of their variables. In particular, a substitution of variables
that allows two terms to unify is a "unifier". Note that unifiers can be
composed, so for example, if T₃ = f(χ,υ), T₄ = f(α,β), φ = {χ/α} and ψ = {υ/β}
then φT₃ ≠ T₄ but φψT₃ = T₄.
I noticed in the examples of Rust-in-Prolog given in the link above that the
author subtly fudges the syntax of Prolog, for example Bar, which is normally
a variable in Prolog, is used as a constant, whereas ?A and ?B which would be
not-variables in Prolog (but partially ground terms) are used as variables. I
wonder if this is part of a now-divide-by-zero step in the author's reasoning,
that I can't figure out exactly because I don't know any Rust. For example,
what is "?A" and what is "Bar" in the context of Rust?
In any case, the author is of course correct that unification is not type
equality- but then, nothing is except for type equality. As far as I
understand these things anyway- I'm not a type nerd. Bottom line, you can't
implement "type equality" as any other kind of "equality" and you'll have to
jump through hoops -the hoops of defining your higher-level notion of
equality- in what ever language you choose.
you'll have to jump through hoops -the hoops of defining your higher-level notion of equality- in what ever language you choose.
Right. The author is just disappointed that Prolog does have a built-in "equality" that isn't the equality they want. A nice solution in Prolog would be to write a meta-interpreter or to do term rewriting on the input program. This would allow the author to write
Yes. I just don't see why this is such a big hassle. Particularly because -I'm guessing- whatever the Rust compiler does to decide type equality can't be less hassle-y than that.
But, I might misunderstand the problem since, again, I don't know Rust.
Comments
I was surprised by this comment because Horn logic, although syntactically restricted, has Universal Turing Machine expressivity and it's difficult to see what Rust needs to do that needs more expressive power than a UTM(!).
Reading the post I understand that the author is speaking about unification in particular, not Horn clauses and resolution, where unification is typically used, however there is still a subtle error, which is the identificatin of unification as "syntactic equality". While unification can be used to decide whether two terms are syntacticall equal, in the sense that if they are, they will unify, unification on its own is not syntactic equality.
First of all, say that T₁ = f(χ) and T₂ = f(α) are two terms. Note that χ is a variable and α is a constant. Clearly T₁ ≠ T₂ and that is true for "syntactic" equality, because χ ≠ α.
Now suppose that θ = {χ/α} is a substitution of the variables in {T₁,T₂}. Now, θT₁ = Τ₂. Read θT₁ as "T₁ with θ applied". In other words, T₁ is equal to T₂ _if_ χ is substituted with α. A unification algorithm (normally, Robinson's unification algorithm) is used to establish that two terms are equal given a substitution of their variables. In particular, a substitution of variables that allows two terms to unify is a "unifier". Note that unifiers can be composed, so for example, if T₃ = f(χ,υ), T₄ = f(α,β), φ = {χ/α} and ψ = {υ/β} then φT₃ ≠ T₄ but φψT₃ = T₄.
I noticed in the examples of Rust-in-Prolog given in the link above that the author subtly fudges the syntax of Prolog, for example Bar, which is normally a variable in Prolog, is used as a constant, whereas ?A and ?B which would be not-variables in Prolog (but partially ground terms) are used as variables. I wonder if this is part of a now-divide-by-zero step in the author's reasoning, that I can't figure out exactly because I don't know any Rust. For example, what is "?A" and what is "Bar" in the context of Rust?
In any case, the author is of course correct that unification is not type equality- but then, nothing is except for type equality. As far as I understand these things anyway- I'm not a type nerd. Bottom line, you can't implement "type equality" as any other kind of "equality" and you'll have to jump through hoops -the hoops of defining your higher-level notion of equality- in what ever language you choose.
Right. The author is just disappointed that Prolog does have a built-in "equality" that isn't the equality they want. A nice solution in Prolog would be to write a meta-interpreter or to do term rewriting on the input program. This would allow the author to write
and have it be interpreted asYes. I just don't see why this is such a big hassle. Particularly because -I'm guessing- whatever the Rust compiler does to decide type equality can't be less hassle-y than that.
But, I might misunderstand the problem since, again, I don't know Rust.