senioria的Agda笔记

公开区
,
1

还是想让ll学术一点的, 但似乎没有什么学术内容好发就发这个吧 qwq (超小声(
senioria也是入门, 基本就是plfa搬运/读书笔记之类的 >< (超小声(

具体讲解agda的部分大概不会很详细… 因为东西都在plfa里了… (超小声(

bb

这就过分

5 个赞
3

滋磁qwq

2 个赞
4

自然数, 和基础语法

我们可以用皮亚诺公理来定义自然数, 这里并不想细说皮亚诺公理的内容, 容易看到, 我们可以用如下方法构造出一种自然数(bb: 当然也可以不包括0, 但这样会让后面的一些东西有点难做…):

  • 定义0为第一个自然数;
  • 定义从一个自然数生成下一个自然数的映射suc, 并且让它满足归纳法.

那么, 在agda里, 我们可以这么定义:

data Nat : Set where
  zero : Nat
  suc : Nat -> Nat

因为是笔记而非教程… 所以senioria就暂时忽略语法方面的介绍吧… >< (超小声(
容易验证, 这样构造出来的自然数满足皮亚诺公理. (超小声(

我们可以定义加法, 不带负数的减法, 乘法和乘方, 这些定义的数学意义都相当直观:

_+_ : Nat -> Nat -> Nat
zero + n = n
suc m + n = suc (m + n)

_.-_ : Nat -> Nat -> Nat
m .- zero = m
zero .- n = zero
suc m .- suc n = m .- n

_*_ : Nat -> Nat -> Nat
zero * n = zero
suc m * n = n + (m * n)

_^_ : Nat -> Nat -> Nat
m ^ zero = 1
m ^ suc n = m * (m ^ n)

和haskell一样, agda的函数和算符也会柯里化(虽然senioria的理解似乎不准确><): 一切函数都只有一个参数, 多个参数的函数实际上是多次抽象/调用的语法糖. 所以可以部分调用一个函数来得到另一个函数.

练习: 二进制数基础

可以如此构造二进制数:

data Bin : Set where
  <> : Bin
  _O : Bin -> Bin
  _I : Bin -> Bin

因为这里的两个构造器都必须接受Bin作为参数, 我们必须定义一个哑元来作为构造的开始, 这也使得我们不能构造理想的二进制数字符串. 同时, 我们也决定认为<>不是合法的二进制字符串. (超小声(
注意到我们的这一定义中并未排除前导0, 所以构造出来的二进制字符串未必是最简的, 之后的练习将会解决这一问题. (超小声(

练习是构造以下几个函数:

inc : Bin -> Bin  -- 给定二进制数i, 得到i + 1
from : Bin -> Nat  -- 将二进制数转换为等价的整数
to : Nat -> Bin  -- 将整数转换为等价的二进制数, 0转化为<> O

下面是它们的实现(也许还是过于复杂 >< ):

inc <> = <> I
inc (b O) = b I
inc (b I) = (inc b) O

from <> =  zero
from (b O) = from b + from b
from (b I) = suc (from b + from b)

to zero = <> O  -- 虽然确实不合理, 但是题目如此要求了><
to (suc n) = inc (to n)

下面的部分… 先咕咕一下 qwq (超小声(

4 个赞
5

好耶！

4 个赞