Transformation from one recursive signature to another

Questions
1

I’m trying to model compilation from a source language to a low-level runtime language. In a nutshell, a source expression compiles to one or more binary instructions. In my current model, these are both recursive signatures for simplicity.

But I’m having trouble defining compilation of expression. When I add a rule for how to compile an expression whose signature has a nested expression inside of it, which must also be compiled, I run into skolemization errors.

I am not sure what to do and would appreciate some advice.

Here’s a mocked up model that demonstrates the basic problem with only a single type of statement at each level (in/out).

module Test

sig RecursiveIn {
	ptr: lone RecursiveIn
}

sig RecursiveOut {
	ptr: lone RecursiveOut
}

pred convert_rec (i: RecursiveIn, o: seq RecursiveOut) {
	// Next line: Analysis cannot be performed since it requires higher-order
	// quantification that could not be skolemized.
	some co: seq RecursiveOut | (no i.ptr => #co = 0 else convert_rec[i.ptr, co]) and
	some ro: RecursiveOut |
	ro.ptr = co.last and
	o = co.add[ro]
}

pred example {
	some i : RecursiveIn |
	some o : seq RecursiveOut |
	convert_rec[i, o] and #o >= 1
}
run example for 1

It may be related that I am modeling compilation as a predicate and not a function. This seems awkward to me because there is a lot of existential quantification. But I can’t figure out how to phrase it in a direct forward manner.

Also, does anyone know if Alloy* still maintained? I can’t access the website.

Thanks!

2

Hi,
I’m not sure to see exactly what you want to specify in the end, but here the problem comes from higher-order quantification rather than recursion: in general, when you need to talk about collections (subsets, lists…) of items, one approach is to reify them as a new signature, e.g. sig RecursiveOutSeq { ros: seq RecursiveOut }. The tedious and tricky part, apart from adapting your code to this new signature, is that you need to handle how this signature will be populated (e.g. what scope you will need on the new signature) and what its properties are. This is broached in the Alloy book in §§ 5.3.1 and 5.4.2.

Then, recursion will probably be a problem too. I suggest you to refer this thread and its answer by Aleks.

Hope this helps.

1 Like
3

Sorry for the very long delay in responding. My email must not have been set up right to receive notifications.

Anyway, I think reification is the insight I was missing. I was able to fix my example as you suggested:

module Test

sig RecursiveIn {
	ptr: lone RecursiveIn
}

sig RecursiveOut {
	ptr: lone RecursiveOut
}

sig RecursiveOutSeq {
	ros: seq RecursiveOut
}

pred convert_rec (i: RecursiveIn, o: RecursiveOutSeq) {
	some co: RecursiveOutSeq | (no i.ptr => #co.ros = 0 else convert_rec[i.ptr, co]) and
	some ro: RecursiveOut |
	ro.ptr = co.ros.last and
	o.ros = co.ros.add[ro]
}

pred example {
	some i : RecursiveIn |
	some o : RecursiveOutSeq |
	convert_rec[i, o] and #o.ros >= 2
}
run example for 3

Thank you for the help!