Backward slicing

[rolyp]

Implement the bwd slicing rules from the paper draft. (I’ve parked the “projectional” idea for now and gone back to a very simple system that just tracks data dependencies – let’s implement this and then revisit projection.) We’ll also need to implement the join operation to merge environments.

Failing test cases:

• arithmetic.fld: BinaryApp case needs to push binding of operator name back into environment
• compose.fld
  • bwd rule for Let should use None rather than e2 as the continuation
  • (+1) 1 has become 1 (+)
• express evalArgs_bwd in terms of zip and fold
• AppOp and BinaryApp cases should demand arguments according to demand on result

[rolyp]

@min-nguyen Let’s meet at our usual time on Friday, but feel to ping me in the meantime. On Friday we can look at some of the examples I’ve sketched out to try to understand what we want from projection (= extracting subcomputations).

[rolyp]

@min-nguyen Added eliminator join rules (which are probably what you expected).

[rolyp]

@min-nguyen The approach I’ve settled on is based on “annotations”: one bit per term constructor to identify whether that node is “selected” or not. Going forward, “selected” means “available”. Going backward, “selected” means “needed”.

From the projectional experiment, I’ve retained the idea that the slicing relations take an additional α which tracks whether input resources (parts of values that get consumed by pattern-matching) are available (going forward) or needed (going backwards). The projectional idea itself is trickier than I thought and something we will probably have to come back to in another paper.

To implement backward slicing as specified, you’ll need to make some minor changes to the representation of traces, so that you can implement the var, op, nil and int cases. These rules need the know the ρ that the original expression was evaluated in. In the formal setting (which you can basically read in a dependently typed way), a trace T is a term (in the metalanguage) of type ρ, e \eval v. In other words, \eval is an inductively defined relation and ρ, e and v are “indices” that are all mentioned in the type of the relation. For example in Agda one could obtain these by simply extract the relevant part of the type of T.

In a simply-typed setting such as PureScript or Haskell 98, we need to make explicit in the value some of that information that would otherwise be carried by the type. That means the var, op, nil and int constructors all need to have an explicit ρ argument.

A similar consideration applies to the apply-prim and binary-apply rules, which need to access the value of the original computation (the v that occurs in the type of T). Again, in a simply-typed setting this means enriching the respective trace constructors with values. For example, the apply-prim trace form T U needs to record the value associated with T and the value associated with U.

Ping me if this doesn’t make much sense!

[rolyp]

@min-nguyen

[rolyp]

@min-nguyen Here are some notes/comments on your latest commit. Overall looks good. I realise this is WIP, so some of these may already be in hand:

• in various places, Bind v x should be Bind x v; we should probably standardise on x ↦ v especially if it makes the meaning clearer
• by the same token, let’s standardise on ε rather than a mixture of Empty and ε
• I would suggest giving a Foldable instance for Bindings, rather than a bespoke foldl with a different signature. We could then (for example) implement reverse in terms of foldl
• the second clause of update looks strange :)
• we shouldn’t need reverse to implement filter
• let’s standardise on tab sizes – we seem to be using a mixture of 1, 2, 3 and 4 character tabs
• the definition of any looks a bit weird – I can guess the intended behaviour from its use in intersect, but then I would expect it to be recursive (and is it elem you want?)
• I would probably fix the notion of equality for nubBy, etc – i.e. just define nub and lose the eq' parameter, given that these definitions are already not completely straightforward
• for the sake of diff, let’s standardise on ending every file with a single line terminator, and stripping trailing whitespace from each line (there’s a setting in VS Code)
• let’s use κ (rather than k) to range over instances of k; there are also a few cases where you’re using el instead of σ
• we could simplify the Lattice instance for Expr a little by factoring it through an instance for RawExpr
• top and bot need to be recursive (and so would also benefit from the RawExpr instance)
• we haven’t got sections in PureScript, but \k' -> k ∨? k' can be written (∨?) k
• in the List cases of maybeJoin and maybeMeet, is there a reason you can’t just do σ1 ∨? σ2 where you have maybeσ? (It looks like you’ve just inlined some of the recursive call..)
• we can probably put Elim in a separate module now – that caused a cyclic dependency when patterns weren’t nested, because Elim depended on Expr, but now it should be possible.

Let’s chat tomorrow if any of these would benefit from some discussion.

[rolyp]

I’ve finished migrating the old code to arbitrary data types, so the parameterised version of Elim has been replaced by the more dynamic version (called Elim2 in the WIP). I’ve migrated the pattern-matching logic to the new design, including the backward-slicing bits. Here’s some more feedback on the current implementation of backward slicing:

• In the variable case of unmatch, the input environment ρ always has the required binding at the head – so you don’t need remove, but should instead assume that ρ is of the form ρ' :+: x ↦ v, where x is the variable you’re looking for.
• Similarly, with filterRecDefs, the input ρ will have, at its head, a number of bindings (necessarily of closures) equal to the length of δ, so all you need to do is pop that many off.
• Let’s adopt a convention where we list imports in the order [Prelude; other PureScript standard libraries; our modules], and then alphabetically within each of those (I’ve added this suggestion to src/README.md).
• In the formalism we use T, U to range over traces, v to range over values and u to range over “raw” values, but this doesn’t work too well in code where the variables are lowercase – suggest we keep u for raw values, and use t, t’’ etc for traces.
• The relation which is written \rightharpoonup (that takes a list of recursive definitions and turns it into an environment of closures) is called closeDefs in Eval.ts, and closeDefs_fwd in Fwd.ts. The backward-slicing counterpart of closeDefs_fwd (which I think is joinClosures) should be called closeDefs_bwd.
• closeDefs_bwd can’t impose the requirement that the input environment ρ is non-empty, since (for example) lambdas introduce closures with an empty δ and therefore for which closeDefs produces an empty environment. Moreover it can assume that ρ consists entirely of closures, since that’s the output of closeDefs.
• Let’s always write join as ∨ rather than than join (apart from in its definition).
• In fact, the pure functional implementation of closeDefs_bwd is tricky and will require some thought. (I apologise again that the specification is not at all clear.) Let F be the set of function names being mutually recursively bound. For each f in F, the input environment to closeDefs_bwd associates a closure - that’s what the left-hand side of the definition is asserting. (It’s an “environment comprehension”, if you like.) There are then three outputs of closeDefs_bwd: an environment, a list of recursive definitions and a “selected” flag. Let’s deal with those separately:
  • Each of those closures has its own copy ρ_f of the environment originally active when the closures were created. Those have to be joined to produce the environment returned by closeDefs_bwd – that’s what \bigvee ρ means on the right: take the join of all ρ_f for every f in F.
  • Each closure also has two other bits of information: a copy δ_f of the original recursive definitions, which will have been annotated with their usage in any recursive calls, and the function itself λσ_f, which will be annotated with the usage of the function at this call. The list of recursive definitions produced by closeDefs_bwd is the join of the δ_f’s (written \bigvee δ), also joined with the another set of recursive definitions (with the same shape as each of the δ_f’s) formed from the λσ_f’s.
  • Finally the output selected flag is simply the join of the α_f’s associated with each closure, written \bigvee α.

The recursive stuff isn’t easy to grok and I wouldn’t worry if it’s hard to intuit what’s going on initially. Ironically (perhaps) it’s a case where the imperative implementation is almost trivial by comparison, so I guess the difficulty will come trying to prove that the two are equivalent.

Luckily, join imposes a hard constraint on the things being joined (namely that they are the same thing modulo annotations) so you’ll discover quickly enough if you’re trying to merge two environments, or two lists of recusive definitions, that aren’t compatible in this sense.

[rolyp]

@min-nguyen Thanks for the latest commit - looking pretty close now. Some additional comments:

• I like the use of × for the Tuple constructor. The nice thing about this is we should be able to use the same notation for T3 (following Data.Tuple.Nested).
• It would be reasonable to use mustEq (≜) in filterRecDefs (and maybe we could give it a more suggestive name like split, but that’s only a suggestion). The last case could be simplified to go acc Empty _ = error absurd.
• Let’s use ε uniformly for Empty environments. And we should also reserve x (xs) to range over variables (lists of variables), except in generic functions it seems reasonable to use x to refer to an argument of polymorphic type.
• When there are a lot of variables in scope, I find it improves readability to avoid naming unused variables (i.e. use _ where you can).
• If a definition relies heavily on non-trivial local functions, we should probably give those type signatures as well.

I’ve pushed a minor commit that applies some of the above suggestions.

I didn’t manage to convince myself that we have is correct yet – in particular it looks like joinRecDefs will not only merge the δ_f’s and ρ_f’s from the various functions (which makes sense – each function starts with an identical copy of δ and ρ, and when backward slicing, these differ only in their annotations, so their joins are defined), but will also merge their σ_f’s. This isn’t well defined, as each function has its own body, so they can’t be joined. These only need to be accumulated into the additional RecDefs which is eventually merged with \bigvee δ. So I suspect the type of joinRecDefs needs to change to replace Val (assumed to be a closure) by Env × RecDefs × Selected.

It might also be able to factor joinRecDefs into two functions, one which is just a regular fold over Env which does the merge of the ρ_f’s and δ_f’s (and which doesn’t need to use the variable name f), and one which just extracts the RecDefs. For the former, we could then just provide a Foldable instance for Bindings.

In terms of how to proceed after that, my suggestion would be to look at runExample in Test.Main.purs and integrate backward slicing into that, so that every test case is backward-sliced as well as forward-sliced. That should tease out any obvious problems with closeDefs_bwd, as any undefined joins will fail.

[rolyp]

@min-nguyen Just some tidying up to do and then we can close this task:

• fix broken build
• delete Pretty2
• delete other version of mustEq
• delete runExample and rename RunExampleBwd to runExample
• reinstate environment lookup instead of find op primitives in Eval.purs
• add Str case to eval_bwd (similar to Int case)
• reinstate previous compilation scripts in package.json
• delete eitherToBool (use isRight from Data.Either instead)
• factor append, concat, map, concatMap from Primitive.purs through an embedding of List Expr into Expr

[rolyp]

@min-nguyen Implemented #376, which solves the performance issue to the point where backward slicing can work. Did some other tidying up/bug-fixes; can’t do any thorough testing of backward slicing until #382, but at least we are now exercising eval_bwd on every test.