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!