Backup diff of Example Programs vs current(No. 13)

The added line is THIS COLOR.
The deleted line is THIS COLOR.
#author("2022-04-26T18:49:56+09:00","default:LMNtal","LMNtal")
//[[Documentation]]

*Example Programs
*Example Programs [#xab918dc] 

A number of example programs, including
A number of example programs are included in the distribution of [[LaViT>http://www.ueda.info.waseda.ac.jp/lmntal/lavit/index.php?Download]] and can be found in the "demo" folder.  They include:

-those with just one or a few rules,
-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.),
-those using LMNtal Java's GUI,
-programs with just one rewrite rule &color(#00d){(sorting, factorial, Tower of Hanoi, etc.)};,
-encodings of various calculi &color(#00d){(propositional logic, Petri Nets, lambda calculus, ambient calculus, etc.)};,
-state-space search using SLIM's nondeterministic execution &color(#00d){(typical AI problems etc.)};,
-model checking &color(#00d){(distributed and concurrent algorithms, protocol verification, etc.)};,
-graph visualization using UNYO-UNYO &color(#00d){(fullerenes (C60) etc.)};, and
-those using LMNtal Java's GUI.

and so on, can be found in 
[[''this directory'' (click here)>http://www.ueda.info.waseda.ac.jp/lmntal/demo/]].
They can be found also in [[''this folder'' (click here)>http://www.ueda.info.waseda.ac.jp/lmntal/demo/]].  Furthermore, 

-The 'ltl' subdirectory contains both programs and LTL formulas to model-check them.
-The 'unyo' subdirectory contains programs to be run under the UNYO-UNYO visualizer.
-The 'wt' subdirectory contains programs to be run with the LMNtal window toolkit of LMNtal Java.
-The [[''ltl'' subfolder>http://www.ueda.info.waseda.ac.jp/lmntal/demo/ltl/]] contains both programs and LTL formulas to model-check them.
-The [[''unyo'' subfolder>http://www.ueda.info.waseda.ac.jp/lmntal/demo/unyo/]] contains programs to be run under the Graphene or UNYO-UNYO visualizer.
//-The [[''wt'' subfolder>http://www.ueda.info.waseda.ac.jp/lmntal/demo/wt/]] contains programs to be run with the LMNtal window toolkit of LMNtal Java.

All these programs are included in the latest distribution of [[LaViT>http://www.ueda.info.waseda.ac.jp/lmntal/lavit/index.php?Download]].
Let us introduce some simple examples.

Let us introduce some simple examples below.
**List Concatenation [#c822cef6]

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

Lists formed with c(cons) and n(il) 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).

Enter those rules with the following initial state:
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 abbreviation scheme''' explained [[here>Syntax]].  By further applying the term abbreviation scheme and the Prolog-like list syntax, list concatenation can be written also as:
The above initial state is written using the '''term notation''' explained [[here>Syntax]].  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.

**Self-Organizing Loops
**Greatest Common Divisor [#v8af293e]

Ten agents with two free hands are going to hold hands with others.
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:

 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).
 
 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 [#x13c986d]

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: Twenty possible final configurations.  You can randomly compute them by running the program using LMNtal Java with the ''-s'' (shuffle) option, or running SLIM with the ''-nd'' (nondeterministic execution) option.  LaViT's ''StateViewer'' will show you a state transition diagram of the problem.
RESULT: There are 20 possible final configurations, which can be computed by running SLIM/LaViT with the ''--nd'' (nondeterministic execution) option.  LaViT's ''State&#86;iewer'' shows a state transition diagram of the problem.

**Vending Machine
**Vending Machine [#uebe51a2]

Two customers with different amounts of coins and hunger
Two customers with different hunger and the numbers of coins
are buying chocolates from a vending machine.
Each chocolate costs three
and only two kinds of coins are considered: one and five.
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, buying 2 chocolates
 {customer,b,five,hunger}.                 % Customer b has $5, buying 1 chocolate
 {vending,choco,choco,choco,one,one}.      % Vending machine has 3 chocolates
 {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,choco,one,one} :-
    {customer,$c,choco,one,one}, {vending,$v,five}.
 {customer,$c,hunger,one,one,one}, {vending,$v,choco} :-
    {customer,$c,choco}, {vending,$v,one,one,one}.
 {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}.

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

 RESULT 1:
   {customer,a,choco,choco,one},
   {customer,b,choco,one,one},
   {vending,five,five,one}, <RULES>
 RESULT 2:
   {customer,a,hunger,hunger,five,one,one},
   {customer,b,choco,one,one}, 
   {vending,choco,choco,five}, <RULES>
 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>

Observe that applying each rule preserves
the total amount of coins and chocos within the system.
//Observe that applying each rule preserves the total number of coins and chocolates within the system.