luomein's questions

在《Software Abstractions》一书中，第 5.2.2 Skolemization 章提到，

其中sx是新的自由变量F[sx/x]是约束F，用sx代替x。

但是，当我在 Alloy 中提供自由变量时，它显示语法错误。Alloy 接受自由变量吗？

sig A {
  relation:  A
}
fact {
 some A
}
check{
  //correct expression
  //some a : A | one a.relation

  //Skolemization
  (a: A) and (one a.relation)
}