recursion - Alloy での再帰関数のプログラミング

Question

Alloy で再帰関数を構築しようとしています。Daniel Jackson の本に示されている文法によれば、これは可能です。私の機能は次のとおりです。

fun auxiliaryToAvoidCyclicRecursion[idTarget:MethodId, m:Method]: Method{
    (m.b.id = idTarget) => {
        m
    } else (m.b.id != idTarget) => {
        (m.b = LiteralValue) => {
           m 
        } else {
           some mRet:Method, c:Class | mRet in c.methods && m.b.id = mRet.id => auxiliaryToAvoidCyclicRecursion[idTarget, mRet]
        }       
    }
}

しかし、ソルバーは呼び出しについて次のように主張してauxiliaryToAvoidCyclicRecursion[idTarget, mRet]います。

"This must be a formula expression.
Instead, it has the following possible type(s):
{this/Method}"