Skip to content

Latest commit

 

History

History
1335 lines (868 loc) · 74 KB

intro-course.org

File metadata and controls

1335 lines (868 loc) · 74 KB

An Introductory Course in Formal Languages and Protocols in Computational Law

This document lives at https://github.com/smucclaw/complaw/tree/master/doc/intro-course.org

Introduction

This course was designed in mid-2017 to survey the field of computational contracts, which is just now emerging from academia toward industrial practice. It has been regularly updated since and was reviewed in 2020.

Audiences

The course is intended for specific audiences.

One, the non-technical reader with some experience with the legal profession, considering a career in legal engineering, unafraid to dip a toe into computer science. A bright young law student, perhaps with some natural affinity for programming, who seeks alternatives to the standard future: junior associate, senior associate, partner, corpse.

Two, the technical reader, perhaps a self-taught or classically educated programmer, who is interested in approaching contract law as a special case of applied computer science.

By the end of this course

You will gain passing acquaintance with the foundational technologies, past and current efforts, and leading figures in the field of computational law in general, and computable contracts and legislation in particular.

Course Structure

This is a self-study course. It’s mostly readings, web pages, and some videos.

If you get stuck, ask for help.

Volume 1 (two days) – Background Survey

Motivation and Explication

  1. What if we could write contracts (and statutes) the way we do programs? (Not to mention compile, test, debug, and verify … or even share and sell.)
  2. http://compk.stanford.edu/ articulates the vision.
  3. Harry Surden (2014) explains computable contracts on his blog (part 1, part 2).
  4. Eventually, professional services will be provided around contract drafting. Wait – law firms already do that! Except, by and large, without technology and tools. Automation is just the first step.
  5. Darmstadter’s Precision’s Counterfeit angsts about the problem from the point of view of a lawyer.
  6. One premise of the approach in this course is that the CS field of Formal Verification has much to offer. In Sep 2017 the Atlantic Magazine discussed how FV could save the world from The Coming Software Apocalypse.
  7. https://www.youtube.com/watch?v=YHri1NdYKS0 Ron Dolin on an Engineer’s Journey Through the Legal System

Some context

What Legalese the Startup Thinks, in slides and videos

A Quick Survey of Prior Art in Computable Contracts

Ready to add some tabs to your browser?

The three most important readings are marked IMPORTANT below. If you print anything, print those. Skim everything else, but read those.

Computable contracts is a narrow segment of computational law, which goes back over 30 years. For a sense of the larger field, see the contents page of Computer Science and Law (1979), the ICAIL retrospective “A History of AI and Law in 50 papers” (2012), and slides from the intro to AI & Law workshop at ICAIL 2017.

Meng gave a presentation covering some of this material at CodeX on 2017-09-09. The novel version of that movie is available at https://github.com/legalese/complaw-deeptech/blob/master/doc/chapter-201707.org (HTML version).

American Work

  1. The earliest work dates back to 1988: skim Ronald Lee’s A Logic Model for Electronic Contracting.
  2. In the late 1990s and early 2000s, Nick Szabo put forward a formal language for contracts.
  3. IMPORTANT – In 2011 some Argentinians published FormaLex. They followed up in 2017.
  4. More recently, Flood & Goodenough published Contract as Automaton (2015, 2017).
  5. In 2016, Josias Dewey of contractcode.io wrote a white paper.
  6. In 2017, Shrutarshi Basu, Ph.D. candidate at Cornell, wrote a conveyancing reasoner: http://basus.me/conveyor/
  7. In 2016 and 2017, William Farmer and Qian Hu at McMaster University produced FCL: A Formal Language for Writing Contracts.

