The substance program tells Penrose what objects and relations to draw. In the set-theory example, for example, we can have the following substance program:
Set A, B, C IsSubset (A, C) IsSubset (B, C) Not (Intersecting (A, B)) AutoLabel All
The first line declares the objects that are to be drawn, the last line tells Penrose to automatically label the objects based on their names. All other lines invoke the predicates defined in the domain schema to declare relations between objects.
Notably, like the domain schema, the substance program does not contain any instructions about how, say, a
Set must be rendered, or how the relation
IsSubset should be reflected in the diagram. The substance program only declares the existence of these objects and relations, whereas the style schema shows how these objects and relations can be drawn.
Formally, a substance program can contain five types of statements.
An object declaration declares the existence of an object, and specify its type:
type_nameis a type that is declared in the domain schema; and
object_nameis the name given to this object, which can be referred to in other parts of the substance program.
Once an object is declared, we can refer to it using
object_name, which becomes a substance variable.
Penrose also allows users to declare multiple objects of the same type at the same time:
type_name object_name_1, object_name_2, ...
This is equivalent to declaring the objects sequentially and separately.
We can apply the predicates (first defined in the domain schema) in our substance program simply by invoking it. The syntax is
predicate_nameis the name of the predicate, as declared in the domain schema; and
argument_listis a comma-separated list of objects (defined earlier in the substance program) or other predicate applications.
The types of the substance objects in
argument_list must match the types of the arguments as declared in the domain schema, allowing for subtypes to match their supertypes. Furthermore, if the domain argument type is
Prop, then the substance argument should be a predicate application.
We illustrate these rules with some examples. Suppose we have domain schema
type Atom type Hydrogen <: Atom type Oxygen <: Atom type NotAnAtom predicate Bond (Atom, Atom) predicate Not (Prop)
and substance object declarations
Hydrogen H Oxygen O Atom A NotAnAtom NA
Function and Constructor Applications
In Penrose, functions and constructors behave equivalently. There are two ways of invoking a function or constructor. The first way is
object_name := function_constructor_name (argument_list)
which requires object with
object_name to be declared beforehand in the substance program. The second way combines the declaration of the object and the invocation of the function into one statement:
type_name object_name := function_constructor_name (argument_list)
The rules for
argument_list remain the same as in predicate applications. We further require that the output type of the function or constructor must match the type of
object_name, up to subtyping. That is, if the function outputs type
object_name has type
B, then if
A is a subtype of
B, then the assignment is valid.
Each declared object has a label, which can be accessed in the style schema. In the substance program, the labeling statements specify the value of these labels.
There are three types of labeling statements:
AutoLabel All: this statement assigns the label of each object in the substance program to be its name. For instance, if we declare object
Atom A, then
AutoLabel Allwill automatically assign
Aas its label;
Label object_name label_value: this statement manually assign object
object_name's label to be
NoLabel object_list: this statement ensures that objects in
object_listdo not have a label.
If an object has an assigned label, then in the style schema, we can access the object's
Comments are ignored by the Penrose engine. In the substance program, comments are declared using double dashes:
-- this is a comment