# Module 6: Regulative Rules

**Prerequisites:** Modules 1–5

In this module, you'll learn how to model legal obligations, permissions, and prohibitions—the core of contract and regulatory law.

## Learning Objectives

By the end of this module, you will be able to:

- Define Actor and Action types
- Create obligations with MUST
- Create permissions with MAY
- Create prohibitions with SHANT
- Chain obligations with HENCE and LEST
- Test regulative rules with #TRACE

---

## What Are Regulative Rules?

**Regulative rules** define what parties must, may, or must not do. They're the building blocks of contracts and regulations:

- **Obligations** (MUST): "The seller must deliver goods"
- **Permissions** (MAY): "The buyer may inspect goods"
- **Prohibitions** (SHANT): "The employee shall not disclose confidential information"
- **Option** (DO): "The employee discloses confidential information"

L4 represents these using the **DEONTIC** type.

---

## The DEONTIC Type

A DEONTIC value represents an obligation, permission, or prohibition. It has:

- **Who** (PARTY): The actor with the duty/permission
- **What** (action): The action to be performed
- **When** (WITHIN): The deadline
- **Consequences** (HENCE/LEST): What happens next

The complete working example:



```l4-file
-- Module 6: Regulative Rules - Complete Examples
-- All examples are validated and use natural language identifiers

-- =============================================================================
-- SECTION 1: Actor and Action Types
-- =============================================================================

-- Parties to a contract
DECLARE `Contract Party` IS ONE OF
    `the buyer`
    `the seller`
    `the landlord`
    `the tenant`
    `the employee`
    `the employer`

-- Actions in a sale contract
DECLARE `Sale Action` IS ONE OF
    `deliver the goods`
    `pay the invoice` HAS amount IS A NUMBER
    `inspect the goods`
    `cancel the order`

-- =============================================================================
-- SECTION 2: Basic Obligations with MUST
-- =============================================================================

-- Simple delivery obligation
GIVETH A DEONTIC `Contract Party` `Sale Action`
`the delivery obligation` MEANS
    PARTY `the seller`
    MUST `deliver the goods`
    WITHIN 14
    HENCE FULFILLED
    LEST BREACH

-- =============================================================================
-- SECTION 3: Permissions with MAY
-- =============================================================================

-- The buyer may inspect goods
GIVETH A DEONTIC `Contract Party` `Sale Action`
`the inspection right` MEANS
    PARTY `the buyer`
    MAY `inspect the goods`
    HENCE FULFILLED

-- =============================================================================
-- SECTION 4: Chained Obligations with HENCE
-- =============================================================================

-- Complete sale contract: deliver then pay
GIVETH A DEONTIC `Contract Party` `Sale Action`
`the complete sale contract` MEANS
    PARTY `the seller`
    MUST `deliver the goods`
    WITHIN 14
    HENCE
        PARTY `the buyer`
        MUST `pay the invoice` 1000
        WITHIN 30
        HENCE FULFILLED
        LEST BREACH
    LEST
        PARTY `the seller`
        MAY `cancel the order`
        HENCE BREACH

-- =============================================================================
-- SECTION 5: Alternative Consequences with LEST
-- =============================================================================

-- Late payment with penalty
GIVETH A DEONTIC `Contract Party` `Sale Action`
`the payment with late fee` MEANS
    PARTY `the buyer`
    MUST `pay the invoice` 1000
    WITHIN 30
    HENCE FULFILLED
    LEST
        PARTY `the buyer`
        MUST `pay the invoice` 1100
        WITHIN 14
        HENCE FULFILLED
        LEST BREACH

-- =============================================================================
-- SECTION 6: Real-World Example - Wedding Vows
-- =============================================================================

DECLARE Spouse IS ONE OF
    Spouse1
    Spouse2

DECLARE Vow IS ONE OF
    `exchange vows`
    `love and cherish`
    abandon
    `be unfaithful`

-- The wedding ceremony: mutual exchange of vows
GIVETH A DEONTIC Spouse Vow
`the wedding ceremony` MEANS
    PARTY Spouse1
    MUST `exchange vows`
    WITHIN 1
    HENCE
        PARTY Spouse2
        MUST `exchange vows`
        WITHIN 1
        HENCE FULFILLED
        LEST BREACH BY Spouse2 BECAUSE "failed to exchange vows"
    LEST BREACH BY Spouse1 BECAUSE "failed to exchange vows"

-- Fidelity clause: prohibition
GIVETH A DEONTIC Spouse Vow
`the fidelity clause` MEANS
    PARTY Spouse1
    SHANT `be unfaithful`
    HENCE FULFILLED
    LEST BREACH BY Spouse1 BECAUSE "was unfaithful"

-- =============================================================================
-- SECTION 7: Tests
-- =============================================================================

-- Test the delivery obligation - fulfilled
#TRACE `the delivery obligation` AT 0 WITH
    PARTY `the seller` DOES `deliver the goods` AT 10

-- Test the delivery obligation - breached (late delivery)
#TRACE `the delivery obligation` AT 0 WITH
    PARTY `the seller` DOES `deliver the goods` AT 20

-- Test the complete sale - happy path
#TRACE `the complete sale contract` AT 0 WITH
    PARTY `the seller` DOES `deliver the goods` AT 10
    PARTY `the buyer` DOES `pay the invoice` 1000 AT 35

-- Test the late payment with penalty - the day-35 payment misses the
-- 30-day deadline, so the buyer must pay again with the 10% late fee
#TRACE `the payment with late fee` AT 0 WITH
    PARTY `the buyer` DOES `pay the invoice` 1000 AT 35
    PARTY `the buyer` DOES `pay the invoice` 1100 AT 40

-- Test the wedding ceremony - happy marriage
#TRACE `the wedding ceremony` AT 0 WITH
    PARTY Spouse1 DOES `exchange vows` AT 0
    PARTY Spouse2 DOES `exchange vows` AT 0

-- Test the fidelity clause - breach
#TRACE `the fidelity clause` AT 0 WITH
    PARTY Spouse1 DOES `be unfaithful` AT 100
```