European Work

  1. Knowledge-Based Systems and Legal Applications, 1991: https://www.elsevier.com/books/knowledge-based-systems-and-legal-applications/bench-capon/978-0-12-086441-6
  2. In the 2000s, Jean-Marc Eber wrote Composing Contracts: an adventure in financial engineering. That paper begat MLFi, a domain-specific language for financial contracts. Eber’s company, LexiFi, sells to financial institutions.
  3. In 1999, Aspassia-Kaliopi Daskalopulu wrote a PhD thesis at the University of London on Logic-Based Tools for the Analysis and Representation of Legal Contracts; subsequent work explored model checking.
  4. In 2002, Using Event Semantics for Modeling Contracts came out of the Netherlands.
  5. The Estrella Project ran from 2006 to 2008, out of Amsterdam, and produced LKIF, a legal ontology – one of many; see Approaches to Legal Ontologies. LKIF stands on the shoulders of KIF which was a creation of Michael Genesereth at Stanford and others. See papers such as The LKIF Core Ontology of Basic Legal Concepts which probably has some overlap with the OWL Ontology of Basic Legal Concepts.
  6. In 2005, Adrian Paschke at TUM.de (et al) described ContractLog to cover SLAs. (link)
  7. In 2007, the LegalXML OASIS working group produced the eContracts v1.0 specification.
  8. From 2007 to 2010, in Norway, the CoSoDIS project begat the contract language CL, under Schneider (in Sweden). Browse publications. Particularly, Model Checking Contracts.
  9. IMPORTANT – Chapter 1 of Camilleri’s 2015 Analysing Normative Contracts briefly surveys the field of computable contracts. The rest of the thesis demonstrates applications of CL: contract-oriented diagrams (web), a CNL editor (web), and CLan (Java), a contract language analyzer, produced under the REMU project, funded by the Swedish Research Council.
  10. IMPORTANT – Chapter 1 of Hvitved’s 2012 Contract Formalization comprehensively surveys the prior art in contract languages. That chapter describes many efforts not listed here.
  11. Chapter 2 introduces Hvitved’s language, CSL. CSL was developed as part of POETS under the Danish Advanced Technology Foundation’s 3gERP project. The implementation is in Haskell.
  12. Starting in the 2000s a Newcastle Group including Carlos Molina-Jimenez, Santosh Shrivastava, Abdelsadiq and Ellis Solaiman worked on formalization and model checking. Languages included “X-Contracts” and EROP.
  13. In 2017, Eric Tjong Tjin Tai from Tilburg, NL, published a short paper, ”Formalizing Contract Law for Smart Contracts”.
  14. Most contract law concerns itself primarily with deontic logic; but parties must give notice to one another, and we might call that epistemic logic. Some people in Amsterdam have been working on model checking of epistemic logic.

Prior Art in Regulations, Compliance, and Rules

Contracts are private law; legislation and regulation are public law. Enterprises have internal laws, called Business Rules.

  1. Vinay Gupta (2017) motivated computable legislation in his manifesto The Internet of Agreements: smart contracts need smart law.
  2. In Australia, Guido Governatori has been doing for legislation what the above efforts do for contracts. http://digital-legislation.net describes computable legislation and regulations; see the marketecture PDF. His previous efforts include Regorous and DrContract.
  3. Monica Palmirani chairs the OASIS committee for LegalRuleML (2013 tutorial). See the mailing list archives.
  4. The MIREL Project (Mining and Reasoning with Legal Texts) kicked off in February 2016 and is going strong.
  5. The eContracts standard ran from 2000 to 2007.
  6. The NormeinRete project ran from 1999 to 2007, and has produced work such as xmLegesEditor, part of the XMLeges suite.
  7. In Pittsburgh (with Matthias Grabmair), the LUIMA project attempts to extract semantics from regulations. See also Adam Wyner; and Applying Software Development Techniques to Statutory Drafting.
  8. Akoma Ntoso is a markup XML for legislation.
  9. The Global Justice XML Data Model is a data reference model for the exchange of information within the justice and public safety communities.
  10. The Linked Open Vocabularies project may list a few contract/legal ontologies.

The name for this field is “RegTech”.

Some Software Projects, Companies, and Consortia

  1. A2JAuthor is a software tool that delivers greater access to justice for self-represented litigants by enabling non-technical authors from the courts, clerk’s offices, legal services programs, and website editors to rapidly build and implement customer friendly web-based interfaces for document assembly.
  2. Business Rules Engines have been around forever: Oracle Policy Automation dates back to 2008. Neota Logic is a recent entrant. See also Drools, Jess, iLog. IBM Watson’s Debater does a bit of this.
  3. Ben Grosof’s company Coherent Knowledge commercializes Textual RuleLog (a Prolog variant) as Ergo, to reason through regulatory compliance. See 2016 YouTube demo (15m), 2015 RuleML slides.
  4. R3 has raised a lot of money. They work with banks, because that’s where the money is. They run summits on smart contracts and have published on smart contract templates: foundations and requirements (2016). See slides from June 2016 and June 2017. Their demo runs ISDA master templates through an end-to-end proof of concept prototype against a DLT/blockchain.
  5. ISDA, the trade association, encourages the use of FpML.

Prior Art: Non-Computational Contracts

We call this the “document assembly” or “document automation” industry.

Commercial efforts

Opensource Template and Expert Systems

Expert Systems

Why aren’t template approaches good enough?

Conferences and Books

Skim the proceedings of past conferences.

Researchers

European researchers tend to be CS professors with an interest in law.

US researchers tend to be law professors with an interest in software.

European researchers

  • Gerardo Schneider, CS Professor at the University of Gothenburg, Sweden. (Connected with CL)
  • Gordon Pace, Associate CS/ICT Professor at the University of Malta. (publications)
  • John J. Camilleri, Ph.D. student at Chalmers University of Technology and the University of Gothenburg, Sweden.
  • Guido Governatori, Senior Principal Researcher at NICTA Queensland, Australia. (Connected with digital-legislation.net)
  • Giovanni Sartor, Professor, Legal Informatics, European University Institute of Florence.
  • Adam Wyner, Lecturer, University of Aberdeen, focuses on modeling argumentation and legal reasoning.
  • Rinke Hoekstra, VU University Amsterdam, is the LKIF OWL guy.
  • Peter McBurney at King’s College London is interested in blockchain smart contracts.

