Step 4: Axioms 🧾
In imperative programming, we bring our program to life with procedures that implement some particular algorithm. In contrast, ALM is completely declarative - we state what must always be true, and the Flamingo runtime makes it so (or the Flamingo compiler explains why it can't). Axioms are the rules for what must always be true.
There are four kinds of axioms:
Facts, which hold true unconditionally. The syntax is a function expression with a period, e.g.:
f(x) = y.State constraints, which say, e.g., "if f(X) is true in given state, then g(X) is also true in that same state". These have the syntax[1]:
```g(X) if f(X).```Causal laws, which say, e.g., "if f(X) is true in a given state, and Y occurs, then g(X) is true in the next state". These have the syntax:
```occurs(Y) causes g(X) if f(X).```Executability conditions, which say "if a given condition is true in a given state, then it is impossible for a given action to occur in that state."
```impossible occurs(A) if [some condition].```(We'll cover executability conditions more in the next section).
This syntax might be strange at first, but will make sense with a few more examples. Let's write out the axioms of our fruit and basket system (in plain English first):
- Golden Delicious and Granny Smith apples are good for baking.
- The basket is full if there are three distinct fruits in it.
- You can bake a pie if you have two apples that are good for baking.
- When you put a fruit in the basket, it becomes in the basket.
💡 Always write your axioms out in plain English first. You don't really know what you're writing until you've done so, and converting it to ALM's syntax afterwards is usually trivial. Always write it out! Always!
The first axiom represents two facts about varieties of apples. The syntax is pretty straight forward:
The next axiom is a state constraint. In ALM's syntax:
A few things of note:
- Identifiers that begin with an uppercase letter stand for variables. These will try to
match any value that fits in that "position" - e.g, in this example,
X
,Y
, andZ
all stand forfruits
since, in our function declaration forin_basket
, the first parameter isfruits
. - Different variables do not automatically represent different values. Thus, we must explicitly
compare the fruits
X
,Y
, andZ
with the!=
operator to ensure they are truly distinct. - Boolean functions are so common in ALM that they have built-in shorthands. Any function
like
f(x) = true
can be written as justf(x)
, and any expressionf(x) = false
as-f(x)
. So the idiomatic syntax for the first axiom is as follows [2]:
Our third axiom, also a state constraint, is quite similar:
The last axiom, a causal law, is a bit different:
This ALM axiom would read something like this in English:
"When action A
occurs, it causes Fruit
to be in_basket
if
A
is an instance of the put_fruit_in_basket
action AND
the selected_fruit
of A
is Fruit
."
The instance
function is a built-in static function that returns
true if the first argument is an instance of the sort given in
the second argument (or a transitive subsort).
The instance
function is extremely useful - you can use it do all kinds
of cool object-oriented tricks for modular goodness. That said, we'll
leave the fancier stuff for later examples.
That's all the axioms of our fruit and basket system. In fact, that's the whole system! Let's the see the whole program all together:
The syntax of logic programming takes practice. But note something important: each axiom has a very straightforward reading in English that is very similar to its original formulation in English. This is what Flamingo is all about: reducing the gap between informal specification (in English) and the formal specification (in a programming language). This leads to more simpler, more compact, and easier-to-maintain code.
[1]: While it's sometimes it's more natural in English to say "if [condition], then [conclusion]", Flamingo follows decades of logic programming tradition and puts the conclusion first.
[2]: This method of "counting" up to three is pretty tedious and doesn't scale - counting to 50 would require 50 variables and 1225 comparisons! This problem is solved by a construct called aggregates, which allow functions like min, max, sum, and count. These haven't been added to Flamingo yet, but are high on the priority list!