### Defining Actor and Action Types

First, define who can act and what actions exist:

```l4
-- Who can act
DECLARE `Contract Party` IS ONE OF
    `the buyer`
    `the seller`

-- What actions exist
DECLARE `Sale Action` IS ONE OF
    `deliver the goods`
    `pay the invoice` HAS amount IS A NUMBER
    `inspect the goods`
```

---

## Creating Obligations with MUST

```l4
GIVETH A DEONTIC `Contract Party` `Sale Action`
`the delivery obligation` MEANS
    PARTY `the seller`
    MUST `deliver the goods`
    WITHIN 14
    HENCE FULFILLED
    LEST BREACH
```

| Part                                                  | Meaning                                               |
| ----------------------------------------------------- | ----------------------------------------------------- |
| `` GIVETH A DEONTIC `Contract Party` `Sale Action` `` | Returns a deontic value with these actors and actions |
| `` PARTY `the seller` ``                              | The seller has this obligation                        |
| `` MUST `deliver the goods` ``                        | They must deliver goods                               |
| `WITHIN 14`                                           | Within 14 days                                        |
| `HENCE FULFILLED`                                     | If they do, the obligation is fulfilled               |
| `LEST BREACH`                                         | If they don't, it's a breach                          |

---

## Creating Permissions with MAY

Permissions don't create breaches if unused:

```l4
GIVETH A DEONTIC `Contract Party` `Sale Action`
`the inspection right` MEANS
    PARTY `the buyer`
    MAY `inspect the goods`
    HENCE FULFILLED
```

Note: MAY doesn't need LEST because not exercising a permission isn't a breach.

---

## Creating Prohibitions with SHANT

Prohibitions say what must NOT happen. From the wedding vows example in 

