As part of the next-gen L4 language definition effort, we present a handful of challenge problems that exercise the proposed semantics at various levels of difficulty and composition.
LTL/CTL style assertions about a contract
These exist at a level outside of the contract itself, just as an LTL assertion exists outside a particular state machine.
At this level, the “MUST DO” keyword is a bounded alethic modal.
Every such alethic “must” is associated with one or more bounds, or desired goals.
The full expression is: it is not possible to satisfy [bounds] without party P performing action A.
The trivial [bounds] is achievement of a final fulfilled state.
Strong and weak forms can be distinguished: the strong form no breach of any subcontract. The weak form allows breaches of subcontract so long as some reparation pathway reaches fulfilled.
These exist within a contract, allowing a contract to say: party P1 may perform some action so long as they are not aware that party P2 has done some thing
Which expands to something like:
THREAD 1
PARTY P1
WHEN P1 NOT knows Fact 1
MAY Action 1
THREAD 2
PARTY P2
MAY notify P1
that Fact 1
multi-temporal logic provides the mechanism for looking at the history of the contract and past state.
For instance, suppose we want to say that P1 may only perform Action 2 if they have not yet performed Action 1, and vice versa
In state transition semantics, this is internal choice: <p1>(action1 || action2) -> …
A contract may phrase it as
THREAD 1
PARTY P1
HAVING NEVER Action 2
MAY Action 1
THREAD 2
PARTY P1
HAVING NEVER Action 1
MAY Action 2
This is a verbose but equivalent way of saying
PARTY P1
MAY Action 1
XOR Action 2
Sometimes a contract will explicitly want to use language from the “external” level.
This poses a problem.
Party P1 may at any time perform some action α, so long as Party P1 is not at that time required to pay a fine.
OK, so the next question is whether they are required to pay a fine. Let’s suppose the fine could arise in some other thread. So the first thread (where you can do α) gets conditioned on whether the second thread is active.
To make things more interesting, let’s complicate the second thread.
Let’s suppose we live in a world where you should pay a fine; but if you fail to do so, you might yet get lucky! If the King is in a good mood on his birthday, he waives the fine.
THREAD penalty
PARTY P1
COULD pay a fine (MUST)
BEFORE July 1
LEST PARTY P1
COULD appeal to the King for clemency (MAY)
BEFORE August 1
HENCE PARTY King
COULD waive fine (MAY)
BEFORE September 1
LEST PARTY P1
MUST pay triple the fine
BEFORE October 1
This reflects, to some degree, the thinking from the classic paper “A fine is a price”. From an opinionated, moralistic perspective, a fine is a fine. From an unopinionated, amoral perspective, a fine is a price, which rational entities choose to pay, or not.
From LegalRuleML’s perspective, this is a “suborder” list. In a conventional, “opinionated”, formulation, it makes sense to use “MUST” and “MAY” to distinguish the degrees of freedom within each clause, or subcontract. The conventional deontic modals are given in parentheses above.
In an “unopinionated” formulation, we simply state the possibilities, and let the chips fall where they may.
So, is the party required to pay a fine?
We could debate that question along opinionated vs unopinionated lines, where the argument turns on whether they COULD at any given time pay a fine. During those periods when the ball is not in their court, we could argue that they are not required to pay the fine, since there’s more game to play.
So we could debate that question along stern vs lax lines, where the answer turns on external luck: whether they enjoy the King’s mercy.
From a stern perspective, the answer is yes, they are required: because the alternative to paying the initial fine, if the King frowns, could lead to paying triple the fine, and the alternative to paying double the fine is breach.
From a lax perspective, no: if the King smiles, then the fine is waived, and the party could get off. So long as there is a possibility of getting off, the party is not 100% inevitably due to pay a fine.
So, the temporal properties can be evaluated under “best case” or “worst case” scenarios, where terms that are out of the party’s control are dispositive!
Keeping the sequence of events in mind, if the King is not generous:
| Month | Required to pay fine? |
|---|---|
| June | yes |
| July | no |
| August | no |
| September | yes |
| October | no, breach state |
So, in this passage, is it true, externally, that P1 “must” pay a fine? Well, they should, because that keeps them on the straight-and-narrow happy path.
But they could get away with not paying it.
Indeed, there is a loophole here; the party could take the original action α simply by waiting until July, because at that time they are not, technically, required to pay a fine; instead they are waiting for the King’s answer.
But surely that is not the intent of the rule!
Perhaps the best way to proceed is to simply decide that the initial specification, in natural language, was badly drafted.
Party P1 may at any time perform some action, so long as Party P1 is not at that time required to pay a fine.
There are two fixes. First, we introduce the idea that being anywhere in the penalty subcontract is disqualifying.
Party P1 may at any time perform some action, unless Party P1 is not then engaged in an unresolved proceeding in relation to a fine.
We should also give the party the initiative to get themselves out of trouble at any time by paying double the fine.
After having incurred a fine, and having failed to pay it, then prior to receiving the King’s answer, the party may resolve the matter by paying double the fine.
So we compose the subcontracts:
THREAD penalty
PARTY P1
COULD pay a fine (MUST)
BEFORE July 1
LEST
{ PARTY P1
COULD appeal to the King for clemency (MAY)
BEFORE August 1
HENCE PARTY King
COULD waive fine (MAY)
BEFORE September 1
OR PARTY P1
COULD pay double the fine (MAY)
BEFORE September 1
}
LEST PARTY P1
MUST pay triple the fine
BEFORE October 1
Expressing the above composition with only indentation is a bit challenging, you kind of need the curly braces.
- A person may frobulate
- if and only if
- the person’s colour attribute is red
- and
- the person’s size attribute is greater than
- if the person is a rectangle, then 10 * 10
- if the person is a circle, then pi * 5 * 5
- if the person is some other shape, then 42
- or
- the person’s electrical charge, if they have one, is positive
There is an element of choice: the person MAY frobulate, and the contract can be fulfilled in two ways: they do, or don’t.
The only way the contract can be BREACHED is if they fail to meet the preconditions, but frobulate anyway.
- if the person has no electrical charge, then line 7 evaluates to false
- “the identity for OR is false”
- person.electricalCharge
- lines 4 and 6 are at the same level. What is the grouping precedence infixl/infixr for an unindented and/or? Jo Hsi has previously pointed out natural4 does opposite to Python. Let’s fix that in this next iteration?
- the IFF on line 2 implies that we can test the contract for other “may frobulate” and detect a conflict if something else also allows frobulation, either directly or in some synthetic way.
- If a person crantulates, then that person frobulates.
- A person may crantulate at any time.
This is a conflict with the previous (1).
The reasoning engine should infer the existence of this conflict, and warn about it.
Line 7 says, “a person’s X, if they have one, is Y”
What are the semantics of “if they have one”?
In Typescript we have optional types; and we might, naively, adopt the notion of “if they have one”
enum PosNeg { Positive, Negative }
interface Person {
electricalCharge ?: PosNeg
}That corresponds to the Haskell
data ElectricalCharge2 = Positive | Negative
data Person = Person {
electricalCharge :: Maybe ElectricalCharge2
}Another way to model electrical charge:
data ElectricalCharge3 = Positive | Neutral | NegativeIn the second case, “if they have one” is given by person.electricalCharge /= Nothing
In the first case, “if they have one” is given by person.electricalCharge /= Neutral
The example so far is not temporally bounded. Do we infer that the permission is coextensive with the conditions? I.e. the conditions need to be tested at every time t, and then the resulting permission holds at that time t.
Or do we add a notion of deadlines:
This is a purely constitutive decision rule, without any deontics / state transitions.
- A person qualifies
- if and only if
- the person’s colour attribute is red
- and
- the person’s size attribute is greater than
- if the person is a rectangle, then 10 * 10
- if the person is a circle, then pi * 5 * 5
- if the person is neither, then 42
- or
- the person’s electrical charge, if they have one, is positive
- Upon qualification, a person may frobulate for 24 hours, but not thereafter.
EVERY person MUST obey the law – IF (always!)
Showing some of the essentials from DeonDigital’s CSL:
- The trivial “identity” contract is FULFILLED.
- The trivial dual to the identity contract is BREACHED.
- Nontrivial contract: C1 @( PARTY P (MUST|MAY|SHANT) DO X {..} BEFORE DEADLINE ) THEN C2 ELSE C3.
- Contracts can be composed using AND, OR, THEN, ELSE relations.
- Contract 1 THEN contract 2 THEN contract 3 ELSE contract 4.
- Contract 1 AND contract 2 OR contract 3.
And that’s the basic underlying semantics for regulative rules!
Suppose we have two subcontracts C1 and C2. Suppose we want to say that either has to be performed.
In CSL syntax, we have
C1 or C2
If we wanted to say that both have to be performed, we could have
C1 and C2
Now, because C1 and C2 are contracts, they can bear their own deadlines D1 and D2 respectively. But what if we want to say that both contracts are to be subject to the same deadline?
(C1 or C2) BEFORE D3 (C1 and C2) BEFORE D3
Then C1 and C2 could be syntactically written as partial contracts, absent a BEFORE deadline keyword
And the deadline D3 would apply to the composition of C1 with C2.
What if C1 and C2 do have their own deadlines?
Like, consider
(C1 then C2) BEFORE D3 C1: ... BEFORE 4 days C2: ... BEFORE 8 days (relative to what timepoint??? start of C1 or end of C2?) D3 = BEFORE 10 days
It might be possible for C1 to take 4 days, and then C2 to take another 8 days, and though both subcontracts are OK, the main D3 is violated.
And that would be valid.
And we would let one of our reasoning backends detect the possibility that 10 days might not be enough.
Suppose P1 has two obligations, expressed in fully-qualified form:
UPON Event 1 PARTY P1 MUST file paperwork BEFORE 1 week
UPON Event 1
PARTY P1
MUST pay $100
to P2
BEFORE 1 week
It is natural to want to simplify the phrasing by factoring out the common parts.
If we went to one extreme we would end up with the delta arising only at the action level:
UPON Event 1
PARTY P1
MUST file paperwork
AND pay $100
to P2
BEFORE 1 week
In linguistics, this factoring is called ellipsis.
However, what if each action had a different deadline?
UPON Event 1
PARTY P1
MUST file paperwork
BEFORE 1 week
AND
MUST pay $100
to P2
BEFORE 2 weeks
Now we see that the UPON and PARTY now multiply across the elements of the AND conjunction:
UPON Event 1
PARTY P1
MUST file paperwork
BEFORE 1 week
AND
UPON Event 1
PARTY P1
MUST pay $100
to P2
BEFORE 2 weeks
This sort of transformation should happen somewhere inside our intermediate repesentation.
Formally: given a record type
R :: [(String, Value)]We derive a syntactic sugar type that allows each attribute to hold multiple values:
R' :: [(Maybe Conjunction, [(String, Value)])]From which we can permute to multiple records of original type R simply by combining every permutation of field values using the given conjunction.
Example:
compound = Clause' { Partial { upon = "Event 1" }
, Partial { party = "P1" }
, And [ Partial { deontic = "must"
, action = "file paperwork"
, deadline = "1 week" }
, Partial { deontic = "must"
, action = "pay $100"
, deadline = "2 weeks" }
]
}This would multiply out to the original form
compounds = And [ Clause { upon = "Event 1"
, party = "P1"
, deontic = "must"
, action = "file paperwork"
, deadline = "1 week"
}
, Clause { upon = "Event 1"
, party = "P1"
, deontic = "must"
, action = "pay $100"
, deadline = "2 weeks"
}
]
}For a linguistic treatment of these transformations, see https://en.wikipedia.org/wiki/Ellipsis_(linguistics)
Suppose we have a simple contract:
- EVERY P:person MAY borrow a book from the library
- THEN:
- P MAY
- return the book BEFORE 1 week
- THEN fulfilled (true)
- ELSE breached (false)
- P MAY
- OR (if the above is true, we short circuit to fulfilled; if it is false, then we continue evaluation)
- P MAY
- return the book BEFORE 2 week
- AND
- pay $100 fine
- THEN fulfilled
- ELSE breached
- P MAY
- OR
- P MAY
- return the book BEFORE 4 week
- AND
- pay $200 fine
- THEN fulfilled
- ELSE breached
- P MAY
- OR
- P MAY
- keep book
- AND
- Library MAY charge $500 replacement cost to the credit card on file
- THEN fulfilled
- ELSE breached (the charge didn’t go through, and so we send the lawyers to your door to recover the book)
- P MAY
Laypeople will analyze this contract as follows:
Bound: … if the goal is that P doesn’t pay a fine and doesn’t end up in BREACHED.
Bound: … if the goal is that P doesn’t end up in BREACHED state.
this is a property assertion – the MUST is an alethic modal, not a specifically deontic modal.
The “must” in the analyses is an alethic modal bounded by specific goals, not a deontic or constitutive modal!
Constitutive rules follow the template:
- for X to be considered Y in context Z, X MUST BE …
Regulative rules follow the template:
- UPON some event, or ALWAYS
- Party P
- if they meet criteria (“WHO”)
- if the world meets certain criteria
- deontic MAY/SHANT/MUST DO some action
- BEFORE/AFTER some deadline
- THEN C1 ELSE C2
Framing: is (2+4) * (5+3) a “fundamentally” multiplicative or a “fundamentally” additive formula? Hmmmm.
Deontic:
- Party P
- MAY do X
- IF and only IF
- P qualifies
Constitutive:
- P qualifies
- IF and only IF
- P previously did Y
From this we infer:
- P MAY Y
- THEN
- P MAY X
Or:
- To (be able to) do X, P MUST (have done) Y
And then the “to be able to” gets dropped out of the explicit stateement, because it moves into the implicit goal bound!
- P MUST Y
Bound: goal = P MAY X
which looks like two purely regulative rules chained together; the constitutive has been compiled out.
But it could be analyzed slightly differently:
- do Y, P MUST BE qualified
- to be qualified, P MUST HAVE done X
All of these readings are semantically equivalent!
We have dealt with this in the past, let’s dig up the old write-up.
But basically it can be in a state of indeterminacy until some event happens which resolves the conditions one way or another and then the rule operates.
See also: conveyanc.es
If anyone is 21 or older at any time in the previous tax year, etc
moving point of reference around
Netflix: “The Gentlemen” S01E01
- “To my daughter, Charlotte,
- I leave the Endurance [some kind of boat],
- with the condition that she sail around the world on her
- in the next six months.”
- (“Well done, Chuckles.”)
- “As well, a trust fund of £1,000 a week
- until she marries
- a man.”
Even the non-regulative decision logic deals with Boolean and Numeric-valued expressions
DECIDE the Payout :: Number IS SUM NumA :: Number NumB :: Number NumC :: Number IF PayoutRuleApplies
WHERE DECIDE NumA :: Number IS IF ConditionA THEN … ELSE 0
DECIDE ConditionA :: Boolean IS True WHEN X < Y False WHEN X > Y False OTHERWISE
DECIDE ConditionB :: Boolean IS ANY/OR [ Bob is over 21 years old , Bob is under 7 years old ]
DECIDE PayoutRuleApplies IF TheRegulatorSaysPayoutRuleApplies
What if the PayoutRuleApplies == False? There is some kind of Default/Maybe monad so that numbers default to identity 0.
Section 1337(a): You can cite as a schmdudction (this is a term of art) whatever interest you paid within the tax year on your debts. [nothing else in Section 1337(a).] [...other sections…] Section 1337(f): i) If you are not a corporation, you cannot invoke as a schmdudction any personal interest paid or accrued during the tax year. (ii) For purposes of this subsection, the term “personal interest” means any interest allowable as a schmdeduction under this chapter other than [...] any raxified moodrigible interest [nonsensical term of art to make cheating harder]
data Interest = Personal | NonPersonal
data Person = Natural | Corporation
data TaxYear
canCite :: Person -> Interest -> TaxYear -> Boolean
canCite p i _
| p /= Corporation && i /= Personal = False
| otherwise = True
canCite _ _ _ = True
Language rule: subsequent things override earlier things
(a) DECIDE canCite IS True IF | always | == 0
…
(f) DESPITE (a) DECIDE canCite IS False IF | Corporation … Personal … | == 2
The Dev-facing IDE could search for un-ordered pairs of rules that define the same terms (“canCite”) and ask the developer for explicit ordering.
We can apply Lex Specialis and Posterior Derogat to assume ordering, and then we have to figure out how the two doctrines fight.
We can do this in an “adversarial” elicitation dialogue, where we use a backend to come up with concrete examples that have ambiguous evaluations, and we ask the user to choose which is “correct” / “desirable” / “prioritized”.
Boolean terms can be annotated with a TYPICALLY default value.
A program can be evaluated with those values set to defaults, or explicitly overridden by the user.
That’s enough to support default and defeasible logic.
X is a Penguin (TYPICALLY false). X is a bird (TYPICALLY true.)
Birds can fly unless they are penguins.
Can X fly?
given: { X is a bird } ==> X flies. Because we are using the assumption X is not a penguin.
given: { X is a bird, X is a penguin } ==> X does not fly.
PARTY Customer MAY make claim WITHIN 1 YEAR OF last renewal
THEN PARTY Customer MAY renew insurance WITHIN 1 YEAR of last renewal THEN residuum
ELSE PARTY Customer MAY renew insurance WITHIN 1 YEAR of last renewal THEN bonus := bonus + 5% – THIS IS THE DIFFERENT BIT AND residuum
DECIDE bonus = 5% * numberOfRenewalsWithoutClaim
The “event sourcing” paradigm:
- EVENT yyyy-mm-dd RENEWAL occurred
- EVENT yyyy-mm-dd CLAIM occurred
- EVENT yyyy-mm-dd RENEWAL occurred
- EVENT yyyy-mm-dd RENEWAL occurred
what if we don’t have explicit type annotations, the system has to figure it out.
From challenge (1) above, we can infer the following data and world model:
- frobulate is an action that a person can take – in an OOP rendering, the Person class has a
frobulate()method - Person has a colour attribute
- Person’s colour attribute can take red as a value, and presumably others
- Person has a size attribute
- Person’s size attribute is numeric
- Person can be the subject of a shape predicate
- the shape predicate takes an input of
rectangle | circle | _– in Prolog it would be something likeisRectangle(Person)isCircle(Person)isOtherShape(Person)
- alternatively, we could restyle to
isShape(Person, rectangle) :- ...isShape(Person, circle) :- ...isShape(Person, _).
- Person has an electrical charge attribute which could be positive; alternatively, they could not have electrical charge attribute, see discussion above.
Oh, and:
give actual type errors lolol
we need to figure out what PURSUANT TO means, or DUE TO, or BY WAY OF
wonder what GPT thinks about those idioms
When is the earliest possible time that … event X could occur?
What sets of conditions/circumstances would be necessary for X to arise in future?
in the actor model, message-passing is the key operation.
we borrow Epistemic Modals:
“Party X may obtain from Party Y certain information I”
unpacks to
PARTY X MAY notify PARTY Y with demand for information I THEN PARTY Y MUST notify PARTY X with information I ELSE fulfilled
The notify keyword is a special action
if it is parameterized with that, we infer that the notified party knows something:
PARTY X MAY notify PARTY Y that something
and we can subsequently use that in reasoning, e.g. to evaluate “if party x can reasonably expect party y to be aware that such-and-such”
or, shorthand, “if party Y knows something”
The rule: downstream clauses inherit bindings defined by upstream clauses.
A clause could be a shared downstream of multiple upstreams.
The type inference checks to see if any upstream fails to define the bindings that are used by the downstream and defined by other upstreams.
§ There's Something About Money
DECLARE Person
HAS Name IS A String
DECLARE Money
HAS Currency IS A String
Amount IS A Integer
§§ It Begins
GIVEN m IS A Money
p IS A Person
q " " "
UPON event 1
describing m
PARTY p
MUST pay
() m
to q
BEFORE deadline 1
HENCE Contract2
LEST Contract3
§§ Contract2
PARTY q
MUST do another thing
also involving m
§§ Contract3
PARTY p
MUST pay
id m * 2
to q
Validating all of this is actually quite complicated because we need to trace the sub-contract graph.
Here we have
"It Begins" -> "Contract2" -> "Contract3"
And then we have a problem when a clause doesn’t actually have a § title. Do we want to force all clauses to be titled? Cause right now those §§ lines are optional.
DECLARE pay IS AN ACTION
HAS to :: Person
amount :: Money
If we get tired of making up that “world-model” by hand, we could steal them from Framenet:
- https://remu.grammaticalframework.org/framenet/#/Eng/pay
- https://remu.grammaticalframework.org/framenet/#/Commerce_pay
- https://framenet2.icsi.berkeley.edu/fnReports/data/frameIndex.xml?frame=Commerce_pay
The document hierarchy is structured by the § prefixes of clauses, or sections, or articles:
| § | H1 | Heading level one |
| §§ | H2 | Heading level two |
| §§§ | H3 | Heading level three |
Sometimes a source text will say something like
For the purposes of this section, ... For the purposes of this Act, ...
(https://sso.agc.gov.sg/Act/SGA1982)
So, we need a way to delimit the scope of a definition.
Indeed, sometimes the source text will say
For the purposes of this section, the next section, and subsection A.52.II.a.i
We need to borrow the notion of text anchors that are used by cross-referencing software like Word and InDesign: instead of the extensional “A.52.II.a.i” we need to tag that section with an intensional name and then have the name resolve to paragraph number at serialization time. Let’s pretend that section is named something like <<More Exceptions>>.
Proposed syntax:
WITHIN this, next, <<More Exceptions>> GIVEN c IS A Contract DECIDE c ...
This should compile to
“For the purposes of this section, the next section, and the section titled More Exceptions…”
and within those sections, the decision rule provided is active.
However, outside of those sections, the decision rule provided is not active.
How do we deal with activation for other kinds of rules – regulative and DECLARE / DEFINE rules?
“A natural person has a name, a gender assigned at birth, a birthdate, and a country of birth.”
“For the purposes of subsection 25.5, a natural person also has a race attribute.”
By default, every clause has WITHIN this
which includes descendants.
1.—(1) In this Act, “contract for the transfer of goods” means a contract under which one person transfers or agrees to transfer to another the property in goods, other than an excepted contract.
WITHIN Act
GIVEN c IS A Contract
DECIDE c IS a contract for the transfer of goods
IF a person transfers
OR agrees to transfer to another
the property in goods
UNLESS c IS excepted contract
The above turns “a person” … “the property in goods” into a PrePost label around [“transfers” || “agrees to transfer to another”]
(2) For the purposes of this section, an excepted contract means any of the following: (a) a contract of sale of goods; (b) a hire-purchase agreement; (c) a transfer or agreement to transfer which is made by deed and for which there is no consideration other than the presumed consideration imported by the deed; (d) a contract intended to operate by way of mortgage, pledge, charge or other security.
WITHIN this
GIVEN c IS A Contract
DECIDE c IS excepted contract
IF c IS a contract of sale of goods
OR c IS a hire-purchase agreement
OR c IS a transfer
OR agreement to transfer
AND made by deed [... AND C IS made by deed ...]
AND there is no consideration for c other than the presumed consideration imported by the deed
OR c IS intended to operate by way of mortgage
OR pledge
OR charge
OR other security
And then we encounter these tautologies:
(3) For the purposes of this Act, a contract is a contract for the transfer of goods whether or not services are also provided or to be provided under the contract, and, subject to subsection (2), whatever is the nature of the consideration for the transfer or agreement to transfer.
Did you notice the ellipsis/elision?
WITHIN Act
GIVEN c IS A Contract
n IS the nature of the consideration for the transfer or agreement to transfer
DECIDE c IS a contract for the transfer of goods
IF c IS a contract for the transfer of goods
AND services are also provided
OR to be provided
under the contract
OR not
OR n
OR NOT n
Uh, isn’t that a function with f a b _ so let’s not talk about c
Prolog would struggle with this, because it would loop.
transferOfGoods(C) :- actualRule(C).
transferOfGoods(C) :- transferOfGoods(C), True.
- A pet owner who has a cat must pay $500 in pet licensing fees.
- A pet owner who has a dog must pay $1000 in pet licensing fees.
I own two cats. I pay $500.
I own both a cat and a dog. I pay $1000 in pet licensing fees. The authority says, “we were expecting $1500.” But I say, look, I did what the rule required. The cat $500 is part of the total $1000 which I have to pay.
a prime number is a whole number greater than 1 that cannot be exactly divided by any whole number other than itself and 1 (e.g. 2, 3, 5, 7, 11).
Let’s pretend some dead English lord wanted to describe prime numbers in the 17th century:
A prime number is a whole number. A prime number is greater than one. A prime number has no other divisors.
This is to be read as a system of constraints implicitly conjoined with AND.
// n is a whole number
GIVEN n IS AN Integer
DECIDE n IS prime
IF n > 0
// greater than 1
GIVEN n IS AN Integer
DECIDE n IS prime
IF n > 1
// that has no other divisors
GIVEN n IS AN Integer
DECIDE n IS prime
IF divisors of n == [1, n]
We have to be careful because typical Prolog semantics would allow 10 to be prime, because it satisfies the second criterion.
So we have an interpretive challenge: given a list of subsidiary predicates, all the subsidiary predicates must be true, for the higher-level predicate to be true:
isPrime(N) :- whole(N), greaterThanOne(N), noOtherDivisors(N).So we have to be sensitive to the implicit conjunctions.
In the Contract for Transfer of Goods case, the ellipsis is … monadic!
https://sso.agc.gov.sg/Act/SGA1982#pr2-
2.—(1) In a contract for the transfer of goods, other than one to which subsection (3) applies, there is an implied condition on the part of the transferor that in the case of a transfer of the property in the goods he has a right to transfer the property and in the case of an agreement to transfer the property in the goods he will have such a right at the time when the property is to be transferred.
DMN decision tables are tabular. Our dmnmd reuses editors’ markdown and org table modes for this, but the inspiration really is Jetbrains MPS’s support for inline decision tables: https://youtu.be/RpQ5JVQaJx4?si=qc_ezzndoaxkJpoN&t=499
Our choice of web editor should be informed by support for tabular editing.
We can implement DMN itself relatively simply.
It has already been done once: see DMNMD.
| Thing to explain | Simple explanation | Haskell evidence |
| (operator, inputs, result) | ||
|---|---|---|
| (or, [(a,Bool)], True) | The result is true because at least one of the sufficient conditions held. | [ x | (x,y) <- inputs, y ] |
| (or, [(a,Bool)], False) | The result is false because none of the sufficient conditions held. | All of these were false: inputs |
| (and, [(a,Bool)], True) | The result is true because all of the necessary conditions held. | All of these were true: inputs |
| (and, [(a,Bool)], False) | The result is false because at least one of the necessary conditions did not hold. | [ x | (x,y) <- inputs, not y ] |
“Necessary” and “sufficient” are, of course, word-problem versions of “conjunctive” and “disjunctive” elements.
The above needs adaptation to work for ternary logic. We sometimes want negation as failure, sometimes we don’t, the context monad has to specify that.
We can compose these simple boolean-oriented explanations with arithmetic equalities, e.g.
| Thing to explain | Simple explanation | Haskell evidence |
(operator, inputs, result) | ||
|---|---|---|
| (any (> 0), [Ord a], True) | The result is true because at least one of the inputs was non-negative. | [ x | x <- inputs, f x ] |
| (any (> 0), [Ord a], False) | The result is false because all the inputs were negative. | inputs |
| (all (> 0), [Ord a], True) | The result is true because all the inputs were non-negative. | inputs |
| (all (> 0), [Ord a], False) | The result is false because at least one input was negative. | [ x | x <- inputs, not $ f x ] |