Say you’re working in a logic language, and you want to encode a reaction like for every turn, draw a card:

turn
---------
draw-card.

The problem is that we haven’t identified the turns; we expect to have something like turn 1, turn 2, … but this rule runs once. Instead, suppose each fact representing an event/episode like this has a temporal id:

turn T
-------------
draw-card ???.

So each turn and each draw-card should have an id, but how do we fill in the blank? We could just re-use T, but this seems wrong; what if we draw more than once per turn? Probably we should have some way to get a fresh id for the new event.

We could keep track of a global counter, and each time we create a new episode we read it and increment it. But now we’ve left the domain of pure, monotone logic programs. We’ve added something to the runtime, and the id values will depend on evaluation order; we’re not just deriving.

Instead, we could transform T somehow, i.e. f(T). We want to ensure that f has a few properties:

• it should be injective;
• it should be a true function (side-effect free);
• its output values shouldn’t collide with any value coming from another rule (logic programs usually have more than one rule).

So, let’s assume this rule actually has a globally unique name (chosen at compile time), and use that name as a data constructor:

turn T
----------------------- [turn-draw]
draw-card (turn-draw T).

Now the compound term turn-draw T uniquely identifies the draw-card event triggered by this rule. The rule remains idempotent, and the id doesn’t depend on the consequences of other rules.

Complex Bodies

There’s a little more to it than this. Say we have this rule:

in-play C, name C goons, buy-card T
----------------------------------- [goons-in-play]
score-point ???

That is, for each copy of Goons in play, each time you buy a card, you score a point. Point-scoring is an event that needs an id; it should get a different one per buy/goons pair. The simplest thing to do is just bind the value of every variable in scope:

in-play C, name C goons, buy-card T
----------------------------------- [goons-in-play]
score-point (goons-in-play C T)

Complex Heads

Say we want to have two responses:

draw-card T
-------------------------------- [draw-card]
reveal-top ???, move-to-hand ???.

We need two fresh ids, so we just enumerate the positions where they occur:

draw-card T
---------------------------- [draw-card]
reveal-top   (draw-card T 1),
move-to-hand (draw-card T 2).

Summary

In summary, we encode fresh timestamps as terms using two ingredients:

• The static part: the name of a rule and a position inside its conclusion.
• The dynamic part: all the values bound by the body.

Skolemization

This is basically the same thing as the conversion process called skolemization, named after logician Thoralf Skolem. When you have a first-order formula like \forall X,Y \exists Z~ p(X,Y,Z), skolemization produces the formula \forall X,Y~ p(X, Y,f(X, Y)), which is satisfiable if and only if the other is. Note that instead of having this variable Z that happens to be existentially quantified after two universally quantified variables, what we have instead is a function symbol f that explicitly states its dependencies.

The correspondence with the above method is like this:

• formula ~ rule
• existentially quantified variable inside a formula ~ fresh timestamp in rule head
• universally quantified var outside of existential ~ variable bound in the body

and it’s quite literal: you can read a deduction rule as for all instantiations of the body, there exists some fresh timestamps at which these new events occur.

“Everything That Ever Happened”?

A funny thing happens: the move-to-hand id refers to the draw-card id, which refers to the turn id. Suppose we initiate turns like this:

--------------- [first-turn]
turn first-turn.

turn T
------------------ [next-turn]
turn (next-turn T).

Now it’s clear that each turn’s id is a natural number: one plus the id of the previous turn (the constructors for zero and successor just have non-standard names).

So, starting from the id of any event, you can trace back through all the rules, prior events, and data values that were causally related to it.¹ All we wanted were fresh id values, but as a bonus we got some runtime data that a programmer might find useful. I suspect there is some simple theorem lurking here that could be stated about this being a freely-generated model of those requirements I stated initially, but I don’t know what it is. It also resembles how the Yoneda embedding tells us any poset is equivalent to a collection of sets ordered by inclusion (an element maps to those elements less than it).

https://cutfree.net