Início / coding / Perguntas / 77714086
Accepted
Gordon Sau
Asked: 2023-12-25 23:07:13 +0800 CST

Extensionalidade de função em Dafny

  • 772

Como podemos provar que se para todas as entradas fe gretornar a mesma saída, então as duas funções são equivalentes?

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

Eu diria que isso é um axioma, mas não funciona. A extensionalidade da função não é verdadeira em Dafny?

dafny

1 respostas

  1. Best Answer

    Não acho que o dafny suporte a extensionalidade da função. Não encontrei nada na documentação oficial, mas aqui está um link para comentar que confirma isso https://github.com/dafny-lang/dafny/issues/2308#issuecomment -1169553777

    Não temos extensionalidade funcional na teoria de Dafny. Perguntei a @RustanLeino sobre isso recentemente e ele achou que não seria trivial acrescentar. Parte do problema é que os lambdas podem ler o heap, portanto, a igualdade pontual sem considerar o heap não é suficiente.

    • 1

relate perguntas