# Negation as failure

 This is Literate TwelfCode: hereStatus: %% OK %% Output: here.

Negation as failure. It is possible to do negation-as-failure using Twelf's logic programming engine, with the use of %deterministic. As an example, we will define logic programs to compute the less-than and greater-than-or-equal-to functions. The less-than function will be defined in a standard way. The greater-than-or-equal-to function will be defined using a negation-as-failure interpretation of the less-function.

### Definitions

Natural numbers and booleans.

```nat	: type.

z	: nat.
s	: nat -> nat.

bool	: type.

true	: bool.
false	: bool.```

less is defined inductively in the standard way.

```less	: nat -> nat -> type.
%mode less +D1 +D2.

less/z	: less z (s _).
less/s	: less (s N1) (s N2)
<- less N1 N2.```

We will need a judgment that tests whether a boolean is false in order to use negation-as-failure.

```isfalse	: bool -> type.
%mode isfalse +D.

isfalse/i	: isfalse false.```

### Coding negation-as-failure

We define a logic program that when given two numbers returns true if the first is less than the second, and false otherwise. We use %deterministic to make the logic programming engine commit to the first solution it finds.

```less-bool	: nat -> nat -> bool -> type.
%mode less-bool +D1 +D2 -D3.
%deterministic less-bool.```

Because the less-bool/true case is first, it will attempt to find a proof that the first number is less than the second.

```less-bool/true	: less-bool N1 N2 true
<- less N1 N2.```

Because of the %deterministic declaration, when searching for a proof of less N1 N2 B, only executes when less-bool/true fails. However, because of pattern matching a search for a proof of less N1 N2 false always succeeds.

`less-bool/false	: less-bool N1 N2 false.`

We will now define gte using less-bool. It has only one rule, which makes a call to less-bool N1 N2 B. It is important to make sure that the result B is not directly identified as false so that it executes less-bool in the appropriate order. We use the call to isfalse B to verify that the output really is false.

```gte	: nat -> nat -> type.
%mode gte +D1 +D2.

gte/i	: gte N1 N2
<- less-bool N1 N2 B
<- isfalse B.```

We can use a number of %solve declarations to test our less and gte judgments.

```%solve deriv : less (s z) (s (s z)).
%solve deriv1 : gte (s (s z)) (s z).
%solve deriv2 : gte z z.
% solve deriv3 : gte (s z) (s (s z)). % should fail```

It is important to note that while these definitions work as intended as logic programs, proving appropriate meta-theorems about judgments that use negation as failure is problematic or impossible.

Note from dklee: I had to run home to take care of some stuff. I will finish documenting this later in the evening.