USA!

Organizations with related interests

Mostly in the blockchain / smart contracts space.

Other Resources

Legalese’s ”Past” page attempts to survey the research.

Legalese’s ”Present” page shows the subset of today’s LegalTech industry landscape related to contracts.

Volume 2 (one semester) – Introduction to L4

This section is under construction.

This volume teaches L4. It will take a few months to get productive.

As a newly fledged legal developer, you will be ready to use the language and its tools to read and write contracts-as-code and legislation-as-code.

You will be able to generate visualizations and operate the verification engine.

You can start contributing to opensource libraries of contract code. Share your work on Github.

Contents

Motivation

Learning Exercise: Shipping Boxes

You and your life partner recently retired from a long and successful career in software engineering. As a retirement job, you decide to open a small grocery convenience store franchise together. You have spent six hours a day pair programming with your partner for the last 30 years, and you think that a change of pace will be pleasant for the two of you. The grocery franchise headquarters sends you these rules:

Delivery is offered for standard or non-standard box when more than half full. Delivery is free when a standard box is more than half full and contains at least $100.00 of groceries. Delivery of all non-standard boxes is charged.

You print those three sentences on a piece of A3 poster paper and tell your two junior staffers to post it on the wall next to the eggs and milk. You and your partner go out to run an errand. When you get back, the place is a mess! All the eggs are smashed and the milk is spilled. “What happened?” you ask. One of your junior staff has a black eye; the other has a bruised chin. They answer: “customers kept coming to us with different combinations of boxes, fullness, and grocery value. And we couldn’t agree on what the rules meant. We used our discretion, but we would decide similar cases differently for different customers. The customers started to fight with us. They called us racist. Then we started to fight with each other; we called each other stupid. Now we need more eggs.”

You say to the staff, “come on, how hard can this be? Take down the poster. We’ll do a new version.”

Reaching for a fresh sheet of paper, grinning at your partner because it feels like you’ve done this a thousand times before, you say: “Shall we begin?”

Before you read more about this exercise online, try to rewrite those rules yourself. As this is a learning exercise, feel free to produce multiple representations as you sketch your way toward a goal. Use any formats or languages you like: you can write functions in C, Javascript, or Python. You can write a logic program in Prolog, if you know Prolog. You can set up a system of SQL queries, if you know SQL. You can draw a flowchart, or a decision tree, or a decision table. Or you can draft it in English.

This exercise was first posed on Twitter: https://twitter.com/jrpotvin/status/1264895071549349889?s=20. A few experts in computational law responded by offering implementations in a range of different notations and languages. This is called “programming chrestomathy”. In practice, it means, “I need to do some basic thing in a new language I’m learning. I’ll go look it up on Rosetta Code”.

After you have produced your version of the rules, run these test cases, and compare your outputs to your classmates’.

What happens when:

  1. a standard box, more than half full, contains $200 of groceries?
  2. a non-standard box, more than half full, contains $200 of groceries?
  3. a non-standard box, less than half full, contains $200 of groceries?
  4. a standard box, less than half full, contains $200 of groceries?

Your classmates may produce implementations that disagree with yours: they may return different outputs for the same inputs. You might believe they are wrong; they might believe you are wrong. What is going on? Is there a bug in their code? A bug in your code? A bug in the spec? As experienced programmers, how do you approach this situation?

Discuss.

This exercise introduces a number of concepts:

  • qualifiers as operators: X when Y. Y => X versus Y <=> X.
  • operator binding and precedence; anaphora resolution
  • conjunctive and disjunctive expansion
  • quantifier binding: what is the difference between “delivery of all non-standard boxes is charged”, or “all delivery of non-standard boxes is charged”?
  • rule fragments and granularity; clauses and sub-clauses.
  • binary versus ternary logic – the law of the excluded middle – the closed-world assumption.
  • natural language versus propositional logic
  • Logical implication versus Gricean implicatures. https://plato.stanford.edu/entries/implicature/#GricTheo
  • ontological representation of concepts

Warm-Ups: Trying Out Some Existing Contract Language Environments

  • Visit AnaCon, CL, Clang. Observe C-OD.
  • Visit the Basus environment.
  • Visit CSL and POETS.
  • You should at least learn SQL.

The Be-All and End-All of Contract Languages

Introduction to L4.

L4 is basically CL’s extensions bolted on top of a CSL core.

Using L4 to develop contracts.

Write your first contract.

Syntax: Control Flow and Clause Composition

Syntax: Rules

Syntax: Genre Extensions

financial agreements

startup investments

corporate law

employment agreements

NDAs

ESOPs

conveyancing

maritime agreements

