# Reference¶

## Overview¶

Apilog is a logic programming language for documenting and testing RPC
interfaces. The language has three fundamental syntactical categories: *types*,
*expressions*, and *actions*. In addition, it has syntax for defining
predicates, APIs, issuing commands and more. Rather than giving a detailed
grammar for all the syntax up front, this document will take you on a tour
around the main concepts of Apilog, explaining some of the syntactical elements
on the go. It is work in progress and currently lacks a description how to
define data types as well as a deeper description of the semantics of the
language.

## Type system¶

The type system of Apilog is fairly standard and behaves like most polymorphic
type systems for functional programming. There are function types, written
using the function arrow syntax (`->`

) and there is a type for logical
formulas, called `prop`

. Then there is a bunch of simple data types such as
`string`

, `int`

, etc. There are also parameterised types besides functions
types. For example, the type of lists of integers is written `list int`

.
Moreover, since the type system is polymorphic, types can contain variables,
written using capitalized identifiers. For example, the type of a predicate
that checks for list membership can be written `A -> list A -> prop`

. Finally,
specification authors can declare new types, as we shall see later.

## Expressions¶

Expressions are similar to expressions in functional languages. Function
application is written `f x`

. The syntax for lambda abstraction is a bit
unusual, however. It is written `X\ e`

, where `X`

is the bound variable and `e`

is some expression.

## Actions¶

The action language is used to describe interactions with an API. It contains syntax for sequencing actions, running actions in parallel, making remote procedure calls, and testing the result of actions. However, apilog specifications can only directly use the syntax for making remote procedure calls. The rest of the action language is only used to describe the actions that Apilog took during testing, and can be shown in the user interface, but not written in the specification itself. Morever, even though actions is a separate syntactical category from expressions, actions can be wrapped as expressions (using a special expression syntax element). This wrapping makes it possible to define short-form constants that describe actions, and include actions in formulas. Specifications will mostly use short-form action expressions from the Apilog library, some of which are:

```
get : path -> list (tuple string string) -> action http_response
post : path -> list (tuple string string) -> string -> action http_response
put : path -> list (tuple string string) -> string -> action http_response
delete : path -> list (tuple string string) -> action http_response
```

The path arguments represent URI paths, the lists of tuples represent HTTP headers and the string arguments represent HTTP request bodies.

## Formulas and terms¶

The connectives in the Apilog logic are *encoded* as expression constants,
which means that logical formulas are simply expressions (of type `prop`

).
There are certain restrictions in place that prevent logical formulas from
quantifiying over logical formulas, in order to make the logic *first-order*.
For this reason we must also talk about *terms*, the subset of expressions that
does not contain formulas.

## Resource declarations¶

The concept of a *resource* is central to Apilog. A resource represents
something that exists in the system behind the API, and that can typically be
manipulated via the API. Resources are encoded as logical predicates (applied
to all their arguments). New such resource constants can be declared with the
`resource`

keyword, followed by a name and a type. Here is an example:

```
resource user : string -> prop.
```

The above declaration says that there is a predicate constant called `user`

with a string argument, and that this predicate (when applied to its argument
and used in a logical formula) represents a resource. In this example, the
string argument could represent the user name.

## Positive formulas¶

Positive formulas are used to generate data as well as to express pre- and post-conditions. They follow this abstract grammar:

where \(P\) stands for atoms and \(t\) for terms.

### Atoms¶

An atom is a non-logical constant applied to all its arguments. As such, it is
a formula that does not contain any logical constants. There are two kinds of
atoms: *resource atoms* and *built-in atoms*.

#### Resource atoms¶

In a resource atom, the constant must have been declared as a resource. For
example, if a constant `user : string -> prop`

has been declared, `user "x"`

would be a resource atom, which could represent the assumption that the user
named "x" exists in the system behind the API.

#### Built-in atoms¶

In a built-in atom, the constant refers to a procedure that is built-in to the
Apilog interpreter. An example of such a constant is ```
parse_json : string ->
json -> prop
```

.

### Multiplicative conjunction¶

\(\tensor\) is the multiplicative conjunction connective from linear logic. It
can be thought of as a version of "and" that can represent the simultaneous
occurence of resources. In the concrete syntax, it is written `,`

(comma), like
conjunction in Prolog. Also like in Prolog, interpretation proceeds
left-to-right.

### One¶