```l4-file
-- Module 6: Regulative Rules - Complete Examples
-- All examples are validated and use natural language identifiers

-- =============================================================================
-- SECTION 1: Actor and Action Types
-- =============================================================================

-- Parties to a contract
DECLARE `Contract Party` IS ONE OF
    `the buyer`
    `the seller`
    `the landlord`
    `the tenant`
    `the employee`
    `the employer`

-- Actions in a sale contract
DECLARE `Sale Action` IS ONE OF
    `deliver the goods`
    `pay the invoice` HAS amount IS A NUMBER
    `inspect the goods`
    `cancel the order`

-- =============================================================================
-- SECTION 2: Basic Obligations with MUST
-- =============================================================================

-- Simple delivery obligation
GIVETH A DEONTIC `Contract Party` `Sale Action`
`the delivery obligation` MEANS
    PARTY `the seller`
    MUST `deliver the goods`
    WITHIN 14
    HENCE FULFILLED
    LEST BREACH

-- =============================================================================
-- SECTION 3: Permissions with MAY
-- =============================================================================

-- The buyer may inspect goods
GIVETH A DEONTIC `Contract Party` `Sale Action`
`the inspection right` MEANS
    PARTY `the buyer`
    MAY `inspect the goods`
    HENCE FULFILLED

-- =============================================================================
-- SECTION 4: Chained Obligations with HENCE
-- =============================================================================

-- Complete sale contract: deliver then pay
GIVETH A DEONTIC `Contract Party` `Sale Action`
`the complete sale contract` MEANS
    PARTY `the seller`
    MUST `deliver the goods`
    WITHIN 14
    HENCE
        PARTY `the buyer`
        MUST `pay the invoice` 1000
        WITHIN 30
        HENCE FULFILLED
        LEST BREACH
    LEST
        PARTY `the seller`
        MAY `cancel the order`
        HENCE BREACH

-- =============================================================================
-- SECTION 5: Alternative Consequences with LEST
-- =============================================================================

-- Late payment with penalty
GIVETH A DEONTIC `Contract Party` `Sale Action`
`the payment with late fee` MEANS
    PARTY `the buyer`
    MUST `pay the invoice` 1000
    WITHIN 30
    HENCE FULFILLED
    LEST
        PARTY `the buyer`
        MUST `pay the invoice` 1100
        WITHIN 14
        HENCE FULFILLED
        LEST BREACH

-- =============================================================================
-- SECTION 6: Real-World Example - Wedding Vows
-- =============================================================================

DECLARE Spouse IS ONE OF
    Spouse1
    Spouse2

DECLARE Vow IS ONE OF
    `exchange vows`
    `love and cherish`
    abandon
    `be unfaithful`

-- The wedding ceremony: mutual exchange of vows
GIVETH A DEONTIC Spouse Vow
`the wedding ceremony` MEANS
    PARTY Spouse1
    MUST `exchange vows`
    WITHIN 1
    HENCE
        PARTY Spouse2
        MUST `exchange vows`
        WITHIN 1
        HENCE FULFILLED
        LEST BREACH BY Spouse2 BECAUSE "failed to exchange vows"
    LEST BREACH BY Spouse1 BECAUSE "failed to exchange vows"

-- Fidelity clause: prohibition
GIVETH A DEONTIC Spouse Vow
`the fidelity clause` MEANS
    PARTY Spouse1
    SHANT `be unfaithful`
    HENCE FULFILLED
    LEST BREACH BY Spouse1 BECAUSE "was unfaithful"

-- =============================================================================
-- SECTION 7: Tests
-- =============================================================================

-- Test the delivery obligation - fulfilled
#TRACE `the delivery obligation` AT 0 WITH
    PARTY `the seller` DOES `deliver the goods` AT 10

-- Test the delivery obligation - breached (late delivery)
#TRACE `the delivery obligation` AT 0 WITH
    PARTY `the seller` DOES `deliver the goods` AT 20

-- Test the complete sale - happy path
#TRACE `the complete sale contract` AT 0 WITH
    PARTY `the seller` DOES `deliver the goods` AT 10
    PARTY `the buyer` DOES `pay the invoice` 1000 AT 35

-- Test the late payment with penalty - the day-35 payment misses the
-- 30-day deadline, so the buyer must pay again with the 10% late fee
#TRACE `the payment with late fee` AT 0 WITH
    PARTY `the buyer` DOES `pay the invoice` 1000 AT 35
    PARTY `the buyer` DOES `pay the invoice` 1100 AT 40

-- Test the wedding ceremony - happy marriage
#TRACE `the wedding ceremony` AT 0 WITH
    PARTY Spouse1 DOES `exchange vows` AT 0
    PARTY Spouse2 DOES `exchange vows` AT 0

-- Test the fidelity clause - breach
#TRACE `the fidelity clause` AT 0 WITH
    PARTY Spouse1 DOES `be unfaithful` AT 100
```

:

```l4
GIVETH A DEONTIC Spouse Vow
`the fidelity clause` MEANS
    PARTY Spouse1
    SHANT `be unfaithful`
    HENCE FULFILLED
    LEST BREACH BY Spouse1 BECAUSE "was unfaithful"
```

`SHANT` is equivalent to "shall not" or "must not."

---

## Chaining Obligations with HENCE

Real contracts have sequences of obligations. Use HENCE to chain them:

