如何避免Coq nats中的堆棧溢出或分段錯誤？

我目前正在與vellvm合作，對其進行改造。我是coq新手。如何避免Coq nats中的堆棧溢出或分段錯誤？

編程時，我遇到以下警告：

Warning: Stack overflow or segmentation fault happens when working with large numbers in nat (observed threshold may vary from 5000 to 70000 depending on your system limits and on the command executed).

我的函數生成此警告計算簽名。簽名分爲上位和下位。給定兩個n1和n2代表高位和低位，它計算（n1 * 65536）+ n2 - 這是將兩個16位二進制數並排放置的抽象。

我很驚訝，因爲COQ NAT定義似乎處理來自外部的大整數，由於構造函數。

我應該如何避免此警告/ COQ中使用大的數字？我打算改變實現從nat到某種二進制構造。

謝謝！

來源

2012-12-01 fotanus

與NATS的工作是這些混沌，因爲他們與'S'建成，這意味着每個號碼將*字面上*是'S'應用程序：你可能會代替整數，它們具有類似的證據原則，但有一個工作基於符號/幅度（位）的表示法：http://coq.inria.fr/library/Coq.ZArith.BinInt.html –

那我該如何使用這些操作呢？（Zpos 1）+（Zpos 2）似乎不工作... - 錯誤：術語「1％Z」有類型「|」而預計會有類型「nat」。 – fotanus

這是因爲「+」意味着多個事情取決於你在哪裏。實際上，「+」只是用於添加nats的語法糖，其中'plus'是在兩個nats上嚴格定義的。你希望使用'plus'作爲整數，它與'nat'（即'Int_scope'）生活在不同的_interpretation scope_中。閱讀關於解釋範圍以及如何打開並使用它們。 –

而不是在Coq中使用nat類型，它有時（當你必須操縱大數字時）更好地使用Z類型，這是使用符號幅度對錶示形式整數的形式化。權衡是你的證明可能稍微複雜一些; nat非常簡單，因此承認簡單的證明原則。

然而，勒柯克有一個廣泛使用的符號，使之易於編寫定義，定理，和證明。 Coq有一個非常小的內核（我們希望這樣做，因爲我們希望能夠相信證明檢查器是正確的，並且我們可以讀取它），並在其上面有很多標記。然而，由於事物有不同的表現形式，只有少數好的符號，我們的符號通常會發生衝突。爲了突破這個，COQ使用interpretation scopes消除歧義的符號，並把它們分解成的名字（因爲「+」表示add，plus，等...）。

你是對的，使用Z_scope是+對於plus在Z內。

來源

2012-12-01 20:05:20

如何避免Coq nats中的堆棧溢出或分段錯誤？

回答

相關問題