Exercise 17. A power to extend a visit

An exercise for the ban, liberty, power, and immunity 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

Arxo 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:

Arxo 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.