```l4
GIVETH A DEONTIC `Contract Party` `Sale Action`
`the complete sale contract` MEANS
    PARTY `the seller`
    MUST `deliver the goods`
    WITHIN 14
    HENCE
        PARTY `the buyer`
        MUST `pay the invoice` 1000
        WITHIN 30
        HENCE FULFILLED
        LEST BREACH
    LEST
        PARTY `the seller`
        MAY `cancel the order`
        HENCE BREACH
```

This creates a chain:

1. Seller must deliver within 14 days
2. **If delivered**: Buyer must pay within 30 days
3. **If buyer pays**: Contract fulfilled
4. **If either fails**: Breach

---

## Alternative Consequences with LEST

LEST specifies what happens on non-compliance:

```l4
GIVETH A DEONTIC `Contract Party` `Sale Action`
`the payment with late fee` MEANS
    PARTY `the buyer`
    MUST `pay the invoice` 1000
    WITHIN 30
    HENCE FULFILLED
    LEST
        PARTY `the buyer`
        MUST `pay the invoice` 1100  -- 10% late fee
        WITHIN 14
        HENCE FULFILLED
        LEST BREACH
```

This gives the buyer a second chance with a penalty before reaching breach.

---

## Conditional Obligations with PROVIDED

Add conditions to obligations:

```l4
PARTY `the buyer`
MUST `pay the invoice` amount PROVIDED amount >= 100
WITHIN 30
HENCE FULFILLED
LEST BREACH
```

`PROVIDED` adds a guard condition—the obligation only applies if the condition is true.

---

## Parallel Obligations with RAND

Use `RAND` (regulative AND) for obligations that must all be fulfilled:

```l4
(PARTY `the seller` MUST `deliver the goods` WITHIN 14 HENCE FULFILLED LEST BREACH)
RAND
(PARTY `the buyer` MUST `pay the invoice` 1000 WITHIN 30 HENCE FULFILLED LEST BREACH)
```

Both obligations must be fulfilled for the contract to be fulfilled.

---

## Alternative Paths with ROR

Use `ROR` (regulative OR) when either path fulfills the contract:

```l4
(PARTY `the seller` MUST `deliver the goods` WITHIN 14 HENCE FULFILLED)
ROR
(PARTY `the seller` MUST `arrange a pickup` WITHIN 7 HENCE FULFILLED)
LEST BREACH
```

The seller can choose either option.

---

## Testing with #TRACE

`#TRACE` simulates scenarios to see what happens:

### Basic Trace

```l4
#TRACE `the complete sale contract` AT 0 WITH
    PARTY `the seller` DOES `deliver the goods` AT 10
    PARTY `the buyer` DOES `pay the invoice` 1000 AT 35
```

This simulates:

- Start at day 0
- Seller delivers at day 10 (within 14-day deadline ✓)
- Buyer pays at day 35 (25 days after delivery—within the 30-day deadline ✓)

Note that a `WITHIN` deadline starts running when its obligation becomes active: the buyer's 30 days count from the delivery on day 10.

Result: `FULFILLED`

### Breach Scenario

```l4
#TRACE `the delivery obligation` AT 0 WITH
    PARTY `the seller` DOES `deliver the goods` AT 20  -- Late! Deadline was 14
```

Result: `BREACH` (seller delivered late)

---

## Real-World Example: Wedding Vows

See the wedding vows example which demonstrates:

- Mutual exchange of vows
- Prohibitions (fidelity clause)
- Using `BREACH BY ... BECAUSE ...` for clear blame assignment

---

## State Graphs

L4 can visualize regulative rules as state transition diagrams:

```bash
l4 state-graph mycontract.l4

# Or from a Haskell checkout
cabal run l4 -- state-graph mycontract.l4
```

This generates a graph showing:

- **States**: Initial, intermediate, Fulfilled, Breach
- **Transitions**: Actions that move between states
- **Deadlines**: When actions must occur

The graph makes complex contracts easier to understand.

---

## Best Practices

### 1. Define Clear Actors and Actions

```l4
-- ✅ Good: Clear, descriptive types
DECLARE `Lease Party` IS ONE OF
    `the landlord`
    `the tenant`

DECLARE `Lease Action` IS ONE OF
    `pay the rent` HAS amount IS A NUMBER
    `maintain the property`
    `provide access`
    `terminate the lease`
```

### 2. Use BREACH BY for Clear Blame

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

### 3. Consider All Paths

Make sure every path leads to either FULFILLED or BREACH:

