The British Nationality Act as a Prolog Program (1986) [pdf]

https://www.doc.ic.ac.uk/~rak/papers/British%20Nationality%20Act.pdf

by Tomte • 1 year ago

35 17 1 year ago

doc.ic.ac.uk

mmastrac• 1 year ago

Even with the apparent certainty you get from code like this, it's still ambiguous without external determination.

Example:

A newborn infant who, after commencement, is found abandoned in the United Kingdom shall, unless the contrary is shown. be deemed for the purposes of subsection (1)

  (a) to have been born in the United Kingdom after commencement and

  (b) to have been born to a parent who at the time of the birth was a British citizen or settled in the United Kingdom.

Notice the vague wording of this law: "unless the contrary is shown". Shown by whom? To what standard? What must be shown?

Much of this exists in commonlaw case law, but all of that would need to be codified into any sort of deciding program.

Perhaps a society could be built around this, but we'd have to build so. much. infrastructure. to manage the links between case law and overall law.

traceroute66• 1 year ago

Such examples can be found all over UK law, it is, as you say in effect a by-product of the common law system.

But also it also comes from the way legislation is written in the UK...

    1. A member of parliament (MP) brings a "bill" to Parliament proposing a new law or a chnge in the law.
    2. If it has legs, then it will end up being debated in Parliament
    3. Almost always politics starts coming into play and MPs of all parties will usually propose real or party-political amendements to the bill which are then debated and voted on.
    4. You then have a ping-pong process with the upper house (Lords), stuff goes back and forth between Lords and Commons ... more amendements are made along the way.
    5. Finally once everyone has come to some sort of agreement it goes to the monarch to be signed into law (this is purely ceremonial, the document is presented to the monarch as a done-deal).

So that's why you end up with all these messy looking and almost incomprehensible pieces of legislation, there's quite a lot of "too many chefs" going on at every stage apart from the first and last.

Therefore as you point out it looking at UK law in the absence of case law is a fool's errand.

It is also where good barristers are worth their money because they are know the case-law like the back of their hand, and if there is no case law for your situation, they will have a good handle on the "letter and spirit" of the law in question and hence your prospects if it goes to court.

eynsham• 1 year ago