Review the contract library.

Jurisdiction customization.

Using L4 to develop legislation.

Write your first bill. Rule defeasibility.

Review the statute library.

Secondary Weapon Enhancements

Automated Bug-Finding.

Introduction to CTL* and model checking.

http://web.iitd.ac.in/~sumeet/slide3.pdf

Introduction to TLA+. http://lamport.azurewebsites.net/tla/book-02-08-08.pdf

Review of Model Checking with CL.

Property verification via model checking.

Conflict detection via model checking.

A Bestiary of Standard Bugs
Type Errors.

Debt vs Equity.

Action Conflicts.
Rule Conflicts.
Loopholes.
Dangling References.
Undefined Terms.
Inconsistency with Legislation.

ambiguity: “These public areas could be any public path, a green or an open space that is managed or maintained for the Government or a public body, and is accessible to the general public without payment of any fee,” the authority said.

https://www.todayonline.com/singapore/no-exercising-dog-walking-within-condominiums-common-areas-bca?cid=h3_referral_inarticlelinks_03092019_todayonline

Model Checking Property Violations.
Incompleteness.

Multilingual Natural Language Generation.

Introduction to GF.

https://www.youtube.com/watch?v=x1LFbDQhbso

http://www.grammaticalframework.org/~aarne/ud-gf-malta-2017.pdf

See Translating Formal Software Specifications to Natural Language

How would you go upstream from https://writing.kemitchell.com/2020/04/18/Common-Form-Simplified.html in GF?

English Output
Italian Output
Indonesian Output
German Output

https://papers.ssrn.com/sol3/papers.cfm?abstract_id=596668

aside: why NLP is hard

the missouri challenge: http://revisor.mo.gov/main/OneSection.aspx?section=233.285&bid=12522&hl=

Type Checking.

Sanity checking.

Domain Expressions.

PCSL.

Debt vs Equity example.

Visualization. Scenario explorers.

Ambiguity.

https://papers.ssrn.com/sol3/papers.cfm?abstract_id=332984

https://papers.ssrn.com/sol3/papers.cfm?abstract_id=1288689

Call-Outs to Oracles.

Integration with Blockchain-based automated execution environments

Advanced L4

The Interpretation Combinator: “It Depends”

Ternary Logic: Yes, No, Maybe

Building an Expert System in L4

Social Implications

Github for Contracts

Volume 3 (one to two years) – Advanced Background

This section is under construction.

There is enough material in here for a Master’s degree. If you go fast, you could cover it all in a year. If you go deep, it might take two.

You will understand the mathematical logic and architectural decisions that inform the design of the L4 language.

You’ll be ready to start developing and extending the core language itself, the way Guido van Rossum develops Python, the way Mats develops Ruby, the way DHH developed Rails.

When you attend academic conferences about law and logic, you will be able to follow the arguments of wizards about the fine points of action logics vs state logics; about whether Hvitved loses anything by defining permission in terms of counterparty obligations; about whether CSL, CL, or FL better sidesteps the paradoxes of Standard Deontic Logic; about whether Governatori’s defeasible logics map elegantly to SBVR and LegalRuleML.

First, Be Well

Motivation and Problems

  • How to be a Genius (vs a Consultant), with thanks to ed kmett.
  • three generations of document assembly

Prior Art: Computational Law Projects

We review the above projects in more detail.

Prior Art: Rule languages. Declarative Programming.

Legal Theory

from Hohfeld and the Analysis of Rights, in Jurisprudence, quoting Rosecoe Pound:

A power is a legally recognized or conferred capacity of creating, divesting, or altering rights, powers and privileges and so of creating duties and liabilities. It has been called a capacity of altering the sphere of rights orjural relations of persons, using these terms to mean rights in the broader sense. (1959, 93)

contrast https://www.postgresql.org/docs/9.6/sql-grant.html

Smart Statutes

http://idiomsoftware.com/docs/deloitte%20brea%20submission%20final.pdf http://idiomsoftware.com/pages/solutions/currentrecentprojects.aspx

NOVA http://www.nova-hub.com/e-government/

https://discuss.digital.govt.nz/d/OI3Xdw68/comment/2258?membership_token=p9cdLqYpaUGiqJhpRQYNNK38&utm_campaign=discussion_mailer&utm_medium=email&utm_source=new_comment

Government desire for rules as code

http://ruleml.org/talks/MarkusTriska-LogicInThePublicSector-RuleMLWebinar-2020-03-25.pdf

EU EMIR reporting regulations as code: https://etendering.ted.europa.eu/cft/cft-display.html?cftId=6051

BoE work: https://www.fca.org.uk/innovation/regtech/digital-regulatory-reporting

https://18f.gsa.gov/2020/05/12/rapid-implementation-of-policy-as-code/

Past Projects

Real World Use of Rules as Code in Singapore

