On Yacas programming


Example: implementing a formal grammar

To illustrate the use of rules, consider a theorem prover in a simple formal grammar. (The example is the "ABIN system" from the book: W. Robinson, Computers, minds and robots, Temple University Press, 1992. Warning: the book is about philosophy.)

Well-formed expressions consist of symbols A, B, I, N and are either

This defines a certain set of well-formed expressions (statements of the ABIN language); for example, NBII is a statement of the language but AB is not. The truth/falsehood interpretation of the ABIN language is the following. All well-formed expressions starting with NB are interpreted as true statements (they are "axioms" of the system). In addition, there is one deduction rule allowing one to prove "theorems":

Thus, NABIBI can be proved starting from the axiom NBI, but NANBB cannot be proved. The task at hand is to decide whether a given sequence of symbols is a provable statement of the ABIN language.

(The idea behind this interpretation is to assume that all B, BI etc. are some false statements that one could denote "B0", "B1" according to the number of "I" symbols; "N" is the logical Not and "A" is the logical And. Then the statement NABIB would mean "it is false that both B0 and B1 are true" and NANBB would mean "it is false that both B0 and negation of B0 are true". The NANBB statement is true in this interpretation but the deductive system of ABIN is too weak to obtain its proof.)


Implementation using predicates

The easiest way to model the ABIN language in Yacas is by using predicates. Our goal will be to define a predicate IsProvable(x) that will return True when x is a provable ABIN statement and False otherwise. We shall define IsProvable(x) recursively through several auxiliary predicates. Naturally, we would like to have a predicate to test well-formedness: IsExpr(x). It is necessary also to have predicates for B-expressions, N-expressions and A-expressions, as well as for axioms and theorems. We might implement expressions by lists of symbols, e.g. {"B", "I"} and begin to code by

IsExpr(x_IsList) <-- IsBExpr(x) Or
  IsNExpr(x) Or IsAExpr(x);
IsProvable(x_IsList) <-- IsAxiom(x) Or
  IsTheorem(x);
IsAxiom(x_IsList) <-- IsNExpr(x) And
  IsBExpr(Tail(x));

