在Agda中可以定義一個具有方程的數據類型嗎？

我想描述的整數：在Agda中可以定義一個具有方程的數據類型嗎？

data Integer : Set where 
    Z : Integer 
    Succ : Integer -> Integer 
    Pred : Integer -> Integer 
    ?? what else

以上沒有定義的整數。我們需要Succ（Pred x）= x和Pred（Succ x）= x。但是，

spReduce : (m : Integer) -> Succ (Pred m) = m 
    psReduce : (m : Integer) -> Pred (Succ m) = m

無法添加到數據類型。整數的一個更好的定義是肯定，

data Integers : Set where 
    Pos : Nat -> Integers 
    Neg : Nat -> Integers

不過我很好奇，如果有等式添加到數據類型的方式。

來源

2014-10-28 Jonathan Gallagher

請注意，由於0是一個「Nat」，所以您仍然可以將'Pos 0'和'Neg 0'作爲整數0的兩個冗餘表示形式。 – Cactus 2014-10-28 02:48:05

看來你想要做的就是定義你的Integers類型的標識Succ (Pred m)與m等阿格達不支持了等價關係的商式的 - 有一個實驗庫試圖做到這一點（通過迫使所有函數通過需要證明表示不變的輔助函數來定義商數類型的所有函數），但是隨後有人發現實現不夠嚴密，因此可能導致不一致（基本上通過訪問其中一個假設是從外部無法訪問的），詳情可參見this message：

我們不確定這個破解是否正確。現在，多謝丹，我知道它不是。

[...]

鑑於這些觀察，很容易證明，上面的假設是站不住腳：

我認爲最好的時刻（如果你想/需要堅持一個鬆散的表示與等價它收緊）是定義你的類型Setoid ..

來源

2014-10-28 02:55:18 Cactus

感謝您的參考！ – 2014-10-28 17:29:28

我會去了解它通過定義一個record：

record Integer (A : Set) : Set where 
    constructor integer 
    field 
    z : A 
    succ : A -> A 
    pred : A -> A 
    spInv : (x : A) -> succ (pred x) == x 
    psInv : (x : A) -> pred (succ x) == x

此記錄可用作某種類型A的行爲應該如Integer的證明。

來源

2014-10-28 13:04:01

在Agda中可以定義一個具有方程的數據類型嗎？

回答

相關問題