\(\one\) is the unit of \(\tensor\) from linear logic, and is written `one`

in the
concrete syntax. It represents the absence of resources and can be thought of
as a version of "true" from more standard logics.

### Additive disjunction¶

\(\adisj\) is the additive disjunction connective from linear logic. It can be thought of as a version of "or" that can represent non-deterministic choice between resources. It is written in the concrete syntax with ';' (semi-colon), like disjunction in Prolog.

When the Apilog interpreter finds this connective in a goal (pre-condition), it makes a randomized choice of which branch to try first, and performs chronological backtracking upon failure. It does not try to find multiple solutions.

When the Apilog intepreter finds this connective in a hypothesis (post-condition), it tries the first branch and then the second. If there is more than one solution, it yields a "fatal error", indicating an error in the specification. In effect, specifications are required to be deterministic.

### Zero¶

\(\zero\) is the unit of \(\adisj\) from linear logic and is written `zero`

in the
concrete syntax. It represents a resource that cannot be produced and can be
thought of as a version of "bottom" or "false" from more standard logics.

### Existential quantification¶

\(\exists x.A^+\) is existential quantification. In concrete syntax, it can be
written using the built-in constant `exists : (A -> prop) -> prop`

. For
example: `exists (X\ e)`

where `e`

is some expression typically containing `X`

.

The quantified variable must be of term type.

### Equality¶

\(=\) is term equality, written `=`

in concrete syntax.

### Recursion¶

Positive formulas can be *recursive* using the the fixed point combinator \(\mu\).
In the surface syntax, this combinator is not available. Instead, recursion is
achieved by making a definition that refers to itself. This self-reference is
then translated into an application of the fixed-point combinator.

## Negative formulas¶

Negative formulas are used to describe APIs. They follow this abstract grammar:

### Additive conjunction¶

\(\with\) is the additive conjunction connective from linear logic. It is used to
represent a (client-side) choice between APIs. It can be thought of as a
version of "and" from more standard logics, and is written `&`

in the concrete
syntax.

### Top¶

\(\top\) is the unit of \(\with\) from linear logic and is written `top`

in the
concrete syntax. It is used to represent the empty API and can be thought of as
version of "true" from more standard logics.

### Universal quantification¶

\(\forall x.A^-\) is universal quantification. In concrete syntax, it can be
written using the built-in constant `forall : (A -> prop) -> prop`

. For
example: `forall (X\ e)`

where `e`

is some expression typically containing `X`

.

The quantified variable must be of term type.

### Linear implication¶

\(\limp\) is the linear implication arrow from linear logic, written `-o`

in the
concrete syntax. It can be seen as a resource-aware version of logical
implication. The antecedent (the left argument) must be a *positive* formula,
which can contain resources, and the consequent (the right argument) must be a
*negative* formula. When a linear implication is used to prove its consequent,
the resources in the antecedent are *consumed*.

### Action modality¶

\(\langle a \rangle x.A^+\) is a modal formula that means that the formula \([t/x]A^+\) is true after action \(a\) has happened, if term \(t\) is the result of \(a\).

The concrete syntax is:

```
{a}f
```

where `a`

is an action of type `action r`

, and `f`

a function of type ```
r ->
prop
```

(more precisely, a function from the result of the action to a *positive*
formula). For example:

```
{get /users/U _ _ _}(R\ status 200 R, user U)
```

Resources in the formula returned by `f`

(like `user U`

in the above example)
are added to the set of assumptions about the system under test, after the
action `a`

is performed, during testing. Note that `status 200 R`

in this
example is not a resource atom, but a *defined* atom (which will be explained
later).

## Definitions¶

As alluded to earlier, Apilog allows *definitions* of contants. A definition is
a top-level statement that declares a new constant and assigns it a logical
formula. Internally, such atoms are substituted by their definitions which
explains why they are not present in the abstract syntax (as presented in the
sections on positive and negative formulas).

There are two kinds of definitions: *API definitions* and *predicate
definitions*.

### API definitions¶

API definitions are made with the `api`

keyword, like in the following example:

```
api get_user := user U -o {get /users/U _ _ _}(R\ status 200 R, user U).
```

The right hand side (right of `:=`

) is always a *negative* logical formula.

#### Variables and quantification¶

Any *unbound* and *capitalized* identifier in the formula (like `U`

in the
example) is implicitly *universally* quantified. I.e. there is a hidden forall-
quantifier for `U`

