Markdown for LLMs

Exercise 17. A power to extend a visit

The source Markdown for this article. Copy it into your assistant or download it as a text file.

# Exercise 17. A power to extend a visit

An exercise for the [ban, liberty, power, and
immunity](/tutorials/modalities/) page. On the page the reader may
request a visit extension. Who may grant it, the page does not say.

**Setup.** Write the director's power to extend a visit: it is exercised
by an extension order, valid only upon the reader's request, and the
effect is the "visit extended" fact. An order with a request yields
`TRUE_ONLY` on the extension question; an order without a request yields
`NEITHER` and a `POWER_INVALID_EXERCISE` problem; a request without an
order yields `NEITHER` with no problems.

**Hint.** A power has four parts: who, over whom, exercised by what, and
valid under which condition. The effect creates a fact rather than
deriving it.

Below is the solution. Try it yourself first.

## Solution

```law
language "law.core" version "0.2";
package tutorial.archive version "0.7.1";
namespace "urn:law:tutorial:archive";

entity Person;
entity Official;

relation in_researcher_registry(p: Person) kind institutional;
relation visit_registered(p: Person, from: Date, to: Date) kind empirical { key(p); }
relation requests_extension(p: Person) kind empirical;
relation director(d: Official) kind institutional;
relation extension_order(d: Official, p: Person) kind empirical;
relation visit_extended(p: Person) kind institutional;
```

The power:

```law
rule ExtensionPower strict {
    for d: Official;
    for p: Person;
    for from, to: Date;
    when director(d) and visit_registered(p, from, to);
    then power ExtendVisit {
        holder d;
        over p;
        exercise extension_order(d, p);
        valid_when requests_extension(p);
        effect create(visit_extended(p));
    };
}
```

Three condition outcomes are three different power states. An order with
a request: the exercise is valid, the effect materialised. An order
without a request: the exercise exists, the validity condition fails, and
the engine names it a problem rather than staying silent: the director
acted but could not. A request without an order: the power exists but is
unexercised, and that is no problem but ordinary silence.

## Check

| Facts beyond registry, director, and visit | `visit_extended(ivanova)` | Problems |
|---|---|---|
| order, request | `TRUE_ONLY` | none |
| order | `NEITHER` | `POWER_INVALID_EXERCISE` |
| request | `NEITHER` | none |

Removing the `valid_when` line must bring the `LDC-E1305`
refusal: a power's validity condition is mandatory.

What the exercise teaches. A power differs from an ordinary norm in
holding an **invalid exercise** — a situation where the authority acted
outside the condition. A norm with an "order and request" body would give
the same `TRUE_ONLY`, but for it an order without a request would be mere
silence, and the consumer would never learn an order existed at all.