https://www.sciencedirect.com/science/article/pii/S0926580515000370 in the BIM field Survey of the Rules Landscape: Technologies and Tools

Decision Tables, DMN, SBVR, BDDs

Prolog, Flora-2, RuleLog from Coherent Knowledge; see Jason Morris’s work

constitutive/definitional vs prescriptive/behavioral rules (LegalRuleML) http://www.rulespeak.com/en/ and http://www.brsolutions.com/wp-content/uploads/2016/10/TableSpeak-Primer.pdf RAAP, Xalgo, OpenFisca, Background Reading on Smart Statutes History – https://repository.law.umich.edu/cgi/viewcontent.cgi?article=1028&context=articles https://sci-hub.tw/10.1145/112646.112660# https://cgi.csc.liv.ac.uk/~tbc/publications/ICAIL87supp.pdf https://www.researchgate.net/publication/317044637_Legal_Ontology_for_Open_Government_Data_Mashups https://aiasworkshop.org/AIAS2019.html https://sites.google.com/view/legregsw2019/home

better Rules

discussion [2019-05-01 Wed] with Brenda in NZ about the benefits thing

https://twitter.com/mattwadd/status/1123270422152318977

https://twitter.com/BR3NDA/status/1123364483479375872

legislative source

http://www.legislation.govt.nz/act/public/1973/0005/latest/DLM409673.html

3 Rates rebate

  1. A ratepayer who, at the commencement of a rating year, was the ratepayer of a residential property

    is entitled, on application in that year, to a rebate of—

    (a) so much of the rates payable for that rating year in respect of the property as represents—

    (i) two-thirds of the amount by which those rates exceed $160,

    reduced by—

    (ii) $1 for each $8 by which the ratepayer’s income for the preceding tax year exceeded $25,180, that last-mentioned amount being increased by $500 in respect of each person who was a dependant of the ratepayer at the commencement of the rating year in respect of which the application is made;

    or

    (b) $630,—

    whichever amount is smaller.

(1A) A ratepayer who, at the commencement of a rating year, was the ratepayer of a residential property, and later during that year becomes the ratepayer of another residential property, is entitled to a rates rebate under subsection (1). The amount of the rebate must be apportioned according to the amount of time the ratepayer was the ratepayer of each residential property during the rating year.

(2) The Governor-General may from time to time, by Order in Council, amend the provisions of subsection (1) by substituting any amount for any amount specified in that subsection.

OpenFisca implementation

https://github.com/ServiceInnovationLab/openfisca-aotearoa/blob/master/openfisca_aotearoa/variables/acts/rates_rebates/rates_rebates.py#L36

(beard tax example)

https://github.com/ServiceInnovationLab/example-rules-as-code/blob/master/legislation.pdf

my reactions
“there’s got to be a better way!”
alleged bug in the code

https://twitter.com/BR3NDA/status/1123374702502662144

We put it into open fisca, and its been running in production for nearly 3 years. (3 years of Rebates). I’ve got a report that its not doing the right numbers just for this year, but not much further info. so I’m rereading that legislation to see they mean by “wrong numbers”.

what was the bug in the code?
test cases
test 1

rate_payable = 5000 ratepayer_income = 50000 dependents = 4

what is the rebate?

2/3*(5000-160) - (50000 - (25180 + 500*4)) / 8

2/3*(rate_payable-160) - (ratepayer_income - (25180 + 500*dependents)) / 8

openfisca source code
class rates_rebates__rebate(Variable):
    value_type = float
    entity = Titled_Property
    definition_period = YEAR
    label = "Yearly rebate applied to housing rates."
    reference = "Obtained from spreadsheet at Department Of Internal Affairs Innovation Lab"

    def formula(titled_properties, period, parameters):
        income_threshold = parameters(period).entitlements.rates_rebates.income_threshold
        additional_per_dependant = parameters(period).entitlements.rates_rebates.additional_per_dependant
        initial_contribution = parameters(period).entitlements.rates_rebates.initial_contribution
        maximum_allowable = parameters(period).entitlements.rates_rebates.maximum_allowable

        # sum allowable income including all the dependants for property
        allowable_income = (titled_properties.sum(titled_properties.members('rates_rebates__dependants', period)) * additional_per_dependant) + income_threshold

        # wrapping floor math function is non legislative and only to conform output of variable with existing infrastracture.
        excess_income = floor((titled_properties.sum(titled_properties.members('rates_rebates__combined_income', period)) - allowable_income) / 8)

        # minus the initial contribution
        rates_minus_contribution = titled_properties('rates_rebates__rates_total', period) - initial_contribution

        # perform the calculation
        rebate = rates_minus_contribution - ((rates_minus_contribution / 3) + excess_income)

        # Ensures the results aren't negative (less than 0) or greater than the maximum_allowable
        return clip(rebate, 0, maximum_allowable)
how did the bug arrive in the code?

