1樓：
可以有一種叫 Theorm Prover 的程式做驗證，但要滿足幾個條件。簡要概括就是。
被比對的函式是 pure functional 且 total functional，如果 rec 還要保證 terminate，且只由滿足以上條件的函式定義。
有提供足夠的 lemma。
條件滿足就可以用 induction 來證明。
接下來用是 ACL2 做證明，用的是 Common Lisp 的子集。
(defun
rec(x)
(if(endpx)
1(+1
(rec
(cdr
x)))))
#|The admission of REC is trivial, using the relation O< (which is known
to be well-founded on the domain recognized by O-P) and the measure
(ACL2-COUNT X). We observe that the type of REC is described by the
theorem (AND (INTEGERP (REC X)) (< 0 (REC X))). We used primitive
type reasoning.
|#主要就是驗證是否滿足 (1)。像乙個不 terminate 的函式就不讓過了。
(defunf(
x)(consx(
fx)))然後用 rec 寫定義
(defun
fun1(a
b)(+
(reca)
(rec
b))))
(defun
fun2(a
b)(+
1(rec(ab
))))
可驗證(
defthm
prove
(equal(zz
ab)(
fun2ab
)))#|
Perhaps we can prove *1 by induction. Three induction schemes are
suggested by this conjecture. Subsumption reduces that number to two.
However, one of these is flawed and so we are left with one viable
candidate.
REC. If we let (:P A B) denote *1 above then the induction scheme
we'll use is
(AND (IMPLIES (AND (NOT (ENDP A)) (:P (CDR A) B))
P A B))
(IMPLIES (ENDP A) (:P A B))).
two nontautological subgoals.
Subgoal *1/2
Subgoal *1/2'
Subgoal *1/1
Subgoal *1/1'
*1 is COMPLETED!
Thus key checkpoint Goal' is COMPLETED!
Q.E.D.
|#然而 Theorem prover 是個相當複雜的系統，且是用來主動做證明而不是被動驗證的玩意，要靠人來提供相當多的 lemma 才能做 non trivial 證明，當然，比只靠人力證明強多了。
REF
Matt Kaufmann1 and J Strother Moore2, How to Prove Theorems Formally.
ACL2 Users Manual
2樓：櫻七子
一一對映
來來來把實數域複數域先窮舉一遍。
如果函式也能處處一致收斂那麼兩函式相等。
這時候有人要打我了，窮舉你怎麼不去上天呢。
佔坑，等我把程式編出來打臉。
3樓：rainoftime
程式等價性不可判定。另外「等價」也有不同定義，語法/語義等價，內涵/外延等價等等。。
但是有很多情況還是可以的，比如某種lambda演算的contextual equivalence什麼的。。
舉個用SMT solver + 命令式語言的例子。。 判斷以下2個函式的等價性（ 函式的「」in-out關係「」等價）
intpower3
(intin)
intpower3_new
(intin)
可以簡單地做迴圈展開，然後用邏輯公式來encode程式語義（需要引入中間變數）。以上兩個程式分別編碼為
1. 邏輯需要建模Fixed-width integer和*，正巧 QF_BV(quantifie-free bitvector theory)剛好適合（複雜度NEXP-complete）。等價性就轉化為判斷以下公式的Validity（可以轉化為Satisfiability）
2. 比較取巧的，對於這個例子，其實可以用QF_EUF(theory of equality with uninterpreted function) (複雜度NP-complete)：把*換成uninterpreted function ，得到
對應地，得到
4樓：李遙
除了停機問題，還可以這麼想：大部分數學定理都可以表達成乙個帶有變數的等式，那麼把等式兩邊拆成兩個函式，假如真有乙個程式能機械判斷兩個函式是否等價，那麼還要數學家去挖空心思找證明幹什麼？
數學基本法則之一就是正面對抗無窮（證明無窮集上的元素都有或沒有某個屬性）往往是徒勞的，必須啟發式地迂迴作戰（用人類智慧型來證明定理）
5樓：碼農醬
符號執行也許可以幫忙，傳送門：s2e/EquivalenceTesting.rst at master · dslab-epfl/s2e · GitHub
6樓：舒自均
你這問題一看就是不可能的,點開看果然有人把它規約到停機問題了.
不過你的追問的這種相等判定是可以做到的,只要取取樣點就可以了.例如如果答案是乙個多項式,你取超過這個多項式的次數個的取樣,只要在取樣點全相等,那兩個多項式就會相等了.當然這樣的話會誤判一些錯誤答案,但是能輸入這些錯誤答案的人必然也是已經算出正確答案是啥了.
7樓：劉然
關於函式判等不可計算這件事，其他答主已經講的很清楚了，下面回答一下追問的問題:為什麼存在一些程式可以判斷表示式相等？
其實不能再簡單了:
在允許一些誤差的情況下，這些系統一般是通過test case來進行大概的判斷:即在式子中帶入一些預先構造的或者是隨機生成的測試輸入，判斷結果是否相等即可。
不信你可以構造乙個明顯會導致運算溢位但是最終結果正確的算式試一下。
8樓：孫文全
其實其它答主忽略了一點：雖然針對圖靈機的函式判等是不可行的，但是由於現實中的計算機並不能真正handle無窮——也就是真實計算機的狀態數是有限的，所以對於某一函式，合法的輸入是可列舉的，所以判斷函式等價事實上在邏輯的層面是可行的——雖然可計算性會分分鐘糊你一臉
-_-誰知道手機搜狗怎麼打分割線-_-
昨天我忘記加對問題的限定了，我把問題私自篡改為在某台具體的電腦上兩個函式表現為等價能不能被判定——不過問題裡可沒有限定在那台計算機上跑這個判定程式——所以你大可以理解為上帝造了一台速度和記憶體都無窮大的玩意來，反正你要是用數學證明也可以看做是寫了個抽象解釋程式跑在腦袋裡是不……
9樓：
這是不可能的。在函式式程式設計中，函式是一等公民，但是從來沒有見過支援他們比較的算符。如果可以的話，語言設計者一定會加入這麼乙個操作的。
10樓：金岳霖
編寫出乙個程式判斷連個函式是否相等是不可能的，因為這是乙個不可判定問題。
我假設你已經知道了停機定理：
代表乙個圖靈機（程式），是它演算法的編碼。表示在輸入時會停機並輸出。則不存在圖靈機，使得如果停機；如果不停機。
簡單地給乙個證明：我們用反證法，先假設這樣的演算法存在：
如果 ；
如果 。
我們再構造乙個判斷停機問題的演算法。給定了乙個，先建構函式，是乙個在任意輸入下都只輸出0的函式。
然後根據構造：
如果在圖靈機執行的步以內沒有停機；
如果在圖靈機執行的步以內已經停機。
此時我們有：
當且僅當當且僅當不停機當且僅當；
當且僅當當且僅當會停機當且僅當。證畢。
用python寫乙個函式，可以判斷兩個陣列是否環型相等。跪拜大佬幫忙解答一下？
薛衣人 defequal arr1 arr2 if arr1 isNone or arr2 isNone return False count1 arr1 count x forxin sorted set arr1 count2 arr2 count x forxin sorted set arr...
同乙個函式影象可以表述為兩個不同函式嗎？
鐵向榮 可以。舉例 和 用對映的原理分析。設原對映為 把它作為你所說的原函式影象。令新對映為 和 那麼原對映 就可以看作是 與 的合成。也就是新函式影象。可見，是重合的。請模擬向量運算的平行四邊形法則，不看過程，只看結果 歡歡 可以，比如 y sin x 2 n n Z，y cos 2x n n Z...
如何理解這兩個函式的區別（Haskell）？
其實沒區別，區別是編譯器造成的，有個叫CAF 的東西，必應谷歌或者Haskell Wiki 中搜尋 Haskell CAF,第二個中的 x 破壞了這個，編譯器，在 O0 下會自動優化 當然，在不要這個 優化的方式就是備忘錄法，memorization,對於第乙個，當你計算第n個數的時候，時間複雜度是...