Core Abstract Syntax

Overview

Abstract syntax for core L4 concepts.

Files:

• Syntax.hs Declaration of data types (types, classes and instances, modules, expressions, timed automata)
• Exec.hs Execution / evaluation of expresssions
• TaToUppaal.hs Conversion of Timed Automata to the Uppaal XTA format, see https://www.it.uu.se/research/group/darts/uppaal/help.php?file=System_Descriptions/Introduction.shtml
• TransL.hs Translation from L4 BNFC to the core abstract syntax. Very incomplete.
• Typing.hs Type checking of abstract syntax.

The file Test.hs is for testing only and can be discarded.

Versions

0.3.2

with lexicon

Business -> business_2

wordnet annotations in classes

e.g. class Business (132) {

classes

e.g. class Business...

rule expressions

0.3.4

future version! will have support for More Things!

wordnet annotations deleted from classes

class Business {

0.3.6

more typechecking! more expressions!

roundtrip

newSave.l4 goes from IDE to parser & typechecker, which produces an error message, and IDE displays it. (error message in what format: markdown? or old-school fixed-width? decision: plain string.)

s(CASP) English explanations come out of GF

Inari has made a demo! So there is a fragment of s(CASP). Team Bencoolen will continue discussions about how to improve on s(CASP)’s #rped commands.

0.3.8

support for defeasibility

• Notwithstanding
• SubjectTo
• Despite

Let’s start with a simple expression:

34.2 is subject to 34.1.

in the s(CASP) (line 189 of r34.pl) we have an opposes and an overrides statement. TMTOWTDI, of course.

In this style, the override/oppose statement talks about who overrides what, with respect to which conclusion.

Things are more complicatd around line 280: the override is the conclusion of a rule –– it is conditional.

The conclusion being overridden here is the defeasible conclusion of some other rule.

This is our old friend “Subject to 34.1.b, but despite 34.1.a and 34.1.c–f”.

So do we need to name every intermediate conclusion? Lol we need De Bruijn indices for defeasible conclusions

Opposes vs Overrides:

We need an opposes whenever there are two conclusions that can’t defeasibly hold at the same time. (Here, may ≠ must not)

We need an overrides statement whenever the conclusion of one rule defeats the conclusion of another.

Rule 34.1 despite Rule 34.5 override(34.1,34.5)

Rule 34.1 is subject to Rule 34.5 override(34.5,34.1)

Let us agree on the semantics as follows:

Given overrides(defeating_rule, defeating_conclusion, defeated_rule, defeated_conclusion)

means that if defeated_rule applies and it concludes defeated_conclusion, and if defeating_rule applies, then we discard defeated_conclusion and use defeating_conclusion instead.

Of course we also check if the defeating_rule is itself defeated. So we need to order the evaluation. And detect cycles.

Suppose Rule X says:

source legal text

Rule X says: Despite Rule Y, X_inner concludes (May or MustNot)

output

overrides(X_inner,X_conclusion, Y_rule, Y_conclusion)

question: do we deal with Y_rule (outer) or Y_inner?

rule 34.5 says: despite rule 34.1.B hence: overrides(r34_5 ,may(LP,accept,EA) ,r34_1 ,must_not(LP,accept,EA)) :- according_to(r34_1_b ,must_not(LP,accept,EA)).

Martin: all this seems to just be structural organization, why do we need to even have a logic for this stuff – why do we need an “overrides” operator?

Meng thinks: because it’s just syntactic sugar?

Jason: because this is the level of reasoning that the law has; and that the end-user wants to see in explanations, so from the point of view of “argumentation theory” the defeasibility is meaningful to humans.

and because it’s what we’ve implemented in s(CASP), because Jason was writing s(CASP) and wanted a compact representation of some sort; but that’s not the only way to do it.

There could be other ways to do it. We could do the sugar in L4 instead of in s(CASP), and do transformation differently, as long as we ge the same explanations.

Suppose Rule Y says: Subject to Rule X, Y_inner ruleY = overrides(X, Y_inner)

Discussion note: We need an expansion step

34.1.x are “sentence fragments”, but for defeasibility we need to expand the rules to a complete “sentence” which can be used in defeasibility.

Toolchain Versions

l4 version	file	parser status	nlg status	ide status	type checking	reasoner status
0.3.2	mini.l4	ok	ok	syntax highlighting ok
0.3.2	cr.l4	ok	ok
version	language feature	handled by	status	consumed by
0.3.4	class Business { … }	parser	ok
	decl varname : type -> type	parser	ok
	rule <1> for 2: 3,4 if (5) then 6	parser
	forall
	typechecking shows subexpressions	parser - typechecker		ide
	better typechecking errors	parser - typechecker		ide
0.3.6	negation? 2-valued? 3-valued logic? naf?			s(casp)
	states changing over time
	which logic/semantic? process algebra?
	pi calculus! CSP? Petri Nets?
	compositionality
	adding broader ontology support to classes
	functions! macros! metaprogramming!
	module system and importing/exporting

We should have a test suite that creates this dashboard. See issue #4.

Checkin with different departments and backends

To DocAssemble

To s(CASP)

Work started in branch toSCASP

To SMT solvers

Prerequisite and setup

Model checking of L4 assertions can in principle be done with several model checking tools. It should eventually be possible to configure them on the fly, but currently, the Z3 prover is hardwired. Thus, to run the SMT backend, you currently have to install Z3 on your machine.

Some information about Z3 is available here:

• On github.io
• Tutorial description

Z3 is avaible in several package managers.

After installation, the z3 command should be in your path:

> which z3
/usr/bin/z3

Most SMT solvers use the common input format SMT-LIB; the output format is not yet entirely standardized, which makes model interpretation more delicate.

Interfacing is currently done with the SimpleSMT library, which sends commands to the SMT solver and receives acknowledgements and / or results. This communication is currently logged (can easily be switched off).

When invoking an SMT solver on an L4 file, the first assert statement in the file is currently checked for satisfiability. The result is either

• unsat: formula unsatisfiable
• sat: formula satifiable. In this case, the model is displayed (currently rather unreadable)

To prove the validity of a formula, check its negation for satisfiability. If the result of checking the negation is unsat, then the original formula is valid.

Example of invoking the SMT checker:

stack exec -- l4 smt l4/speedlimit_flat_consistent.l4

To GF via PGF

on track

To Other Backends

Uppaal

Interactive use with the GUI

Start Uppaal with java -jar uppaal.jar &, then File / Open system. Load a model (*xml) file. The view typically opens on the Editor tab (system definition with several automata). On the Simulator tab, one can execute the system by stepping through a scenario. On the Verifier tab, one finds several “queries” (corresponding to proof obligations). These are contained in the *q file associated with the model file. Select one of the formulas and verify it by clicking on the Check button. In order to obtain a counter-example, select “Options / Diagnostic Trace” and then one of Some / Shortest / Fastest. On the next Check, the counterexample will be loaded into the Simulator.

Command line interface

In Haskell, running writeFile "test_haskell_uppaal.xta" (ta_sys_to_uppaal (TASys [autA, autB])) produces a textual Uppaal XTA file. The file can in principle be read in by the GUI. As there is no graphical layout information information associated with the file, the elements of the automata are first arranged in an arbitrary fashion. After manually rearranging and storing the model, a .ugi file stores graphic information.

The XTA file can be run (together with a query in a .q file) with shell command verifyta contained in the download bundle, as in bin-Linux/verifyta -t0 test_haskell_uppaal.xta test_haskell_uppaal.q, where test_haskell_uppaal.q is, for example:

E<> AutA.l3 and AutB.l2

A textual trace is then written to standard output.

Installation and Prerequisites

The goal is for this to work:

stack run l4 gf en l4/mini.l4

and you should (eventually) get this output:

if there is no business bsn such that the business is associated with the appointment , then the lawyer doesn't accept the appointment

if a business is illegal , then the lawyer doesn't accept the appointment

So try running the command above; it does a stack build along the way, and you can expect the first run to take a little while.

If you get an error involving Syntax.gf, then you need to get your RGL and WordNet installed correctly. To get RGL installed, you need gf.

Where is gf? From inside the baby-l4 directory (which is where you should already be, if you are reading this):

Inside baby-l4, first run

stack build --dependencies-only

to install all the dependencies, including gf, but not including RGL (more on that later)

Then run

stack exec which gf

You should see something like:

/Users/mengwong/.stack/snapshots/x86_64-osx/0d89070f643fd180a58cfc42b9ba6fbece00cfd59cde65a81136970789de7eb9/8.8.4/bin/gf

Why? Baby-l4’s stack build installs a working gf as a dependency, so we will use that instead of installing gf-core from source.

Because it’s huge, save it to a variable in the shell:

mygf=`stack exec which gf`

Set up GF_LIB_PATH

In your ~/.zshenv or in your ~/.profile, depending on whether you belong to the zsh or bash persuasion, create a line

export GF_LIB_PATH=$HOME/gf_lib_path

For that environment variable to take effect, you can restart your shell or just paste it at your shell prompt. Now when you run:

echo $GF_LIB_PATH

You should see:

/Users/<you>/gf_lib_path

This is where gf will install the RGL, and where baby-l4’s codebase will look for it.

You need to create it.

mkdir $GF_LIB_PATH

TODO: raise a PR against gf-rgl to mkdir -p $GF_LIB_PATH if it doesn’t already exist. Note that this mkdir PR will be complicated by the fact that a GF_LIB_PATH may be a colon-separated list.

Now we are ready to install to it.

Clone gf-rgl

Download gf-rgl from Github:

mkdir ~/src
cd ~/src
git clone https://github.com/GrammaticalFramework/gf-rgl
cd gf-rgl

You should now be in a directory called ~/src/gf-rgl

In the gf-rgl directory, run:

runghc Setup.hs install --gf=$mygf

You should see:

Building [prelude]
Building [present]
Building [alltenses]
Copying to /Users/mengwong/gf_lib_path

Now install gf-wordnet

First, clone gf-wordnet:

cd ~/src
git clone https://github.com/GrammaticalFramework/gf-wordnet
cd gf-wordnet

Then run mygf on some of the WordNet*.gf files; this command will install the compiled gfo files to GF_LIB_PATH.

$mygf --gfo-dir=$GF_LIB_PATH WordNetEng.gf WordNetSwe.gf

Did it work?

stack run l4 gf en l4/mini.l4

should produce a whole bunch of errors you can ignore:

Warning: Unable to find a known candidate for the Cabal entry Prop, but did find:
         * PropEng.gf
         * PropI.gf
         * PropLexiconEng.gf
         * PropLexicon.gf
         * PropTopEng.gf
         * Prop.gf
         * PropTopSwe.gf
         * PropSwe.gf
         * PropTop.gf
         * PropLexiconSwe.gf If you are using a custom preprocessor for this module with its own file extension, consider adding the file(s)
         to your .cabal under extra-source-files.
baby-l4-0.1.0.0: unregistering (local file changes: README.org)
baby-l4> configure (lib + exe)
Configuring baby-l4-0.1.0.0...
baby-l4> build (lib + exe)
Preprocessing library for baby-l4-0.1.0.0..
Building library for baby-l4-0.1.0.0..
Preprocessing executable 'l4' for baby-l4-0.1.0.0..
Building executable 'l4' for baby-l4-0.1.0.0..

Warning: Unable to find a known candidate for the Cabal entry Prop, but did find:
         * PropEng.gf
         * PropI.gf
         * PropLexiconEng.gf
         * PropLexicon.gf
         * PropTopEng.gf
         * Prop.gf
         * PropTopSwe.gf
         * PropSwe.gf
         * PropTop.gf
         * PropLexiconSwe.gf If you are using a custom preprocessor for this module with its own file extension, consider adding the file(s)
         to your .cabal under extra-source-files.
baby-l4> copy/register
Installing library in /Users/mengwong/src/smucclaw/baby-l4/.stack-work/install/x86_64-osx/0d89070f643fd180a58cfc42b9ba6fbece00cfd59cde65a81136970789de7eb9/8.8.4/lib/x86_64-osx-ghc-8.8.4/baby-l4-0.1.0.0-2uuTWxtfYE14aM49x0XA7O
Installing executable lsp-server-bl4 in /Users/mengwong/src/smucclaw/baby-l4/.stack-work/install/x86_64-osx/0d89070f643fd180a58cfc42b9ba6fbece00cfd59cde65a81136970789de7eb9/8.8.4/bin
Installing executable l4 in /Users/mengwong/src/smucclaw/baby-l4/.stack-work/install/x86_64-osx/0d89070f643fd180a58cfc42b9ba6fbece00cfd59cde65a81136970789de7eb9/8.8.4/bin
Registering library for baby-l4-0.1.0.0..

… and eventually produce the desired output:

if there is no business bsn such that the business is associated with the appointment , then the lawyer doesn't accept the appointment

if a business is illegal , then the lawyer doesn't accept the appointment

Help

If this install procedure did not go as planned, ask for help on Slack.

FAQ

My gf-rgl and gf-wordnet paths are different. Could i get away with just appending both to GF_LIB_PATH?

Yes, use colons to separate, as is the convention with $PATH variables.

[PASSIVE-AGGRESSIVE] I want to do all this with Nix

Yes! You can do that!

All you need to do is run nix-shell in the baby-l4 directory or direnv enable if you have direnv installed. This will automatically install gf-rgl and gf-wordnet set the $GF_LIB_PATH variable to point to them.

If you want to use this installation more than once, you can run

echo "export GF_LIB_PATH=$GF_LIB_PATH" >> ~/.zshenv
echo "export GF_LIB_PATH=$GF_LIB_PATH" >> ~/.profile

to export the generated lib-path to your shell profile.

[PASSIVE-AGGRESSIVE] Shouldn’t the above instructions be reducible to a very small shell script?

Yes, patches welcome!

testing.