Agda:如何获得依赖类型的值？

Question

我最近问过这个问题: 该类型中使用的agda命题 - 它是什么意思？ 并收到了一个非常深思熟虑的答案,关于如何使类型隐式并获得真正的编译时错误.

但是,我仍然不清楚如何使用依赖类型创建值.

考虑:

div : (n : N) -> even n -> N
div zero p = zero
div (succ (succ n)) p= succ (div n p)
div (succ zero) ()

其中N是自然数,甚至是以下命题.

even : N -> Set
even zero = \top
even (succ zero) = \bot
even (succ (succ n)) = even n
data \bot : Set where
record \top : Set where

假设我想写一个函数如下:

f : N -> N
f n = if even n then div n else div (succ n)

我不知道如何以我想要的方式做这样的事情......在我看来,最好的办法就是有一个证明(不是(偶数n))\到偶数(succ n).我真的不知道如何在agda中表达这一点.我能写

g : (n:N) -> (even n) -> (even (succ n)) -> N
g n p q = if evenB n then (div n p) else (div (succ n) q)

从这里,我可以做以下事情:

g 5 _ _ 

并评估为正常形式......以获得答案.如果我想写f,我可以这样做

f n = g n ? ?

我得到fn = gn {} 1 {} 2其中？1 =偶​​数n,而？2 =偶数(succ n).然后,我可以像f五那样做,并评估为正常形式.我真的不明白为什么这是有效的...有没有办法告诉agda更多关于以这种方式定义的f的信息.我能否确定如果？1失败？2会成功,所以告诉agda评估f总是有意义的吗？

我将g解释为一个函数,它取n个数,证明n是偶数,证明(succ n)是偶数,并给出一个数.(这是阅读本文的正确方法 - 或者任何人都可以建议更好的方式来阅读本文？)我真的很想完全(或更准确地)理解上述类型如何检查.它是否使用感应 - 它是否连接(偶数B n)与p:偶数n ?? 等等我现在很困惑,因为它知道这一点

if evenB n then (div n q) else (whatever)
if evenB n then div (succ n) q else div n p

不对.第一个我理解为什么 - q是succ n,所以它不匹配.但是第二次失败了,原因更加神秘,而且似乎Agda比我想象的更强大......

如果我能弄明白该怎么做,这是我真正喜欢的第一步(如果有意义的话).

g : (n : N) -> (even n) -> N
g n p = if evenB n then (div n p) else (div (succ n) (odd p))

奇数p是证明即使n是荒谬的证据,那么succ n是偶数.我想,这需要我能够处理依赖类型的值.

最终,我希望能够写出这样的东西:

g : N -> N
g n = 
  let p = proofthat n is even
  in
      if evenB n then div n p else (div (succ n) (odd p))

或类似的规定.甚至

g : N -> N
g n = if evenB n then let p = proofThatEven n in div n p else let q = proofThatEven succ n in div n q

我真的想知道如何制作一个与依赖类型相对应的证明,以便我可以在程序中使用它.有什么建议？

Answer 1

功能和主张

编码作为命题和函数之间存在着至关重要的区别.让我们看看_+_实现为数字和函数的关系.

当然,功能是微不足道的:

_+_ : (m n : ?) ? ?
zero  + n = n
suc m + n = suc (m + n)

_+_作为一个命题是数字的三元关系.对于数字m,n并且o,它应该持有正是时候m + n = o:

data _+_?_ : ? ? ? ? ? ? Set where
  zero : ? {  n  }             ? zero  + n ? n
  suc  : ? {m n o} ? m + n ? o ? suc m + n ? suc o

我们可以举例说明2 + 3 ? 5:

proof : 2 + 3 ? 5
proof = suc (suc zero)

现在,函数对于允许的内容更加严格:它必须通过终止检查器,必须有唯一的结果,所有情况都必须被覆盖等等; 作为回报,他们给我们可计算性.命题允许冗余,不一致,部分覆盖等等,但实际上表明2 + 3 = 5,程序员必须参与其中.

这当然是你的显示器if:你需要能够计算它的第一个参数!

它甚至是吗？

但是有希望:我们可以证明你的even命题对于每个自然数都是可计算的(我应该说是可判定的).我们如何表明这一点？通过编写一个函数来决定它.

我们需要对命题进行否定:

data ? : Set where

¬_ : Set ? Set
¬ A = A ? ?

接下来,我们将记下一个数据类型,告诉我们这个建议是否成立:

data Dec (P : Set) : Set where
  yes :   P ? Dec P
  no  : ¬ P ? Dec P

最后,我们将定义even可判定的含义:

EvenDecidable : Set
EvenDecidable = ? n ? Dec (even n)

这是:even如果对于任何自然数n我们可以显示任何一个even n或者是可判定的¬ (even n).让我们证明这确实是真的:

isEven : EvenDecidable
isEven zero          = yes _
isEven (suc zero)    = no ? ()
isEven (suc (suc n)) = isEven n

从Dec到Bool

现在,我们有:

data Bool : Set where
  true false : Bool

if_then_else_ : {A : Set} ? Bool ? A ? A ? A
if true  then t else _ = t
if false then _ else f = f

和一个isEven返回的功能Dec,而不是Bool.我们可以从去Dec到Bool仅通过内部遗忘的证明(?可通过输入\clL,?通过\clR):

?_? : {P : Set} ? Dec P ? Bool
? yes _ ? = true
? no  _ ? = false

最后,我们可以使用isEven在if:

if ? isEven n ? then ? else ?

衍生矛盾

接下来,你的g功能:您既需要的证明even n和even (suc n).这是行不通的,因为没有人可以给这两者.事实上,我们甚至可以使用以下方法得出矛盾:

bad : ? n ? even n ? even (suc n) ? ?
bad zero          p q = q
bad (suc zero)    p q = p
bad (suc (suc n)) p q = bad n p q

但是,两者都有

bad? : ? n ? even n ? even (suc n) ? ?
bad? n p q = div (suc n) q

bad? : ? n ? even n ? even (suc n) ? ?
bad? n p q = div n p

typecheck就好了,所以我不完全确定你为什么遇到第二个问题if.

把它们放在一起

现在,我们将进入主要部分,即odd功能.如果我们知道这个数字不是even,我们应该能够证明继任者是even.我们将重用以前的否定.agda-mode只需填写右侧C-c C-a:

odd : ? n ? ¬ even n ? even (suc n)
odd zero          p = p _
odd (suc zero)    p = _
odd (suc (suc n)) p = odd n p

现在我们有了编写g函数的所有成分:

g : ? ? ?
g n = ?

我们将询问该号码是否正在even使用该isEven功能:

g : ? ? ?
g n with isEven n
... | isItEven = ?

现在,我们将模式匹配isItEven以找出结果:

g : ? ? ?
g n with isEven n
... | yes e = ?
... | no  o = ?

e是一个证明的数量为even,o是一种证明,它不是even(它有一个类型¬ even n).e可以直接使用div,因为o我们需要使用odd之前定义的函数:

g : ? ? ?
g n with isEven n
... | yes e = div n e
... | no  o = div (suc n) (odd n o)

if 对于 Dec

但是,您无法实现上述版本if.Booleans不附带任何其他信息; 他们肯定没有我们需要的证据.我们可以编写一个if与之相关的变体Dec而不是Bool.这为我们提供了相关的证据分配到的能力then和else分支机构.

if-dec_then_else_ : {P A : Set} ? Dec P ? (P ? A) ? (¬ P ? A) ? A
if-dec yes p then t else _ = t  p
if-dec no ¬p then _ else f = f ¬p

请注意,两个分支实际上都是将证明作为其第一个参数的函数.

g : ? ? ?
g n = if-dec isEven n
  then (? e ? div n e)
  else (? o ? div (suc n) (odd n o))

我们甚至可以为此创建一个很好的语法规则if; 在这种情况下,它几乎是无用的,但是:

if-syntax = if-dec_then_else_

syntax if-syntax dec (? yup ? yupCase) (? nope ? nopeCase)
  = if-dec dec then[ yup ] yupCase else[ nope ] nopeCase

g : ? ? ?
g n = if-dec isEven n
  then[ e ] div n e
  else[ o ] div (suc n) (odd n o)

什么with？

现在,我注意到with在上一个问题中链接的介绍的后面部分中提到了该构造.以下是它的工作原理:

有时您需要在中间表达式上进行模式匹配,例如isEven在上面的代码中.要做到这一点with,你需要实际编写两个函数:

h? : (n : ?) ? Dec (even n) ? ?
h? n (yes e) = div n e
h? n (no  o) = div (suc n) (odd n o)

h? : ? ? ?
h? n = h? n (isEven n)

h?设置我们想要模式匹配的表达式h?并进行实际的模式匹配.现在,像这样的中间表达式上的模式匹配相当频繁,因此Agda为我们提供了更紧凑的表示法.

h : ? ? ?
h n with isEven n
h n | yes e = div n e
h n | no  o = div (suc n) (odd n o)

所以,with表现得好像它添加了一个我们可以模式匹配的额外参数.您甚至可以同时使用with多个表达式:

i : ? ? ?
i n with isCool n | isBig n
i n | cool | big = ?

然后我们可以模式匹配cool,big就像函数有3个参数一样.现在,大部分时间原始左侧保持不变,就像之前的功能所示(在某些情况下它实际上可能不同,但我们现在不需要处理).对于这些情况,我们得到一个方便的快捷方式(特别是当左侧很长时):

i : ? ? ?
i n with isCool n | isBig n
... | cool | big = ?