Most important legislation, including the BNA, is government legislation (indeed, see the white paper: https://www.uniset.ca/naty/maternity/wpaper.pdf). It is therefore drafted by parliamentary counsel, whose advice remains available when amendments are proposed. Most governments also command sufficient majorities to push this kind of legislation through, or at least to come to consensus on amendments. The relevant passage seems clear enough that parliamentary counsel could have drafted it and so I doubt there were ‘too many chefs’ as you put it (although I haven’t checked Hansard).

It is also hard to see what these drafting habits have to do with the common law system. Points 1–5 could be true of a legislature in pretty much any legal tradition.

drdaeman4• 1 year ago

"unless the contrary is shown". Shown by whom? To what standard? What must be shown?

I have no idea about British law, but... As I get it, here we see the fallback logic that defines some defaults when dealing with lack of information (an abandoned newborn). Here we don't know newborn's nationality, so we must make an assumption - the lawmakers decided they didn't want to have proverbial NULLs in here.

- "What must be shown?" - I could be misunderstanding things (especially because English is not my native language), but I believe the intent here is pretty clear. To me it reads as applicability scope, constraining when the fallback kicks in, so we don't create logical contradictions. My understanding is that it says that if there's a known fact that contradicts (a) or (b) it would make those defaults inapplicable - which is logical, because we can't proceed to assume A if we know that ¬A is true. E.g. if there's a known fact (say, a DNA test or a witness testimony or some other evidence) that confirms e.g. that the infant's parent wasn't and isn't a British citizen or permanent resident, this piece won't apply and we won't consider infant to have been born of such father. I think the program at the bottom of the page 374 (page 5 in the PDF) agrees with me on this.

- "Shown by whom?" - as this is clearly unspecified, can't we safely assume that the existence of the fact alone is what should affect the execution flow, not who brought this fact to the light? That is, I believe it reads so anyone or anything can show it, but only the fact (and its truthfulness) itself matters. Again, don't see the issue here - but I'm curious if you have alternative interpretations how it could be read?

- "To what standard?" - this is the only real ambiguity here. Probably because the lawmakers writing the act weren't exactly capable or even aiming to figure out the theory of truth for a natural language. As I get it, for the legal stuff it's pretty normal to have undefined behaviors and return to them when they are triggered and someone is unhappy about the outcome and goes to the court to follow up and clarify the details. When we're rendering laws as machine programs, we mustn't forget what they apply to - to the society governed by those laws. Unless we're running a simulation, the society is external to the program - and it's the only sane design (that doesn't violate Kant's categorical imperative, so the laws should not treat the society as means to some goal but as the goal itself - if I understand the idea correctly, please correct me if I don't) that any or almost any statement may raise an exception-like situation that would require a human to look into it and fix (thus always deferring ultimate legislating to a rational being's will). In other words, it's our usual "I don't want to think too much about this edge case, gotta ship this thing already, so we'll get to this later if we get an error report". This is the universal mechanism that applies not just to this particular question, but to the other questions above that I thought are clear, if someone disagrees.

HannesWes• 1 year ago

Really fun to see this shared here! It is one of the most famous examples of rule-based reasoning in the field of AI & Law. The other option is case-based reasoning, where the starting point is cases - see e.g. HYPO [0].

Rule-based reasoning can be very powerful, as understanding and navigating legislation can be challenging and time-consuming. One limitation is overcoming a number of ambiguities, including:

- Unclear structure - sometimes, when reading legislation, the logical components of a legal article is not always entirely clear. Language is not like code, and even straightforward articles can have multiple possible interpretations [1].

- Open-textured legal terms - the law often has so-called open-textured terms (e.g. "reasonable"), which require an assessment on a case-by-case basis. Encoding such terms into logical rules is very hard, as they require a nuanced application. In my own work, I try to overcome this limitation by providing examples of how a specific term was applied from previous cases [2].

I am very interested to see how rule-based reasoning will evolve in light of generative AI. As you can imagine, mapping rules to a logical representation can be quite tedious, but LLM seems to be able to at least give a good draft as a starting point [3]. LLMs could also help reason with open-textured terms [4].

[0] Ashley, Kevin D, “Reasoning with cases and hypotheticals in HYPO” Crossref (1991) 34:6 International Journal of Man-Machine Studies 753–796.

[1] Ashley, Kevin D, Artificial Intelligence and Legal Analytics: New Tools for Law Practice in the Digital Age, 1st ed (Cambridge University Press, 2017) p.45.

[2] Westermann, Hannes & Karim Benyekhlef, JusticeBot: A Methodology for Building Augmented Intelligence Tools for Laypeople to Increase Access to Justice (Braga Portugal: ACM, 2023). https://arxiv.org/abs/2308.02032

[3] Janatian, Samyar et al, “From Text to Structure: Using Large Language Models to Support the Development of Legal Expert Systems” arXiv.org (2023), online: <http://arxiv.org/abs/2311.04911>.

[4] Westermann, Hannes, “Dallma: Semi-Structured Legal Reasoning and Drafting with Large Language Models” (2024) 2nd Workshop on Generative AI and Law, colocated with the International Conference on Machine Learning, online: <https://blog.genlaw.org/pdfs/genlaw_icml2024/58.pdf>.

einichi• 1 year ago

the BNA is even more complex today after some additional changes

as a British person living abroad who gave birth to a child abroad, it took me a lot of time and mental energy to determine

- what type of British nationality I am (yes, really)

- how that affects my child as she was born abroad

- how that affects any children she has in the future

varying circumstance around birth of all the people listed above change whether they are British citizens automatically, by application or simply not eligible at all

the legislation feels very messy to me

kelseyfrog3• 1 year ago

Fascinating. Last week, I was vibe-coding a project turning the US Constitution into TLA+, but eventually ran out of context window.

There is a sense - engineer's disease - that laws can made better by formal specification, but I've learned that is naive. However, still I believe that laws can be made less prone to abuse by red-teaming them. Even if the laws aren't formally specified, the systems can be and that is valuable in its own way.

drdaeman4• 1 year ago

I'm curious, why have you concluded that it's naive to build a formal model out of a legal document?

I'm not sure about making laws better, but surely a machine can replace lawyers for trivial and well-defined things (where you don't really need a lawyer - and there are a lot of such cases), saving time for a layman person finding appropriate clauses and navigating them while investigating some well-defined (minimally ambiguous and least likely to raise any exceptions) happy paths. Some companies make a lot of money from formalizing tax codes, after all.

kelseyfrog3• 1 year ago

To be specific I believe it's naive to think that formally specified laws will be an improvement on the legal system.

I believe laws ultimately are subject to Godel's theorem. They can either be complete or consistent, but not both (and likely neither). We should recognize the difference. A complete legal system can render a verdict in every case. A consistent legal system has no contradictions. We prioritize the former.

What would it look like for a case to be presented to a judge and for them to respond, "We simply cannot determine if this is legal or not." What would you even do in such a scenario? Rather, we have judges render decisions and deal with the consequences that they are inconsistent and we have further cases to untangle those inconsistencies, in an ever growing patchwork of legal epicycles.

pessimizer• 1 year ago

There is a sense - engineer's disease - that laws can made better by formal specification, but I've learned that is naive.

We can call it Bentham's disease, and it's what gave everybody civil law outside of the systems descended from the Napoleonic Code (another civil law system.) It's naïve to pretend it's something that can be done in an afternoon, but not to think that it's the ideal we should always be aspiring to.

Henry M. Robert, the creator of Robert's Rules of order, was an engineer, not a lawyer. He took Thomas Jefferson's summary and reorganization of English Parliamentary tradition and precedent, extracted the implicit premises from it, then reconstructed a system for deliberative societies from first principles. We use his system now.

see: https://en.wikipedia.org/wiki/David_Dudley_Field_II

also: "Formalizing Robert's Rules of Order: An Experiment in Automating Mediation of Group Decision Making" https://dl.acm.org/doi/10.5555/869694

brudgers• 1 year ago

A previous submission on the original title, https://news.ycombinator.com/item?id=10518507

wormius2• 1 year ago

This has me wondering about converting law into source code, running it through something like Coq or Agda and finding logical contradictions that need resolution.

Not sure that would be feasible (e.g. if those languages would even be capable of doing such a thing), or how much computing power you'd need to churn through however many thousands of pages of something like the US Code and process that all.

wormius2• 1 year ago

I suppose Prolog would also do very well at this, considering that's the topic of the post, and it's main purpose is logic.

The British Nationality Act as a Prolog Program (1986) [pdf]

Related Stories