at the start of the formula in the example. Also, note that
in the example above, the variable `R`

is *not* implicitly quantified as it is
*bound* as an argument to an anonymous function.

#### API clauses¶

In the example above, the formula has a single application of the action
modality. Such a formula we call an *API clause*. We call the modal formula
the *head* of the clause and the antecedent of the linear implication the
*body* of the clause.

#### Combining APIs¶

APIs can be combined with the `&`

connective. I.e. one can write API
definitions that join multiple APIs together like this:

```
api main := get_user & delete_user.
```

One can also write multiple API clauses in one definition:

```
api main :=
user U -o {get /users/U _}(R\ status 200 R, user U) &
user U -o {delete /users/U _}(R\ status 200 R).
```

#### API clause restrictions¶

There are two restrictions on API clauses: they *must not overlap* and they
must have *atomic actions*.

##### Non-overlapping API clauses¶

Overlap between API clauses occur when there are two or more clauses with actions that can be "unified" i.e. which can be made equal using a specific substitution of variables. If this occurs, Apilog complains with an error message.

Note that the body of the clause has no effect on whether the heads actions are considered overlapping or not. The unification of head actions is attempted without looking at the bodies.

This restriction is similar to the behaviour of type class instance resolution in Haskell.

##### Atomic actions¶

Actions in API clauses must be atomic `rpc`

actions. If not, Apilog complains
with an error message.

##### Rationale¶

There are two reasons for these two restrictions.

1) If API clause are non-overlapping and contain only atomic actions, Apilog never needs to consider more than one API clause in its proof search after having made a remote procedure call.

2) With these restrictions, the actions serve well as documentation headings in the generated API documentation, because the resulting headings are guaranteed to be unique, and likely to be short and summary.

### Predicate definitions¶

Predicates can be defined by clauses, with `def`

-`by`

syntax. A type must be
declared and the clauses must be separated by vertical bars (`|`

).

Here is an example of a predicate that checks for list membership:

```
def elem : A -> list A -> prop by
| elem A [A|_]
| elem A [_|L] := elem A L.
```

The expression to the left of `:=`

is called a *head* and the expression to
the right a *body*, the latter which can be omitted. The head must be an atom
with the same predicate constant that is defined (`elem`

in this example). The
body can be any *positive* formula.

This clause-by-clause definition style mimics horn clauses. The same predicate could look like this in Prolog:

```
elem(A, [A|_]).
elem(A, [_|L]) :- elem A L.
```

Clause-by-clause definitions is just a form of syntactial sugar. The Apilog
interpreter always "desugars" the clauses into a function from the arguments of
the predicate to a single *positive* logical formula.

#### Existential quantification¶

All unbound capitalized identifiers in the clauses are implicitly
*existentially* quantified.

#### Recursion¶

A `def-by`

definition can refer to itself, i.e. it can be recursive. However,
Apilog does not yet support mutual recursion.

## Commands¶

Commands are top-level statements prefixed with `#`

, and cause things to
happen. In order to run tests, for example, you need to add a `#check`

command
(see below) to you specification.

### #baseuri¶

#### Syntax¶

```
#baseuri e.
```

where `e`

is an expression of type `string`

.

#### Meaning¶

Sets the base URI that will prefix each path during testing.

#### Example¶

```
#baseuri "https://httbin.org".
```

### #check¶

#### Syntax¶

```
#check e.
```

where `e`

is an expression of type `prop`

, i.e. a formula.
The formula must be *negative* (i.e. an API formula).

#### Meaning¶

Runs tests against the system at the base URI. In order to generate tests,
Apilog does proof search. This search is set up so that the positive API
formula in the argument to the command is put in the *unrestricted context* of
the hypothetical judgement to be proved, which means that Apilog is allowed to
use the API formula any number of times (i.e. it is not *restricted* to be used
linearly).

Any capitalized and unbound identifier in `e`

is implicitly universally
quantified.

#### Examples¶

```
#check {get /foo _ _}(R\ status 200 R).
```

```
#check api1 & api2.
```

### #query¶

#### Syntax¶

```
#check e.
```

where `e`

is an expression of type `prop`

, i.e. a formula.
The formula must be *positive*.

#### Meaning¶

Does proof search with the goal `e`

. Any capitalized and unbound identifier in
`e`

is implicitly existentially quantified.

#### Example¶

```
#query append "foo" "bar" S.
```