如何在 Kind-Lang 等纯函数式语言中使用代数数据类型对 Int 类型进行编码?

问题描述

在 Kind-Lang 等函数式语言助手中,自然数通常被形式化为具有两个构造函数(零和 succ)的递归代数数据类型:

type Nat {
  zero
  succ(pred: Nat)
}

至于 Int 类型,它也包含负数,在 Kind 上编码它的最佳方法是什么?

解决方法

对 Int 类型进行编码的一种简单方法是制作一对 Nat 和一个符号。例如:

Int: Type
  Pair<Bool,Nat>

但是这个定义有一个问题:它包含两个零(-0+0),因此,为了与传统的 Int 集同构,我们需要考虑符号为负时加 1 的数字。因此,例如,{false,2} 代表 -3{false,3} 代表 -4,依此类推。

Agda 使用类似的编码,代替 Bool,每个符号都有一个构造函数。我们可以将其移植为:

// Int.pos(n) represents +n
// Int.neg(n) represents -(n + 1)
type Int {
  pos(n: Nat)
  neg(n: Nat)
}

两种表示都有效,但使用它们来编写算法和证明定理是复杂且容易出错的。例如,这里是 addInt

Int.negate(a: Int): Int
  case a {
    pos: case a.nat {
      zero: Int.pos(Nat.zero)
      succ: Int.neg(a.nat.pred)
    }
    neg: Int.pos(Nat.succ(a.nat))
  }

Int.add(a: Int,b: Int): Int
  case a b {
    pos pos: Int.pos(Nat.add(a.nat,b.nat))
    neg neg: Int.neg(Nat.succ(Nat.add(a.nat,b.nat)))
    pos neg: if b.nat <? a.nat
      then Int.pos((a.nat - b.nat) - 1)
      else Int.neg(b.nat - a.nat)
    neg pos: Int.add(Int.pos(b.nat),Int.neg(a.nat))
  }

一种更好的替代方法,常用于立方语言,是将 Int 表示为商。所以,例如,在 Agda 中,我们可以这样写:

data Int : Set where
  mkInt : (pos neg : Nat) -> Int
  canon : (pos neg : Nat) -> mkInt (suc pos) (suc neg) = mkInt pos neg

这样,我们将整数表示为一对两个 nat,整数表示为第一个自然数减去第二个自然数。因此,例如,mkInt 5 2 代表 3,而 mkInt 2 5 代表 -3。这种编码的问题在于它有很多方法来表示相同的 Int。例如,2 可以表示为 mkInt 2 0mkInt 3 1mkInt 4 2 等。因此,这种类型不会与整数同构。不过,多亏了第二个参数,当我们用一个商数来扩展集合时,它可以识别相同的术语。

在 Kind 中,我们没有直接商,但是,由于使用 Self 编码来表示底层的数据类型,我们能够构建计算构造函数或智能构造函数。这些构造函数与常规构造函数类似,不同之处在于,在某些情况下,它们不会“卡住”。相反,计算以达到规范形式。这样,我们可以用与上面的编码类似的方式对 Int 类型进行编码,加上一个规则,导致 mkInt (succ i) (succ j) reducemkInt i j,直到一个大小为零。所以,我们可以这样写:

type Int {
  new(pos: Nat,neg: Nat) with {
    zero zero: new(zero,zero)             // stuck,thus canonical
    zero succ: new(zero,succ(neg.pred))   // stuck,thus canonical
    succ zero: new(succ(pos.pred),zero)   // stuck,thus canonical
    succ succ: Int.new(pos.pred,neg.pred) // non-stuck,thus computes
  }
}

遗憾的是,上面的语法还没有在 Kind 中实现,但我们可以通过手动编写它们的自编码来直接构建 Int(和类似类型):

Int: Type
  int<P: Int -> Type> ->
  (new: (pos: Nat) -> (neg: Nat) -> P(Int.new(pos,neg))) ->
  P(int)

Int.new(pos: Nat,neg: Nat): Int
  (P,new)
  case pos {
    zero: new(Nat.zero,neg)                     
    succ: case neg {
      zero: new(Nat.succ(pos.pred),Nat.zero)
      succ: Int.new(pos.pred,neg.pred)(P,new)
    }!
  }: P(Int.new(pos,neg))

这个定义有效,让我们有更简单的算法和证明。例如,对于这种新类型,这里是 Int.add

Nat.add(n: Nat,m: Nat): Nat
  case n {
    zero: m
    succ: Nat.succ(Nat.add(n.pred,m))
  }

Int.add(a: Int,b: Int): Int
  open a
  open b
  Int.new(Nat.add(a.pos,b.pos),Nat.add(a.neg,b.neg))

注意它只是重用了 Nat.add。与商相比,这个 Int 的证明更简单,因为 mkInt 3 1mkInt 2 0 根据定义变得相等。

two_is_two: mkInt 3 1 == mkInt 2 0
  refl

相关问答

错误1:Request method ‘DELETE‘ not supported 错误还原:...
错误1:启动docker镜像时报错:Error response from daemon:...
错误1:private field ‘xxx‘ is never assigned 按Alt...
报错如下,通过源不能下载,最后警告pip需升级版本 Requirem...