6260 notes: nat, absDiff, if 条件即证明

nat 能不能喂给收 int 的函数?

子集冒充全集成员,永远安全;全集冒充子集成员,需要论证。

写的每个返回类型都是一句需要被证明的承诺。

function f(x: int): int { x + 1 }
function g(n: nat): nat { n + f(n) }

g 把 nat 传给收 int 的 f,这是子集冒充全集,安全。但如果 f 的函数体改成 x - 100,g 就编译不过 —— 因为 f 可能返回负数,而 g 承诺返回 nat。

function d(a: nat, b: nat): nat { a - b }   // 直接打回

差的绝对值

|x| 的定义本就是分段的:

①x >= 0, |x| = x

②x < 0, |x| = -x

|a-b|同理:

① a >= b, |a-b| = a - b

② a < b, |a-b| = b - a

先减出负数、再翻正 ──改为──→ 先判断方向,再做一个保证非负的减法。

nat 的哲学是让负数不发生。

选对定义方式,证明就消失;选歪定义,后面全是补丁。

function absDiff(a: nat, b: nat): nat {
  if a >= b then a - b else b - a
}
/* absolute difference, but on nats */

then 分支里,a >= b 这个条件本身就是证明。

if 的条件不只是控制流,它是流进每个分支的一条已知事实。

Main

method Main()
{
  print "absDiff(3,7) = ", absDiff(3, 7), "\n";
  print "absDiff(7,3) = ", absDiff(7, 3), "\n";
}

两个易错点:

Main 后面要加 ()

method 体里每条语句要以 ; 分号结尾（而function 体是表达式,不要以;结尾）