4 ms·

You're right, from the point of view of a sufficiently strong logic and a sufficiently strong prover for that logic! But: > N is either ... In a type system

You're right, from the point of view of a sufficiently strong logic and a sufficiently strong prover for that logic! But: > N is either ... In a type system like Prolog's, N can also be any of: f(Y) apple_pie N (a free variable) You assume a type and mode system in which X and N must be bound, and they must be bound to ground natural number terms. You also assume that the logic programming system can deduce positive information from the failing unification on an infinite domain (that X must be s(0) if it is not 0 and not of the form s(s(N)))). It's possible that the article's author also had all these implicit assumptions, but it's not clear to me that they did.

feanaro 8y ago
Right, thanks for the insight. A further thought: `apple_pie` wouldn't actually be problematic, in the sense that we could deduce `¬even(apple_pie)` from the way it's currently written. This is because `apple_pie` is obviously neither `0` nor `s(s(N))`. Of course, this might not be desirable philosophically since it might be preferable to consider applying `even` to `apple_pie` nonsense since they are of different types (informally speaking). Is this right? Am I missing something?
- tom_mellior 8y ago
  > A further thought: `apple_pie` wouldn't actually be problematic, in the sense that we could deduce `¬even(apple_pie)` from the way it's currently written. Yes. We can have the same behavior with the following Prolog implementation: not_even(X) :- X \= 0, ( X \= s(s(_N)) ; X = s(s(N)), not_even(N) ). (This is a translation of the article's definition, except that I added the "X = s(s(N))" condition to make the case distinction explicit and actually bind N in the second branch. It wouldn't work without this for the reason I mentioned above, of deducing this equality from a failure.) ?- not_even(s(s(0))). false. ?- not_even(s(s(s(0)))). true . ?- not_even(apple_pie). true . > Of course, this might not be desirable philosophically since it might be preferable to consider applying `even` to `apple_pie` nonsense since they are of different types (informally speaking). Right. This is one of the reasons why some Prolog extensions and Prolog-like languages like Mercury add static type systems. It makes little sense to ask whether apple pie is even or odd.

feanaro 8y ago

Right, thanks for the insight. A further thought: `apple_pie` wouldn't actually be problematic, in the sense that we could deduce `¬even(apple_pie)` from the way it's currently written. This is because `apple_pie` is obviously neither `0` nor `s(s(N))`. Of course, this might not be desirable philosophically since it might be preferable to consider applying `even` to `apple_pie` nonsense since they are of different types (informally speaking). Is this right? Am I missing something?

tom_mellior 8y ago
> A further thought: `apple_pie` wouldn't actually be problematic, in the sense that we could deduce `¬even(apple_pie)` from the way it's currently written. Yes. We can have the same behavior with the following Prolog implementation: not_even(X) :- X \= 0, ( X \= s(s(_N)) ; X = s(s(N)), not_even(N) ). (This is a translation of the article's definition, except that I added the "X = s(s(N))" condition to make the case distinction explicit and actually bind N in the second branch. It wouldn't work without this for the reason I mentioned above, of deducing this equality from a failure.) ?- not_even(s(s(0))). false. ?- not_even(s(s(s(0)))). true . ?- not_even(apple_pie). true . > Of course, this might not be desirable philosophically since it might be preferable to consider applying `even` to `apple_pie` nonsense since they are of different types (informally speaking). Right. This is one of the reasons why some Prolog extensions and Prolog-like languages like Mercury add static type systems. It makes little sense to ask whether apple pie is even or odd.