AbstractDataType - Nat

Question

我在这里得到了这个抽象的模型，并试图理解它是如何工作的，但无法理解它。

type: NAT

构造函数

null: → NAT 
succ: NAT → NAT 

算子

add: NAT×NAT→ NAT

公理 x，y: NAT

add(X, null) = X
add(X, succ(Y)) = succ(add(X, Y))

问题在于添加。我试着输入一些数字但是..。是怎么回事？-

添加(2，succ(3)) =succ(添加(2，3))现在呢？我只想要2+3 =5

Answer 1

NAT是与'+‘一起的自然数集合，succ是后继函数 (通常与Peano公理有关)

您的2+3示例计算如下：

add(2,3) = succ(add(2,2))
         = succ(succ(add(2,1))) 
         = succ(succ(succ(add(2,0))))
         = succ(succ(succ(2)))
         = succ(succ(3))
         = succ(4)
         = 5