Module 5: Regulative Rules

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:

-- Module 5: 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 - pays late with fee
#TRACE `the payment with late fee` AT 0 WITH
    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:

-- Who can act
DECLARE Person IS ONE OF
    Buyer
    Seller

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

Creating Obligations with MUST

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

Part	Meaning
`GIVETH A DEONTIC Person Action`	Returns a deontic value with Person actors and Action actions
`PARTY Seller`	The seller has this obligation
`MUST \`deliver 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:

GIVETH A DEONTIC Person Action
`the inspection right` MEANS
    PARTY Buyer
    MAY `inspect 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:

GIVETH A DEONTIC Employee EmployeeAction
`the confidentiality clause` MEANS
    PARTY Employee1
    SHANT `disclose confidential information`
    HENCE FULFILLED
    LEST BREACH

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

Chaining Obligations with HENCE

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

GIVETH A DEONTIC Person Action
`the sale contract` MEANS
    PARTY Seller
    MUST `deliver goods`
    WITHIN 14
    HENCE
        PARTY Buyer
        MUST `pay invoice` 1000
        WITHIN 30
        HENCE FULFILLED
        LEST BREACH
    LEST BREACH

This creates a chain:

Seller must deliver within 14 days
If delivered: Buyer must pay within 30 days
If buyer pays: Contract fulfilled
If either fails: Breach

Alternative Consequences with LEST

LEST specifies what happens on non-compliance:

GIVETH A DEONTIC Person Action
`the late payment contract` MEANS
    PARTY Buyer
    MUST `pay invoice` 1000
    WITHIN 30
    HENCE FULFILLED
    LEST
        PARTY Buyer
        MUST `pay 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:

PARTY Buyer
MUST `pay 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:

(PARTY Seller MUST `deliver goods` WITHIN 14 HENCE FULFILLED LEST BREACH)
RAND
(PARTY Buyer MUST `pay 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:

(PARTY Seller MUST `deliver goods` WITHIN 14 HENCE FULFILLED)
ROR
(PARTY Seller MUST `arrange 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

#TRACE `the sale contract` AT 0 WITH
    PARTY Seller DOES `deliver goods` AT 10
    PARTY Buyer DOES `pay invoice` 1000 AT 25

This simulates:

Start at day 0
Seller delivers at day 10 (within 14-day deadline ✓)
Buyer pays at day 25 (within 30-day deadline ✓)

Result: FULFILLED

Breach Scenario

#TRACE `the sale contract` AT 0 WITH
    PARTY Seller DOES `deliver 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:

cabal run jl4-cli -- --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

-- ✅ Good: Clear, descriptive types
DECLARE ContractParty IS ONE OF Landlord, Tenant
DECLARE LeaseAction IS ONE OF
    `pay rent` HAS amount IS A NUMBER
    `maintain property`
    `provide access`
    `terminate lease`

2. Use BREACH BY for Clear Blame

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

3. Consider All Paths

Make sure every path leads to either FULFILLED or BREACH:

-- ✅ 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

-- Happy path
#TRACE contract AT 0 WITH
    PARTY Seller DOES `deliver` AT 5
    PARTY Buyer DOES `pay` AT 20

-- Late delivery
#TRACE contract AT 0 WITH
    PARTY Seller DOES `deliver` AT 20

-- No action
#TRACE 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."

Exercise 2: Chained Obligations

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

Exercise 3: Permission and Prohibition

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

Summary

Concept	Syntax
Obligation	`PARTY actor MUST action`
Permission	`PARTY actor MAY action`
Prohibition	`PARTY actor SHANT action`
Deadline	`WITHIN days`
Compliance result	`HENCE nextObligation` 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 startTime WITH events`
Event	`PARTY actor DOES action AT time`

What's Next?

In Module 6: Putting It Together, you'll build a complete legal model combining everything you've learned.