# DEONTIC

The type for regulative rules representing obligations, permissions, and prohibitions.

## Syntax

```l4
GIVETH A DEONTIC ActorType ActionType
ruleName MEANS
    PARTY actor
    MUST/MAY/SHANT/DO action
    WITHIN deadline
    HENCE consequence
    LEST breach
```

## Purpose

`DEONTIC` is L4's type for modeling legal obligations, permissions, and prohibitions. A DEONTIC value captures:

1. **Who** has the obligation/permission (`PARTY`)
2. **What** they must/may/must not do (`MUST`/`MAY`/`SHANT`/`DO`)
3. **When** it must occur (`WITHIN`)
4. **What happens** on compliance (`HENCE`)
5. **What happens** on breach (`LEST`)

The DEONTIC type is parameterized by two type arguments:

- **ActorType**: The type of parties who can act (e.g., `Buyer`, `Seller`)
- **ActionType**: The type of actions that can be performed (e.g., `deliver`, `pay`)

## Examples

**Example file:** 

```l4-file
-- DEONTIC Type Examples - Regulative Values in L4

-- ============================================================
-- § Type Declarations
-- ============================================================

-- Every DEONTIC value needs Actor and Action types
-- These define WHO can act and WHAT actions exist

DECLARE Actor IS ONE OF
    Buyer
    Seller
    Commissioner

DECLARE Action IS ONE OF
    `deliver goods` HAS description IS A STRING
    `pay invoice` HAS amount IS A NUMBER
    `inspect goods`
    `issue notice` HAS content IS A STRING
    `cancel order`

-- ============================================================
-- § Basic DEONTIC Values
-- ============================================================

-- A DEONTIC value represents an obligation, permission, or prohibition
-- The type signature shows the Actor and Action types

GIVETH A DEONTIC Actor Action
`simple delivery obligation` MEANS
    PARTY Seller
    MUST `deliver goods` "standard package"
    WITHIN 14
    HENCE FULFILLED
    LEST BREACH

-- DEONTIC values are first-class - they can be stored in variables
GIVETH A DEONTIC Actor Action
`the seller's duty` MEANS `simple delivery obligation`

-- ============================================================
-- § DEONTIC with Parameters
-- ============================================================

-- Functions can take parameters and return DEONTIC values

GIVEN deadline IS A NUMBER
GIVETH A DEONTIC Actor Action
`delivery within days` MEANS
    PARTY Seller
    MUST `deliver goods` "standard package"
    WITHIN deadline
    HENCE FULFILLED
    LEST BREACH

GIVEN price IS A NUMBER
      paymentDeadline IS A NUMBER
GIVETH A DEONTIC Actor Action
`payment obligation` MEANS
    PARTY Buyer
    MUST `pay invoice` price
    WITHIN paymentDeadline
    HENCE FULFILLED
    LEST BREACH

-- ============================================================
-- § DEONTIC Composition with HENCE
-- ============================================================

-- HENCE chains DEONTIC values - one obligation leads to another

GIVEN price IS A NUMBER
GIVETH A DEONTIC Actor Action
`sale contract` MEANS
    PARTY Seller
    MUST `deliver goods` "merchandise"
    WITHIN 14
    HENCE
        PARTY Buyer
        MUST `pay invoice` price
        WITHIN 30
        HENCE FULFILLED
        LEST BREACH BY Buyer BECAUSE "failed to pay"
    LEST BREACH BY Seller BECAUSE "failed to deliver"

-- ============================================================
-- § DEONTIC Composition with RAND (Parallel)
-- ============================================================

-- RAND combines DEONTIC values that must ALL be fulfilled

GIVETH A DEONTIC Actor Action
`mutual obligations` MEANS
    (PARTY Seller MUST `deliver goods` "item A" WITHIN 14 HENCE FULFILLED LEST BREACH)
    RAND
    (PARTY Buyer MUST `pay invoice` 1000 WITHIN 30 HENCE FULFILLED LEST BREACH)

