You need the following to resolve the most trivial case:
s2intAux(0,0).
This will cause s2intAux(0,Y)
to be true when Y is instantiated to 0.
In your subsequent lines, you don't have a statement that resolves Z
to 0 when you run out of the s(.)
. For that, you need to take care of the single s(0)
case. Then you can do the general case:
s2intAux(X,Y) :- X = s(0), Y is 1.
s2intAux(X,Y) :- X = s(Z), s2intAux(Z,Y1), Y is Y1 + 1.
Note that on the general case, we have to traverse down to get to the Y is 1
before we can unravel back up and finally assign Y to Y1 + 1
.
You can also write that first line as just:
s2intAux(s(0),Y) :- Y is 1.
Final answer looks like this:
s2intAux(0,0).
s2intAux(s(0),Y) :- Y is 1.
s2intAux(X,Y) :- X = s(Z), s2intAux(Z,Y1), Y is Y1 + 1.