Counter in prolog

Question

I want to create a counter in prolog.

Something like starting it init/0. Adding 1 increment/0, and something like get_counter/1. To get the value.

But I don't know how to start something if you have init/0 with no inputs how to set something to 0.

Can someone give me some tips how I should try to do this?

I'm not a native speaker, so if it's not clear what I mean I'm sorry.

Answer 1

A declarative way to solve this is to see this as a relation between two counter values: One before the increment, and one after the increment.

You can use CLP(FD) constraints to relate the two counter values:

counter_next(C0, C) :- C0 + 1 #= C.

Such a predicate is completely pure and can be used in all directions.

A sequence of such relations describes repeatedly incrementing the counter, relating an initial value to its final state:

?- S0 = 0, counter_next(S0, S1), counter_next(S1, S).
S = 2,
S0 = 0,
S1 = 1

EDIT: Suppose you go the other way and manage to implement a 0-ary predicate increment/0, as you ask for, destructively incrementing a global resource. Then you will have severe declarative problems. For example, incrementing the counter must succeed, so we can expect to see:

?- increment.
true.

But this means that the original query is no longer equivalent to its own answer, because the query:

?- true.
true.

certainly does not increment the counter.

It also means you can no longer test and reason about your predicates in isolation, but have to think about the global resource all the time.

This in turn will make it much harder to understand and correct mistakes in your code.

Therefore, I strongly recommend you adopt a declarative way to think about this task, and make the relation between counter values before and after incrementing explicit. As an additional benefit, you can then also use these relations in the other direction, and ask for example: "Which initial counter values, if any, yield a given value when incremented?", or even more generally: "For which arguments does this relation even hold?"

Answer 2

Here is something that sort of does what you are trying to achieve:

?- X0 = 0 /* init */, succ(X0, X1) /* inc */, succ(X1, X2) /* inc */.
X0 = 0,
X1 = 1,
X2 = 2.

The init is just giving the variable a value, incrementing is done with succ/2, and the getval is implicit.

However, as I already said in the comment, consider your use case! If you are trying to keep track of how deep inside a loop you are, it is perfectly fine to do it with succ/2 or even following the suggestion by @mat.

So, to count the number of foos in a list:

list_foos([], 0).
list_foos([X|Xs], N) :-
    (   dif(X, foo)
    ->  list_foos(Xs, N)
    ;   list_foos(Xs, N0),
        succ(N0, N) % or: N0 + 1 #= N
    ).

You should try out both succ(N0, N) and N0 + 1 #= N to see how you can use them when either one or both of the arguments to list_foos/2 are not ground.

If, however, you need to maintain a global state for some reason: say, you are dynamically changing the database and you need to generate an increasing integer key for a table. Then, you should consider the answer by @coredump. Keep in mind that it is not super easy to write code that runs on any Prolog implementation once you start using "global" variables. One attempt would be to use the predicates for manipulating the database:

:- dynamic foocounter/1.

initfoo :-
    retractall(foocounter(_)),
    assertz(foocounter(0)).

incrfoo :-
    foocounter(V0),
    retractall(foocounter(_)),
    succ(V0, V),
    assertz(foocounter(V)).

And then, you can now count with a global state (it does not need to be in a conjunction like your example use):

?- initfoo.
true.

?- incrfoo.
true.

?- incrfoo.
true.

?- foocounter(V).
V = 2.

This is perfectly valid code but there are many pitfalls, so use with care.

Answer 3

I would use ECLiPSe's non-local variables:

init :- setval(counter, 0).
increment :- incval(counter).
get_counter(V) :- getval(counter, V).

Your implementation might provide something similar. In SWI-prolog, it seems that the same can be achieved with nb_setval (non-backtrackable setval).