Problems & solutions:

Abstraction passing in the presence of mutually recursive predicatess

The problem: Termination

Consider

predicate A(loc x, pred p)
{
| ... => { p(x) ** B(x, p) ** ... }
}

predicate B(loc y, pred q)
{
| ... => { q(y) ** A(y, q) ** ... }
}

{ A(z, pred(w) => [w, 2] }
void free_A(loc z)
{ emp }

The naïve approach to defunctionalizing the application of A in the precondition of free_A leads to an infinite loop with these steps:

• A new predicate definition predicate A$0(loc x) { ... } needs to be generated as a specialization of A to the predicate abstraction in free_As post-condition
• In order to create this, we must also specialize B to the predicate p (which, in this case, is the same abstraction from free_As post-condition)
• To do this, we must generate predicate B$0(loc y) { ... }
• However, in order to generate this, we must again specialize A. To do this we must generate a new predicate definition predicate A$1(loc x) { ... }. This leads us back to the start, resulting an infinite loop.

Recursion can also be considered a special case of mutual recursion here.

A possible solution

Keep track of which pred abstraction instantiations we have already generated. This could be done using a list of triples with the format (origin, original_call, generated_name), where the generated_name is the name of the predicate generated for original_call. Consider the previous example. Here's a table of steps annotated with the list of triples (which starts out empty):

Step #	Action	List of triples
1	Begin generating predicate A$0(loc x) { ... }	[("A", "B(x, p)", "B$0")]
2	Begin generating predicate B$0(loc x) { ... }	[("A", "B(x, p)", "B$0"), ("B", "A(y, p)", "A$1")]
3	Begin generating predicate A$1(loc x) { ... }	[("A", "B(x, p)", "B$0"), ("B", "A(y, p)", "A$1")]
4	In A$1, use B$0(x) instead of B(x, p)	[("A", "B(x, p)", "B$0"), ("B", "A(y, p)", "A$1")]
5	Halt	[("A", "B(x, p)", "B$0"), ("B", "A(y, p)", "A$1")]

The final result being

predicate A(loc x, pred p)
{
| ... => { p(x) ** B(x, p) ** ... }
}

predicate B(loc y, pred q)
{
| ... => { q(y) ** A(y, q) ** ... }
}

predicate A$0(loc x) {
| ... => { [x, 2] ** B$0(x) ** ... }
}

predicate B$0(loc y) {
| ... => { [y, 2] ** A$1(y) ** ... }
}

predicate A$1(loc x) {
| ... => { [x, 2] ** B$0(x) ** ... }
}

While this does some extra work (A$0 could be used instead of generating A$1), it does not require comparison of expressions modulo α-equivalence. An implementation which generates less code by using comparison modulo α-equivalence could be implemented in the future.

A ("abstraction non-regular") recursive example with one predicate

predicate C(loc x, pred p) {
| ... => { p(x) ** C(x, pred(y) => y :-> 0 ** p(y)) }
}

{ C(z, pred(w) => [w, 2] }
void free_C(loc z)
{ emp }

Gives:

Step #	Action	List of triples
1	Begin generating C$0	[("C", "C(x, pred(y) => y :-> 0 ** p(y))", "C$1")]
2	Begin generating C$1	[("C", "C(x, pred(y) => y :-> 0 ** p(y))", "C$1")]
3	In C$1, use C$1 instead of C(x, pred(y) => y :-> 0 ** p(y))	[("C", "C(x, pred(y) => y :-> 0 ** p(y))", "C$1")]
4	Halt	[("C", "C(x, pred(y) => y :-> 0 ** p(y))", "C$1")]

Generating:

predicate C$0(loc x) {
| ... => { [w, 2] ** C$1(x) ** ... }
}

predicate C$1(loc x) {
| ... => { x :-> 0 ** [w, 2] ** C$1(x) ** ... }
}

Note that the "duplicated" heaplet x :-> 0 only shows up once.