The definitions of IsBExpr(x) and IsNExpr(x) are simple recursion to express the rules 1 and 2 of the ABIN grammar. Note the use of Take to create a copy of a list (we'd better not modify the value of x in the body of the rule).

10 # IsBExpr({}) <-- False;
10 # IsBExpr({"B"}) <-- True;
20 # IsBExpr(x_IsList) <-- x[Length(x)]="I"
  And IsBExpr(Take(x, {1, Length(x)-1}));

10 # IsNExpr({}) <-- False;
20 # IsNExpr(x_IsList) <-- x[1] = "N" And
  IsExpr(Tail(x));

The predicate IsAExpr(x) is a little bit more complicated because our rule 3 requires to find two well-formed expressions that follow A. Also, for proving theorems we need to be able to extract the first of these expressions. With this in mind, we define another auxiliary function, FindTwoExprs(x), that returns the results of search for two well-formed expressions in the list x. The return value of this function will be a pair such as {True, 3} to indicate that two well-formed expressions were found, the first expression being of length 3. We shall use a For loop for this function:

FindTwoExprs(x_IsList) <-- [
 Local(iter, result);
 For( [ iter:=1; result:=False; ],
  iter < Length(x) And Not result,
    iter:=iter+1 )
   [
    result := IsExpr(Take(x, iter))
     And IsExpr(Take(x, {iter+1,
	   Length(x)}));
   ];
 {result, iter-1};
];

Now we can define the remaining predicates:

10 # IsAExpr(x_IsList)_(Length(x) <= 1)
  <-- False;
20 # IsAExpr(x_IsList) <-- x[1] = "A" And
  FindTwoExprs(Tail(x))[1];

IsTheorem(x_IsList) <-- If(IsNExpr(x) And
  IsAExpr(Tail(x)) And IsProvable(
    Concat({"N"}, Take(Tail(Tail(x)),
   FindTwoExprs(Tail(Tail(x)))[2]) ));

The ABIN language is now complete. Let us try some simple examples:

In> IsExpr({"A","B"});
Out> False;
In> IsExpr({"N","B","I"});
Out> True;
In> IsAxiom({"N","B","I"});
Out> True;
In> IsTheorem({"N","B","I"});
Out> False;
In> IsProvable({"N","B","I"});
Out> True;
In> IsProvable({"N","A","B","I","B"});
Out> True;

It is somewhat inconvenient to type long lists of characters. So we can create an interface function to convert atomic arguments to lists of characters, e.g. AtomToCharList(BII) will return {"B","I","I"} (provided that the symbol BII has not been given a definition). Then we define a function ABIN(x) to replace IsProvable.

AtomToCharList(x_IsAtom) <-- [
  Local(index, result);
  For( [ index:=Length(String(x));
     result:={}; ],
   index > 0, index:=index-1 )
   Push(result, StringMid(index, 1,
     String(x)));
  result;
];
Holdarg(AtomToCharList, 1);
ABIN(x) := IsProvable(AtomToCharList(x));

In> AtomToCharList(NBII);
Out> {"N", "B","I","I"};
In> ABIN(NANBB);
Out> False;

It is easy to modify the predicates IsTheorem() and IsAxiom() so that they print the sequence of intermediate theorems and axioms used for deriving a particular theorem. The final version of the code is in the file examples/ABIN.ys. Now we can try to check a "complicated" theorem and see an outline of its proof:

In> ABIN(NAAABIIBIBNB);
Axiom {"NBII"}
Theorem NABIIBI derived
Theorem NAABIIBIB derived
Theorem NAAABIIBIBNB derived
Out> True;


Creating plugins for Yacas


Introduction

Yacas supports dynamical loading of libraries ("plugins") at runtime. This allows to interface with other libraries or external code and support additional functionality. In a Yacas session, plugins are seen as additional Yacas functions that become available after a plugin has been loaded. Plugins may be loaded at any time during a Yacas session.

Currently, plugins are implemented as ELF dynamic libraries (or "shared objects", .so) under Linux. As of version 1.0.48, plugins are not yet supported on other platforms.

Plugins currently have to be written in C++ and require certain include files from the Yacas source tree. A plugin may be compiled as a shared object after Yacas itself has been compiled and installed successfully.


An example plugin

Here is what we need to do to make a new plugin:

// FILE: func1.h
double func1_cc (double x, double y);

// FILE: func1.cc
#include "stubs.h"	// required
#include "func1.h"	// our exported API

#include 
// we need math.h for sin()
double func1_cc (double x, double y) {
  return sin(x/y);
}

For our simple plugin, we shall only need a few lines of code in the Yacas stub:

/* FILE: func1_api.stub */
Use("cstubgen.rep/code.ys");

/* Start generating a C++ stub file */
StubApiCStart();

/* Write some documentation */
StubApiCRemark("This function computes
  beautiful waves.");

/* define a plugin-specific include file */
StubApiCInclude("\"func1.h\"");

/* Declare a plugin-specific function */
StubApiCFunction("double","func1","Func1",
  { {"double","x"},{"double","y"}});

/* generate a C++ stub file
  "func1_api.cc" */
StubApiCFile("func1_api");

Another example of a Yacas stub is found in the file plugins/example/barepluginapi.stub of the source tree.

yacas -pc func1_api.stub

c++ -shared -I/usr/local/include/yacas/
  -I/usr/local/include/yacas/plat/linux32/
  -Wl,-soname,libfunc1.so -o libfunc1.so
  func1.cc func1_api.cc

If compilation succeeds, the dynamic library file libfunc1.so is created. This is our plugin; now it could be installed into the Yacas plugin path (/usr/local/share/yacas/plugins/) or kept in the working directory.

In> DllLoad(FindFile("./libfunc1.so"));
Out> True;

The FindFile() function will help locate the Yacas path; we need to use it because DllLoad() requires a full path to the library file. Alternatively, if the plugin file were kept in the Yacas working directory, we could have used the command DllLoad("./libfunc1.so").

In> Func1(2,3);
Out> 0.61837;
When we are finished using the function, we might unload the DLL:

In> DllUnload("./libfunc1.so");
Out> True;


A dynamically generated plugin

Since Yacas can load plugins at runtime, why not have them generated also at runtime? Here is how we could dynamically create plugin functions to speed up numerical calculations.

Suppose we had a numerical function on real numbers, e.g.

In> f(x,y):=Sin(2*x*Pi)+Sqrt(2)*Cos(y*Pi);
Out> True;

We can generate some C++ code that calculates this function for given floating-point arguments (not for multiple-precision numbers):

In> CForm(f(x,y));
Out> "sin(2 * x * Pi) + sqrt(2)
* cos(y * Pi)";
(Note that we would need to define Pi in the C++ file.)

Now it is clear that all the steps needed to compile, link, and load a plugin that implements f(x,y) can be performed automatically by a Yacas script. (You would need a C++ compiler on your system, of course.)

This is implemented in the function MakeFunctionPlugin() (see file unix.ys in the addons/ subdirectory). To use it, we might first define a function such as f(x,y) above and then call

In> MakeFunctionPlugin("fFast", f(x,y));
Function fFast(x,y) loaded from
  ./plugins.tmp/libfFast_plugin_cc.so
Out> True;
In> fFast(2,3);
Out> -1.41421;

Now we can use the function fFast(x,y) which is implemented using an external plugin library. The function MakeFunctionPlugin() assumes that all arguments and return values of functions are real floating-point numbers. The plugin libraries it creates are always in the plugins.tmp/ subdirectory of current working directory and are named like libNNN_plugin_cc.so.

If MakeFunctionPlugin() is called again to create a plugin function with the same name (but different body), the DLL will be unloaded and loaded as necessary.