-- ============================================================
-- § DEONTIC Composition with ROR (Alternative)
-- ============================================================

-- ROR combines DEONTIC values where ANY ONE fulfills the contract
-- Note: ROR applies to entire provisions, not individual obligations

GIVETH A DEONTIC Actor Action
`flexible delivery` MEANS
    (PARTY Seller MUST `deliver goods` "express shipping" WITHIN 7 HENCE FULFILLED LEST BREACH)
    ROR
    (PARTY Seller MUST `deliver goods` "standard shipping" WITHIN 14 HENCE FULFILLED LEST BREACH)

-- ============================================================
-- § Terminal DEONTIC Values
-- ============================================================

-- FULFILLED - The contract is successfully completed
-- BREACH - The contract is broken (optionally with blame)

GIVETH A DEONTIC Actor Action
`already fulfilled` MEANS FULFILLED

GIVETH A DEONTIC Actor Action
`immediate breach` MEANS BREACH

GIVETH A DEONTIC Actor Action
`breach with blame` MEANS BREACH BY Seller BECAUSE "goods were defective"

-- ============================================================
-- § Conditional DEONTIC Values
-- ============================================================

-- DEONTIC values can be computed conditionally

GIVEN isUrgent IS A BOOLEAN
GIVETH A DEONTIC Actor Action
`conditional delivery` MEANS
    IF isUrgent
    THEN
        PARTY Seller
        MUST `deliver goods` "urgent delivery"
        WITHIN 3
        HENCE FULFILLED
        LEST BREACH
    ELSE
        PARTY Seller
        MUST `deliver goods` "standard delivery"
        WITHIN 14
        HENCE FULFILLED
        LEST BREACH

-- ============================================================
-- § The EVALTRACE Function
-- ============================================================

-- EVALTRACE is the underlying function for evaluating contracts
-- Type: FORALL party action. DEONTIC party action -> NUMBER -> LIST (EVENT party action) -> DEONTIC party action

-- Create events using the EVENT constructor
testEvents MEANS LIST EVENT Seller (`deliver goods` "standard package") 5, EVENT Buyer (`pay invoice` 100) 20

-- Evaluate a contract against events starting at time 0
#EVAL EVALTRACE `simple delivery obligation` 0 testEvents

-- ============================================================
-- § Testing DEONTIC Values with #TRACE
-- ============================================================

-- #TRACE is syntactic sugar for EVALTRACE

-- Test 1: Simple obligation fulfilled
#TRACE `simple delivery obligation` AT 0 WITH
    PARTY Seller DOES `deliver goods` "standard package" AT 10

-- Test 2: Simple obligation breached (deadline passed)
#TRACE `simple delivery obligation` AT 0 WITH
    PARTY Seller DOES `deliver goods` "standard package" AT 20

-- Test 3: Parameterized delivery
#TRACE `delivery within days` 7 AT 0 WITH
    PARTY Seller DOES `deliver goods` "standard package" AT 5

-- Test 4: Sale contract - happy path
#TRACE `sale contract` 500 AT 0 WITH
    PARTY Seller DOES `deliver goods` "merchandise" AT 10
    PARTY Buyer DOES `pay invoice` 500 AT 30

-- Test 5: Mutual obligations with RAND
#TRACE `mutual obligations` AT 0 WITH
    PARTY Seller DOES `deliver goods` "item A" AT 10
    PARTY Buyer DOES `pay invoice` 1000 AT 25

-- Test 6: Flexible delivery with ROR (first option)
#TRACE `flexible delivery` AT 0 WITH
    PARTY Seller DOES `deliver goods` "express shipping" AT 5

-- Test 7: Flexible delivery with ROR (second option)
#TRACE `flexible delivery` AT 0 WITH
    PARTY Seller DOES `deliver goods` "standard shipping" AT 12

-- Test 8: Conditional delivery (urgent)
#TRACE `conditional delivery` TRUE AT 0 WITH
    PARTY Seller DOES `deliver goods` "urgent delivery" AT 2

