maude-system - Maude-system 一个操作可以有两个以上的操作数吗？

Question

我知道在 maude 中，您可以通过以下方式之一定义操作：

op operation_: Nat -> Bool . // for 1 operands
op _operation_: Nat Nat -> Bool . // for 2 operands

但是有没有办法定义操作，使其有更多的操作数？

Answer 1

我想三元条件运算符（来自 Basic Maude）应该是一个很好的例子：“函数名称中存在下划线意味着我们正在使用 mixfix。这个想法是函数的每个参数都将替换一个下划线。例如，考虑

op if_then_else_fi : Bool Nat Nat -> Nat .

然后我们可以像这样应用这个运算符：

if B then X else Y fi

其中 B 是布尔值，X 和 Y 是 Nats。”

手册中没有提到对运算符数量的限制（阅读 pp.33-35 以包含运算符声明的全部功能），所以

op _ _operation_ _ _: Nat Nat Nat Nat Nat -> Bool . // for 5 operands

也应该没问题。我想在某些时候你应该达到特定于实现、平台或内存的限制。