它们似乎具有类似的目的。到目前为止我注意到的唯一区别是,虽然 Program Fixpoint
可以接受类似于 {measure (length l1 + length l2) }
的组合度量,但是 Function
会拒绝这样做,只允许 {measure length l1}
。
Program Fixpoint
是否比 Function
更强大,还是它们更适用于不同的用例?
它们似乎具有类似的目的。到目前为止我注意到的唯一区别是,虽然 Program Fixpoint
可以接受类似于 {measure (length l1 + length l2) }
的组合度量,但是 Function
会拒绝这样做,只允许 {measure length l1}
。
Program Fixpoint
是否比 Function
更强大,还是它们更适用于不同的用例?
这可能不是一个完整的列表,但这是我目前找到的:
Program Fixpoint
允许度量衡查看多个参数。Function
创建一个 foo_equation
引理,可以用来重写对 foo
的调用与其 RHS。非常有用,避免像Coq simpl for Program Fixpoint这样的问题。Function
可以定义一个 foo_ind
引理,以沿着递归调用 foo
的结构进行归纳。再次,非常有用,可以证明关于 foo
的事情,而不实际重复证明中的终止参数。Program Fixpoint
可以被欺骗支持嵌套递归,请参见https://dev59.com/Dqbja4cB1Zd3GeqPbBlN#46859452。这也是为什么当Function
不能时,Program Fixpoint
可以定义Ackermann函数的原因。