-- Test 9: Conditional delivery (not urgent)
#TRACE `conditional delivery` FALSE AT 0 WITH
    PARTY Seller DOES `deliver goods` "standard delivery" AT 10

-- ============================================================
-- § Advanced: PROVIDED Clause for Pattern Matching
-- ============================================================

-- PROVIDED adds conditions to action pattern matching

GIVETH A DEONTIC Actor Action
`minimum payment contract` MEANS
    PARTY Buyer
    MUST `pay invoice` amount PROVIDED amount >= 100
    WITHIN 30
    HENCE FULFILLED
    LEST BREACH

-- Test: Payment meets minimum
#TRACE `minimum payment contract` AT 0 WITH
    PARTY Buyer DOES `pay invoice` 150 AT 20

-- Test: Payment below minimum (doesn't match, continues waiting)
#TRACE `minimum payment contract` AT 0 WITH
    PARTY Buyer DOES `pay invoice` 50 AT 20

-- ============================================================
-- § Advanced: EXACTLY for Precise Matching
-- ============================================================

-- EXACTLY requires an exact value match in patterns

GIVEN requiredAmount IS A NUMBER
GIVETH A DEONTIC Actor Action
`exact payment required` MEANS
    PARTY Buyer
    MUST EXACTLY `pay invoice` requiredAmount
    WITHIN 30
    HENCE FULFILLED
    LEST BREACH

-- Test: Exact amount paid
#TRACE `exact payment required` 500 AT 0 WITH
    PARTY Buyer DOES `pay invoice` 500 AT 15

-- Test: Wrong amount (doesn't match)
#TRACE `exact payment required` 500 AT 0 WITH
    PARTY Buyer DOES `pay invoice` 499 AT 15

-- ============================================================
-- § Advanced: WAIT UNTIL for Time Advancement
-- ============================================================

-- WAIT UNTIL advances time without an event
-- Useful for testing deadline behavior

#TRACE `simple delivery obligation` AT 0 WITH
    (`WAIT UNTIL` 20)

-- ============================================================
-- § DEONTIC as Return Values
-- ============================================================

-- Functions can compute and return DEONTIC values dynamically

GIVEN orderType IS A STRING
      price IS A NUMBER
GIVETH A DEONTIC Actor Action
`create order contract` MEANS
    IF orderType EQUALS "express"
    THEN
        PARTY Seller
        MUST `deliver goods` "express order"
        WITHIN 3
        HENCE
            PARTY Buyer
            MUST `pay invoice` expressPrice
            WITHIN 7
            HENCE FULFILLED
            LEST BREACH
        LEST BREACH
    ELSE
        PARTY Seller
        MUST `deliver goods` "standard order"
        WITHIN 14
        HENCE
            PARTY Buyer
            MUST `pay invoice` price
            WITHIN 30
            HENCE FULFILLED
            LEST BREACH
        LEST BREACH
    WHERE
        expressPrice MEANS price + 50

-- Test express order
#TRACE `create order contract` "express" 200 AT 0 WITH
    PARTY Seller DOES `deliver goods` "express order" AT 2
    PARTY Buyer DOES `pay invoice` 250 AT 5

-- Test standard order
#TRACE `create order contract` "standard" 200 AT 0 WITH
    PARTY Seller DOES `deliver goods` "standard order" AT 10
    PARTY Buyer DOES `pay invoice` 200 AT 30
```



### Basic Usage

```l4
DECLARE Actor IS ONE OF Buyer, Seller
DECLARE Action IS ONE OF `deliver goods`, `pay invoice` HAS amount IS A NUMBER

GIVETH A DEONTIC Actor Action
`delivery obligation` MEANS
    PARTY Seller
    MUST `deliver goods`
    WITHIN 14
    HENCE FULFILLED
    LEST BREACH
```

### Terminal Values

DEONTIC has two terminal values:

| Value       | Meaning                    |
| ----------- | -------------------------- |
| `FULFILLED` | Contract successfully done |
| `BREACH`    | Contract broken            |

### Breach with Blame

```l4
LEST BREACH BY Seller BECAUSE "failed to deliver on time"
```

## Type Signature

When a function returns a DEONTIC value, use:

```l4
GIVETH A DEONTIC ActorType ActionType
```

For example:

- `GIVETH A DEONTIC Person Action` — Obligations involving `Person` actors and `Action` actions
- `GIVETH A DEONTIC ContractParty ContractAction` — Custom actor and action types

## Composition

DEONTIC values can be composed in several ways:

### Chaining with HENCE

```l4
PARTY Seller MUST `deliver` WITHIN 14
HENCE
    PARTY Buyer MUST `pay` WITHIN 30
    HENCE FULFILLED
    LEST BREACH
LEST BREACH
```

### Parallel with RAND

All obligations must be fulfilled:

```l4
(PARTY Seller MUST `deliver` WITHIN 14 HENCE FULFILLED LEST BREACH)
RAND
(PARTY Buyer MUST `pay` WITHIN 30 HENCE FULFILLED LEST BREACH)
```

### Alternative with ROR

Either obligation fulfills the contract:

```l4
(PARTY Seller MUST `ship` WITHIN 14 HENCE FULFILLED LEST BREACH)
ROR
(PARTY Seller MUST `pickup` WITHIN 7 HENCE FULFILLED LEST BREACH)
```

## Evaluation

### #TRACE

Test DEONTIC values by simulating events:

```l4
#TRACE `delivery obligation` AT 0 WITH
    PARTY Seller DOES `deliver goods` AT 10
```

### EVALTRACE Function

The underlying evaluation function:

```l4
EVALTRACE : FORALL party action.
    DEONTIC party action ->    -- The contract
    NUMBER ->                  -- Start time
    LIST (EVENT party action) -> -- Events
    DEONTIC party action       -- Result
```

Use `EVENT` to construct events:

```l4
#EVAL EVALTRACE myContract 0 (LIST EVENT Seller `deliver` 5, EVENT Buyer `pay` 20)
```

## Deontic Modalities

| Modality  | Keyword | Meaning     | On Action      | On No Action   |
| --------- | ------- | ----------- | -------------- | -------------- |
| Must      | `MUST`  | Obligation  | HENCE (comply) | LEST (breach)  |
| May       | `MAY`   | Permission  | HENCE (comply) | Nothing        |
| Shall not | `SHANT` | Prohibition | LEST (breach)  | HENCE (comply) |

## Advanced Features

### PROVIDED Clause

Add conditions to action matching:

```l4
PARTY Buyer
MUST `pay invoice` amount PROVIDED amount >= 100
WITHIN 30
```

### EXACTLY Keyword

Require exact value matching:

```l4
PARTY Buyer
MUST EXACTLY `pay invoice` 500
WITHIN 30
```

### WAIT UNTIL

Advance time in traces without events:

```l4
#TRACE myContract AT 0 WITH
    (`WAIT UNTIL` 20)
```

## Related Keywords

- **[PARTY](/l4/reference/regulative/PARTY.md)** — Specifies who has the obligation
- **[MUST](/l4/reference/regulative/MUST.md)** — Creates an obligation
- **[MAY](/l4/reference/regulative/MAY.md)** — Creates a permission
- **[SHANT](/l4/reference/regulative/SHANT.md)** — Creates a prohibition
- **[BECAUSE](/l4/reference/regulative/BECAUSE.md)** — Adds blame reason to breach
- **[Regulative Rules](/l4/reference/regulative.md)** — Full regulative reference

## Further Reading

- [Regulative Rules Concept](/l4/concepts/legal-modeling/regulative-rules.md) — Deep dive into deontic logic
- [Foundation Module 5](/l4/courses/foundation/module-5-regulative.md) — Tutorial on regulative rules
- [Tom Hvitved's PhD Thesis](https://di.ku.dk/english/research/phd/phd-theses/2011/hvitved12phd.pdf) — Theoretical foundation