```l4
-- ✅ Good: All paths handled
MUST action
WITHIN deadline
HENCE FULFILLED
LEST BREACH

-- ❌ Bad: What happens if they don't comply?
MUST action
WITHIN deadline
HENCE FULFILLED
-- Missing LEST!
```

### 4. Test with Multiple Scenarios

```l4
-- Happy path
#TRACE `the complete sale contract` AT 0 WITH
    PARTY `the seller` DOES `deliver the goods` AT 5
    PARTY `the buyer` DOES `pay the invoice` 1000 AT 20

-- Late delivery
#TRACE `the complete sale contract` AT 0 WITH
    PARTY `the seller` DOES `deliver the goods` AT 20

-- No action
#TRACE `the complete sale contract` AT 0 WITH
    -- Empty: what happens at deadline?
```

---

## Exercises

### Exercise 1: Simple Obligation

Write a regulative rule: "The employee must submit a timesheet within 7 days."

<details>
<summary>Solution</summary>

```l4
DECLARE `Employment Party` IS ONE OF
    `the employee`
    `the employer`

DECLARE `Employment Action` IS ONE OF
    `submit the timesheet`

GIVETH A DEONTIC `Employment Party` `Employment Action`
`the timesheet obligation` MEANS
    PARTY `the employee`
    MUST `submit the timesheet`
    WITHIN 7
    HENCE FULFILLED
    LEST BREACH

#TRACE `the timesheet obligation` AT 0 WITH
    PARTY `the employee` DOES `submit the timesheet` AT 5
```

</details>

### Exercise 2: Chained Obligations

Write a contract: "Buyer must pay deposit within 7 days. After deposit, seller must deliver within 14 days."

<details>
<summary>Solution</summary>

```l4
DECLARE `Sale Party` IS ONE OF
    `the buyer`
    `the seller`

DECLARE `Deposit Action` IS ONE OF
    `pay the deposit`
    `deliver the goods`

GIVETH A DEONTIC `Sale Party` `Deposit Action`
`the deposit contract` MEANS
    PARTY `the buyer`
    MUST `pay the deposit`
    WITHIN 7
    HENCE
        PARTY `the seller`
        MUST `deliver the goods`
        WITHIN 14
        HENCE FULFILLED
        LEST BREACH
    LEST BREACH

#TRACE `the deposit contract` AT 0 WITH
    PARTY `the buyer` DOES `pay the deposit` AT 3
    PARTY `the seller` DOES `deliver the goods` AT 12
```

</details>

### Exercise 3: Permission and Prohibition

Write rules for: "Tenant may have pets. Tenant shall not smoke indoors."

<details>
<summary>Solution</summary>

```l4
DECLARE `Lease Party` IS ONE OF
    `the tenant`
    `the landlord`

DECLARE `Lease Action` IS ONE OF
    `keep a pet`
    `smoke indoors`

GIVETH A DEONTIC `Lease Party` `Lease Action`
`the pet permission` MEANS
    PARTY `the tenant`
    MAY `keep a pet`
    HENCE FULFILLED

GIVETH A DEONTIC `Lease Party` `Lease Action`
`the smoking prohibition` MEANS
    PARTY `the tenant`
    SHANT `smoke indoors`
    HENCE FULFILLED
    LEST BREACH BY `the tenant` BECAUSE "smoked indoors"

#TRACE `the pet permission` AT 0 WITH
    PARTY `the tenant` DOES `keep a pet` AT 1

#TRACE `the smoking prohibition` AT 0 WITH
    PARTY `the tenant` DOES `smoke indoors` AT 10
```

</details>

---

## Summary

| Concept              | Syntax                                       |
| -------------------- | -------------------------------------------- |
| Obligation           | `PARTY actor MUST action`                    |
| Permission           | `PARTY actor MAY action`                     |
| Prohibition          | `PARTY actor SHANT action`                   |
| Deadline             | `WITHIN days`                                |
| Compliance result    | `HENCE next obligation` or `HENCE FULFILLED` |
| Non-compliance       | `LEST consequence` or `LEST BREACH`          |
| Condition            | `PROVIDED condition`                         |
| Parallel obligations | `obligation1 RAND obligation2`               |
| Alternative paths    | `obligation1 ROR obligation2`                |
| Simulate             | `#TRACE rule AT start time WITH events`      |
| Event                | `PARTY actor DOES action AT time`            |

---

## What's Next?

In [Module 7: Putting It Together](/l4/courses/foundation/module-7-capstone.md), you'll build a complete legal model combining everything you've learned.