Example Programs

Example Programs †

A number of example programs are included in the distribution of LaViT and can be found in the "demo" folder. They include:

programs with just one rewrite rule (sorting, factorial, Tower of Hanoi, etc.),
encodings of various calculi (propositional logic, Petri Nets, lambda calculus, ambient calculus, etc.),
state-space search using SLIM's nondeterministic execution (typical AI problems etc.),
model checking (distributed and concurrent algorithms, protocol verification, etc.),
graph visualization using UNYO-UNYO (fullerenes (C60) etc.), and
those using LMNtal Java's GUI.

They can be found also in this folder (click here). Furthermore,

The ltl subfolder contains both programs and LTL formulas to model-check them.
The unyo subfolder contains programs to be run under the Graphene or UNYO-UNYO visualizer.

Let us introduce some simple examples.

↑

List Concatenation †

Lists formed with c (cons) and n (nil) constructors can be concatenated using the following two rules:

append(X,Y,Z), n(X)      :- Y=Z.
append(X,Y,Z), c(A,X1,X) :- c(A,Z1,Z), append(X1,Y,Z1).

Let them rewrite the following initial state:

append(c(1,c(2,c(3,n))),c(4,c(5,n)),result).

RESULT: result(c(1,c(2,c(3,c(4,c(5,n)))))) with the two rules above.

The above initial state is written using the term notation explained here. By using the term notation and the Prolog-like list syntax, the program can be written also in a functional style as:

Z=append([],    Y) :- Z=Y.
Z=append([A|X1],Y) :- Z=[A|append(X1,Y)].
result = append([1,2,3],[4,5]).

RESULT: result=[1,2,3,4,5] with the two rules above.

↑

Greatest Common Divisor †

The following program computes the GCD of two numbers using one rule, based on the fact that the GCD won't change by replacing the larger number with the difference between the two numbers:

n=100, n=72.
n=$x, n=$y :- $x>$y | n=$x-$y, n=$y.

RESULT: n=4, n=4 with the rule above.

See Built-in Types and Guards for how to handle numbers in LMNtal.

↑

Self-Organizing Loops †

Ten agents, each with two free hands, are going to hold hands with others. Is it possible that some agent is left alone?

a(free,free), a(free,free), a(free,free), a(free,free), a(free,free),
a(free,free), a(free,free), a(free,free), a(free,free), a(free,free).
a(X,free),a(free,Y) :- a(X,C),a(C,Y).

RESULT: There are 20 possible final configurations, which can be computed by running SLIM/LaViT with the --nd (nondeterministic execution) option. LaViT's StateViewer shows a state transition diagram of the problem.

↑

Vending Machine †

Two customers with different hunger and the numbers of coins are buying chocolates from a vending machine. Each choc(olate) costs three and only two kinds of coins are accepted: one and five.

{customer,a,five,one,one,hunger,hunger}.  % Customer a has $7 and wants to buy two chocs
{customer,b,five,hunger}.                 % Customer b has $5 and wants to buy one choc 
{vending,choc,choc,choc,one,one}.         % Vending machine has 3 chocs

{customer,$c,hunger,five}, {vending,$v,choc,one,one} :-
   {customer,$c,choc,one,one}, {vending,$v,five}.
{customer,$c,hunger,one,one,one}, {vending,$v,choc} :-
   {customer,$c,choc}, {vending,$v,one,one,one}.

SLIM/LaViT with --nd will compute two possible final states:

RESULT 1: {customer,a,choc,choc,one},
          {customer,b,choc,one,one},
          {vending,five,five,one}, <RULES>
RESULT 2: {customer,a,hunger,hunger,five,one,one},   // Oops!
          {customer,b,choc,one,one}, 
          {vending,choc,choc,five}, <RULES>

MENU