surfacing bugs is a pain in the ass; consider the case reported in https://www.modernanalyst.com/Resources/Articles/tabid/115/ID/3109/The-Role-of-SQL-in-Decision-Centric-Processes.aspx

We have another example that demonstrates this in practice. A government front-line department had miscalculated average daily pay for a decade, thereby underpaying all termination payments. The average daily pay had to be recalculated for the entire period from original source data. So in the new process, daily accumulators were created for every day that an employee was employed. Then every payment that spanned any given day needed to be added to the day’s average on a pro-rated basis: for instance, weekly and overtime earnings, shift allowances, various monthly, quarterly, and annual adverse condition and other bonuses, annual and long service leave etc. The ‘provenance’ of each and every payment made had to be assessed against the provenance of each individual daily accumulator – that is, the context of every payment to the employee had to be matched with the context of the daily accumulator, while that specific accumulator was being processed.

could we do better? how would we know we are doing better?
we could rewrite the implementation in OpenFiscaa discussion of OpenFisca

https://openfisca.org/doc/coding-the-legislation/25_vectorial_computing.html vectorial computing basically means that all formulas operate in the Array monad.

this idea of “vectorial” computing shows up in Prolog and in Alloy as well.

we could rewrite the implementation in some other pet languagebut all of these rewrites would suffer the same problem as the originalDunning-Krueger effectthis has been discussed inhttps://sci-hub.tw/10.1145/112646.112660#how can we have more confidence in the software we produce?

this is an old question in software engineering

we offer three ways to answer this question:

  • tests (which descends from Zermelo’s answer to the Russell Paradox: set theory)
  • correctness by construction (which descends from Russell’s answer to the paradox: type theory)
  • natural language isomorphism

tests expand to model checking, SAT/SMT

correctness by construction expand to ITP/ATP CoQ, B, specification languages

these approaches intertwine; Alloy and TLA+ backend to SAT engines and model checkers

natural language isomorphism is a novel approach: it complements the other two.

they could have had test cases and illustrative examples
test cases might have surfaced the bug

the QuickCheck tradition

