proof-of-correctness

12熱度

3回答

爲了找到樹的直徑，我可以從樹中取任何節點，執行BFS以找到距離它最遠的節點，然後執行BFS在該節點上。距第二個BFS最遠的距離將產生直徑。雖然我不確定如何證明這一點？我曾嘗試在節點數量上使用歸納，但情況太多。任何想法，將不勝感激......

0熱度

1回答

如何證明此算法的正確性？

我正在從codeforces解決問題。我們的工作是找到使給定整數序列成爲非遞減序列的最小成本。我們可以在每一步增加/減少任意數量的序列1，它的成本爲1. 例如，當給出序列3,2,1,2,11時，我們可以使序列是非成本4減少（通過減少3到2和增加-1到2，所以非遞減的順序將是2，2，2，2，11）根據此問題的editorial，就可以解決這個問題使用2個序列的動態規劃（一個是給定的序列，另一個是

2熱度

1回答

在形式邏輯中證明正確性

我想知道是否有人能幫我回答這個問題。它來自之前的考試報告，我可以在知道準備好今年考試的答案的情況下做。這個問題似乎很簡單，我完全失去了，究竟是什麼要求？考慮代碼涉及整數變量的以下部分： if (i < j) { m = i; } else { m = j; } 通過規定適當的輸出條件，然後驗證正確性的代碼段的，證明執行之後，m是等於 i和j的最小值。我已經拿到了

2熱度

1回答

如何證明以下算法的正確性？

考慮以下算法min，它將列表x，y作爲參數，並以x和y的並集返回第z個最小元素。前提條件：X和Y是按升序排列的整數列表，它們是不相交的。公告稱，其僞代碼，所以索引從1開始不是0 Min(x,y,z): if z = 1: return(min(x[1]; y[1])) if z = 2: if x[1] < y[1]: return(m

3熱度

2回答

爲了證明SKK和II是beta相當的，lambda微積分

我是lambda微積分新手，正努力證明以下幾點。 SKK和II是beta等價物。其中 S =拉姆達xyz.xz（YZ） K =拉姆達xy.x I =拉姆達XX 我試圖測試通過打開它減少SKK，卻得到了不通，它變得混亂。不認爲SKK還可以不擴大S爲減少，K

9熱度

6回答

寫一個算法的證明

嗨，大家好，我試圖比較2個算法，並認爲我可能會嘗試爲他們寫一個證明！（我的數學很爛所以因此問題）通常，在去年我們的數學課，我們將給予像一個問題證明：（2R + 3）= N（N + 4）然後我會做所需的4個階段，並在最後得到答案我在哪裏卡住證明prims和克魯斯卡爾斯 - 我怎樣才能得到這些算法在形式像上面的數學一樣，所以我可以着手證明注意：我不是要求人們回答疫情週報對我來說 - 只要幫

0熱度

1回答

我需要一個函數後置條件的證明

這是一項家庭作業，但我無法通過編寫正式的證明來解決整個業務問題。任何人都可以破解這個和寫正式證明此FNC的後置條件：串REPLACE_BY（字符串s，炭C，炭d）後置條件返回的值是通過替換每發生從s形成的串c（d）（否則保持不變）。

1熱度

1回答

LAMBDA減少證明S K'= K我

您好我無法證明這些組合子S K'= K我用括號[]中的步驟只是告訴你步驟我在做什麼。例如λyz.xz（yz）中的[λxy.x/ x]表示我將用表達式λyz.xz（yz）中的每個x代替（λxy.x）我到目前爲止所嘗試的是減少SK和我得到這個： S K (λxyz.x z(y z)) (λxy.x) [λxy.x/x] in λyz.x z(y z) (λyz. (λxy.x) z(y z)

1熱度

1回答

證明通過使用+2

我想知道是否通過誘導這種變異證明是正確的感應感應的證明標準規定，如果一個公式/算法，適用於N和可以證明它適用於N + 1那麼你可以假設它適用於每個大於或等於n的整數。現在，如果你有2個基本情況（例如：2和3），並且你要證明它適用於n + 2，那麼你可以說它適用於每個大於2的整數嗎？，因爲假設你能證明它的正確的N + 2， 2+2=4 3+2=5 4+2=6 等，讓你覆蓋每一個整數更大然

2熱度

1回答

懶惰計算的正確性與總體（勒柯克）

正如標題所暗示的，我的問題的關注證明在勒柯克算術表達式的惰性評估的正確性和整體性。我想證明的定理總共有三種：計算中只給出規範表達式作爲結果定理Only_canonical_results：（FORALL X Y：AEXP，比較x和y - >規範Y）。正確性：計算關係保留表達式的外延定理correct_wrt_semantics：（forall的x和y：AEXP，小樣X Y - >