Simple semantics for defaults in Catala
Catala is a programming language for the law.
As described in an ICFP 2021 paper by Merigoux et al., Catala has multiple features designed for making it easy to write code that implements legal texts.
The feature I want to talk about here is Catala's support for default reasoning.
Default reasoning involves rules like “X is the case, except when Y, Z, ...”. Apparently, such patterns are common in the law.
The ICFP paper points out that default reasoning is analogous to exceptions in normal programming languages. The paper describes how to translate default reasoning into exceptions.
I think that a good way to see how it works is in terms of a simple “exceptions monad”.
The authors define the “default calculus”, which is the λ-calculus extended with constants for undefinedness and conflict and a default operator.
The default operator looks like this:
〈e1, ..., en | j :- c〉
where the intended meaning is “if
true then evaluate to
c and if
j is undefined or
false then evaluate to undefined, unless any of
en are defined, in which case if exactly one
ei is defined then evaluate to
ei, if more than one is defined then evaluate to conflict”.
The Catala ICFP paper defines an operational semantics for the default operator. The authors give a translation into a λ-calculus with exceptions. They have proved the translation correct using F star.
I think a more perspicious way of looking at how the default operator works is to think of it in terms of a simple monad.
I'll use OCaml syntax.
A “Catala value” is either
Undefined or an actual
type 'a catala = | Conflict | Undefined | Value of 'a
This definition is basically the
option/exceptions monad with two exception values.
There is an “information” ordering on Catala values, with
Undefined at the bottom,
Conflict at the top, and the
Values in between.
I'll not use the monad structure much, but we can decompose Catala's default operator into three simpler operators on Catala values.
The first is a conflict-adverse combination operator, which can be used to combine two Catala values into one:
let (<+>) x y = match x, y with | Undefined, x | x, Undefined -> x | Conflict, _ | _, Conflict -> Conflict | Value _, Value _ -> Conflict
Undefined always loses,
Conflict always wins, and two attempts at a value (even if they are equal) results in conflict.
This is a commutative monoid with
Undefined as the unit, and it is monotone in both arguments.
It'll be useful to be able to combine a list of Catala values using
let combine_list xs = List.fold_left (<+>) Undefined xs
guard operator is a sort of gate that evaluates to its second argument if the first is
true, and undefined otherwise (unless there was a conflict).
let guard x y = match x with | Conflict -> Conflict | Value true -> y | Value false | Undefined -> Undefined
This is also monotone in both arguments.
unless operator acts like a backwards try-catch.
unless x y defaults to
y is defined or is in conflict. Operationally, it tries
y first, and if it throws the
x is used instead.
let unless x y = match y with | Conflict -> Conflict | Undefined -> x | Value y -> Value y
This is not monotone in its second argument.
With these operators, we can recover Catala's default operator. It defaults to a guarded value, unless an exception is defined. In the event of multiple potential definitions, conflict is signaled.
let default value ~justification ~exceptions = unless (guard justification value) (combine_list exceptions)
I think this gives a simpler account of Catala's default operator than the ICFP paper.
We can see that the non-monotone behaviour of the default operator arises from the
unless operator, which you might expect from a try-catch like operator that rescues definition from undefinedness.
unless operator is a kind of “try this if that didn't work” operator, like exception handling and ordered choice in PEGs. I reckon that a semantics of data types with negation would be helpful in understanding such operators by recording “that didn't work” as a negation.
Why is it a
Conflictto combine two values that are equal? I think that Catala thinks of
Conflictas a mistake in the code or in the drafting of the law. But if there is a conflict that has no effect, then is that bad? What if a Catala value was a set of possible outcomes?
This formulation must be easier to reason about in a theorem prover than the ICFP paper's operational semantics or exception-based implementation.
What is the connection to Default Logic? The Catala paper states that the default operator is based on prioritised default logic, but doesn't elaborate on the formal relationship. Catala is focused on definitions, and rules are treated as a boolean-valued definitions. But default logic only deals in rules?
The Catala implementation seems to have a “without exceptions” translation but it seems more complicated than what I've written above. What is the connection?