主页 / coding / 问题 / 77714086
Accepted
Gordon Sau
Asked: 2023-12-25 23:07:13 +0800 CST

Dafny 中的函数外延性

  • 772

我们如何证明如果对于所有输入，f并且g返回相同的输出，那么这两个函数是等价的？

lemma func_ext(f: int -> int, g: int -> int)
requires forall x :: f(x) == g(x)
ensures f == g

我认为这是一个公理，但它不起作用。Dafny 中的函数外延性不成立吗？

dafny

1 个回答

  1. Best Answer

    我认为 dafny 不支持函数外延性。我在官方文档中没有找到任何内容，但这里有评论链接，证实了这一点https://github.com/dafny-lang/dafny/issues/2308#issuecomment-1169553777

    达夫尼的理论中不存在功能外延。我最近向 @RustanLeino 询问了此事，他认为添加这一点并不简单。部分问题在于 lambda 可以读取堆，因此不考虑堆的逐点相等是不够的。

    • 1

相关问题