Substance Usage #

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.

Object Declarations #

An object declaration declares the existence of an object, and specify its type:

type_name object_name

where

• type_name is a type that is declared in the domain schema; and
• object_name is 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.

Predicate Applications #

We can apply the predicates (first defined in the domain schema) in our substance program simply by invoking it. The syntax is

predicate_name (argument_list)

where

• predicate_name is the name of the predicate, as declared in the domain schema; and
• argument_list is 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

Then,

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 A and object_name has type B, then if A is a subtype of B, then the assignment is valid.

Labeling Statements #

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 All will automatically assign A as its label.
• Label object_name label_value: this statement manually assign object object_name's label to be label_value. There are two types of label_values:
  • A math label is a TeX string delimited by dollar signs, e.g., Label p $p_0$
  • A text label is a plain-text string delimited by double quotes, e.g., Label p "a point".
• NoLabel object_list: this statement ensures that objects in object_list do not have a label.

If an object has an assigned label, then in the style schema, we can access the object's label property.

Comments #

Comments are ignored by the Penrose engine. In the substance program, comments are declared using double dashes:

-- this is a comment