(and quickcheck for state machines! https://github.com/advancedtelematic/quickcheck-state-machine/)

tests for undefinedness and errors arising from compositional complexity; see Hillel

they could have written it code-first, English-second
of course this was too much to ask in 1973
but code in what language?
anyway, how would this piece of code be represented in other languages?
GPLspythontypescriptscalahaskellracket or common lisprule languagesakoma ntoso

doesn’t quite cut the mustard

ruleml and legalruleml SBVRDMNPL/SQLxalgorithmsprolog https://www.amzi.com/articles/prolog_under_the_hood.htmflora-2LPS logicalcontracts worksheets / symbiumdrools and others in the JRS-94 familyback to openfisca
Let’s introduce a better way: L4 brings NLG and FV
representing the rule in L4 is no less readable

show

alternative verbosities are available, in various styles of compactness vs normalization
thanks to the NLG it is possible to produce natural language

http://www.grammaticalframework.org/doc/tutorial/gf-tutorial.html#toc134

thanks to the reversibility of GF it is possible to parse natural language

library for arithmetic

library for deontics

library for synonymous locutions, synonymous vs non-synonymous rearrangements

contra Coode (1845) and Adams (2018), real-world legal grammars require multiple ways to say the same thing

in other words, they require synonyms; though sometimes the synonyms are not quite synonyms, because of nuance; as we have just shown, ha ha.

see also vagueness vs ambiguity in Claire Hill and in Layman Allen

the first thing that L4 gives drafters is rich IDE support through LSP
Here is an editor that produces natural language through the magic of Language Server Protocol
pedagogy: we implement a simple version of L4 constrained to a theory of conditional predicates * integer and real arithmetic

this is a larger thing https://www.researchgate.net/publication/221665834_The_GF_Mathematics_Library

here is the abstract languagehere is the concrete syntaxhere is the GF grammaractually here are multiple GF grammars; some more purple, some more plainhere is the LSP working with emacshere is the LSP working with VS CodeEclipse?

http://www.molto-project.eu/sites/default/files/freerbmt2012.pdf

for our Eclipse specialist to review:

it’s really the LSP language server that knows how to do cool tricks.it can do live output to english; as you type, the english changes.

(well, every time your buffer contents are syntactically valid)

autocompletionautomated testinglive output to French!each automated test brings up an explainerhere is an explainer written in Flora-2 that says why something is the way it is.here is an extraction to an expert system shell, that automatically asks relevant questions

like docassemble?

here is a debugger for the language that prints the state of a rule during executionhere is the test suite using Gherkin / Zenroom syntaxhere is a more advanced test suite that uses some TLA+ / LTL / CTL / Alloy syntax for assertionshere is the specification transpiled to a form suitable for running in a corresponding FV enginehere is the FV engine automatically finding bugs in your regulationhere is the abstract language compiling to all the other languages we have visited so farhere is the abstract language compiling to a visualization

see what haapio and passera and hagan have been working on

but wait, there’s more; let’s also compile it to blockchain languages alsoethereumbitcoinadjointkadenaagorictezosagrellozenroometca summary of benefitsone input, multiple outputs

bringing the benefits of controlled natural languages

features useful to the drafter

IDE livecoding

reading it in natural language https://www.sciencedirect.com/science/article/pii/S0167642314000069?via%3Dihub

test suites

code sharing, working with other jurisdictions

features useful to the user

interface; expert system; explainer; who to complain to

features useful to the power user

how to submit a pull request in your current democracy

features useful to industry

“what-if” scenario modeling

open questionsshould we make more use of Attempto

codeco https://link.springer.com/article/10.1007%2Fs10849-012-9167-z

acerules https://github.com/tkuhn/AceRules

but acerules is not enough to do the LSAT

let us get advice from Schneider, Inari, Camilleri

Use Case: terms of service, privacy policies

Other Requirements and Use Cases

A Party has a Right during qualifying portions of the business process

Our expression language gives a way to concisely filter the business process states and state transitions for party rights.

Running Code

https://twitter.com/roundtablelaw/status/1201186332120367104?s=21

OWL and LKIF and all that are well and good but how do we reduce this stuff to practice? What does it even mean to reduce a specification language to practice?

Use Case: corporate secretarial paperwork

considered as a planning problem

Planning as a field of AI

Introduction to Legal Ontologies

http://people.cs.ksu.edu/~abreed/CIS890/

the two books:

OWL vs SUMO.

“multi-agent systems”

Introduction to Business Modeling

modal extensions to BPMN

time

https://hal.archives-ouvertes.fr/file/index/docid/921390/filename/iiWAS_2013.pdf

deontics

epistemics

message-passing

Modeling contracts in BPMN, UML, etc

Logical Spreadsheets

http://logic.stanford.edu/people/mkassoff/papers/introtologicalspreadsheets.pdf

consider a simpler DSL for BPMN itself

formal BPMN

BPMN 2.0’s lack of a formal semantics has been addressed by multiple authors:

LTS
https://link.springer.com/chapter/10.1007/978-3-319-28934-2_9
OCL
https://www.researchgate.net/publication/338300241_Enhancing_the_Correctness_of_BPMN_Models
Petri Nets
https://link.springer.com/chapter/10.1007/978-3-319-23063-4_4 and https://www.sciencedirect.com/science/article/pii/S0020025516322782 (RECATNets)
logic programming
https://link.springer.com/chapter/10.1007/978-3-319-03677-9_5

The Interaction of Business Modeling and Games

Introduction to Semantic Web and Rules

RIF
https://www.w3.org/2005/rules/wiki/RIF_FAQ

Introduction to Business Rules

Introduction to KRR

Three Kinds of Reasoning

https://www.emse.fr/~zimmermann/Teaching/KRR/intro-krr.pdf

causeruleseffectreasoningproducestechniquealso
givengivendeductiveconclusionslogiclaw
givengiveninductivetheoriesML, pattern recognitionscience
givengivenabductivemodelsSAT solving, constraint solving, backtracking, ASPjokes. engineering. applied psychology.
givenhistory
givenreligion
givenart

https://twitter.com/clairlemon/status/1253226791163981824?s=21

ReasoningQuestionExamplesProblemsPrimary Programming Paradigm
DeductiveLogic
InductiveMachine Learning
AbductiveAnswer Set

Previous Work

Knowledge representation and reasoning

http://www.mirelproject.eu/publications/D1.1.pdf

e.g. the representation of time: http://ceur-ws.org/Vol-1875/paper2.pdf

http://www.molto-project.eu/workplan/knowledge-engineering

OWL, RDF, SparQL

https://en.wikipedia.org/wiki/SNePS

OWL goes to F-Logic: https://arxiv.org/pdf/0808.1721.pdf

OpenCyc

npacerules

https://wiki.opencog.org/w/AtomSpace

ape lexicon

Grakn

https://en.wikipedia.org/wiki/Curry_(programming_language)

decheem.io

https://carneades.github.io/

c&c boxer

On Logic Languages

Prior Art: Computational Contracts

Introduction to Computational Linguistics

Introduction to Mathematical Logic

What does all this mean for us?

Applying these concepts to the legal domain, doing some violence in translation along the way, we might simplify to say:

Epistemic Logic
Did Party A give notice to Party B about Fact F? Party C represented & warranted, in a contract already signed, that they had no knowledge that Fact F might be true; they believed it was false. Can Party D demonstrate that Party C was lying? Perhaps if Party D gave Party C notice about Fact F being true before the contract was signed.

https://en.wikipedia.org/wiki/Speech_act#In_multiagent_universes

Deontic Logic
Is Party A obliged to perform act X by deadline D?
Temporal Logic
Is condition C always or sometimes true across a time span T1 to T2?
Defeasible Logic
You have to do what Dad tells you to do, unless Mom tells you differently.
Dynamic Logic
Let’s model the future as a set of actions and assertion/invariants that hold or don’t, after those actions. If Party A performs action X, then they must perform action Y immediately afterwards or they will breach the contract. If Party A checks in luggage weighing more than 25 kg, they must immediately pay a $50 surcharge, or they will not be allowed on the flight.
Kripke structures
Once this assertion is true, how do we know it will always be true? What could make it untrue? What can we know about related assertions?
Petri Nets
Visualize our future state transitions.

Introduction to Functional Programming.

  • Introduction to Functional Programming. haskellbook.com.

consider the “cases not exhaustive” from haskell – this should be a key feature of our language, but beyond sum types, to any kind of theory domain partitioning. basically https://ndmitchell.com/downloads/paper-qualifying_dissertation-30_jun_2005.pdf but for law. every time, every possible action by every party, is it accounted for?

https://www.reddit.com/r/haskell/comments/chcd9j/why_is_nonexhaustive_patterns_in_case_a_runtime/

Applications in AI

Apollo vs Dionysus

  • The A.I. Dichotomy: Symbolic vs Statistical, Logic vs Emotion, Apollo vs Dionysus

explainability

Programming Language Theory

  • Programming Paradigms.
  • Types and Programming Languages.
  • Automated Theorem Proving

http://www.leancop.de/mleancop/ https://www.academia.edu/36734121/A_Simple_Semi-automated_Proof_Assistant_for_First-order_Modal_Logics (see citation 5 in particular)

Positional-Slotted, Object-Applicative RuleML (PSOA RuleML) permits relation applications with optional object identifiers and, orthogonally, arguments that are positional or slotted. The resulting positional-slotted, object-applicative (psoa) terms and rules over them were given a first-order model-theoretic foundation (paper, slides), blending slot distribution, as in RIF, with integrated psoa terms, as in RuleML. In order to support reasoning in PSOA RuleML, the implemention of the PSOA2TPTP translator is in progress, which maps PSOA RuleML knowledge bases to the TPTP format, as widely used for theorem provers. With this translator, reasoning in PSOA RuleML is available using the VampirePrime prover. The composition of PSOA2TPTP and VampirePrime to PSOATransRun is being developed at PSOA RuleML. http://ruleml.org/index.html

  • Agda, Idris and CoQ
  • Dependent Types in Haskell
  • Dependent Types in GF

Model Checking and Formal Verification

Relatable (or at least real-world) Examples:

nonself design bug

https://www.aclu.org/blog/juvenile-justice/minnesota-prosecutor-charges-sexting-teenage-girl-child-pornography

sibling(X,Y) :- parent(X,Z), parent(Y,Z).

oops, now i am my own sibling

sibling(X,Y) :- parent(X,Z), parent(Y,Z), X \== Y.

Our Contribution

  • https://en.wikipedia.org/wiki/Cognitive_dimensions_of_notations
  • Introduction to Contract Law.
  • The Clause Construct.
  • Definitions.
  • The Interpretation Combinator: Definitions for the purpose of a context.
  • Legal idioms.
  • Ambiguity vs vagueness.
  • Oracles: calling the expert witness forward in time.
  • Extending the core language with subdomain expression languages.
  • Language Features for L4 concrete syntax
    specification rather than implementation language
    supports refinement to multiple targets
    declarative rather than imperative
    though certain rules may be described “within a ‘do’ monad”
    progressive refinement may be considered an extremely verbose syntax
    imagine giving a class definition using one sentence for each keyword, one paragraph for each attribute (although subclassing represents one approach to progressive refinement which is more cognate). There is some meat to this idea: maybe one family of ideas is (unit testing with manual tests, set-theoretic approaches, case based reasoning); another is (reasoning from principles, type-theoretic approaches, ATP/ITP, property-based testing); is there a convergence between these schools of thought?
    rewriting
    refactoring at the level of macros
    counterfactual
    see for example companies act regarding waiver of AGM: many rules operate as if the AGM had not been waived
    principled reasoning
    overaps with defeasibility, because one principle can override another, and there can be meta meta rules; this reminds me of the metarule logic developed by that japanese dude who presented at salzburg 2017
    default rules
    lurking in the background, provided by legislation and by case law
    defeasibility
    every predicate is augmented with an invisible “well, unless”; this interacts with the “rewriting” feature
    case-based vs rule-based
    some rule decisions can be punted to something more resembling ML case-based reasoning, with KNN etc; see CMMN from OMG
    introspection
    any rule which involves gender shall be adjusted to be gender neutral

Volume 4 (three to six years) – Research Directions

After mastering the above subjects, pick an advanced topic and dive in. You may spend several years advancing the state of the art. For extra credit, move to Northern Europe and attach yourself to one of the professors in the field. You will probably come away with a Ph.D.