Agda中允许省略函数不可能输入定义的公理是什么？

首先看给出的Agda函数定义：

_/_ : (dividend divisor : ℕ) .{{_ : NonZero divisor}} → ℕ
m / (suc n) = div-helper 0 n m n

一、这种定义的形式化依据 #

这个定义的核心是依赖类型的约束能力，结合Agda的实例参数机制实现：

• NonZero divisor是依赖于divisor的谓词类型：当divisor为zero时，该类型是空类型（无任何元素）；当divisor为suc n（非零自然数）时，该类型存在合法元素。
• 函数_/_的类型要求必须提供NonZero divisor的实例参数（.{{...}}表示隐式实例参数），这意味着只有除数非零时，该函数才有合法调用方式。
• 从类型论角度，这利用了空类型的消除规则：空类型没有居民，因此不可能构造出divisor = zero的合法调用场景。Agda的类型检查器会验证所有合法调用必然满足除数非零，因此无需为除数为0的情况编写定义分支。

二、类型论中是否存在对应公理？ #

这种“省略不可能输入定义”的能力不需要额外添加类似公理J、K的新公理，它是依赖类型系统中空类型消除规则的直接推论：

• 空类型（通常记作⊥）的消除规则规定：对于任意类型A，存在函数⊥-elim : ⊥ → A。也就是说，只要能得到空类型的元素，就能生成任意类型的结果——但空类型根本没有元素，所以这个函数永远不会被实际调用。
• 在除法函数的例子中，如果强制构造除数为0的调用，就需要提供NonZero zero（空类型）的实例，此时我们可以用⊥-elim直接生成ℕ类型的结果，但这种场景不可能在合法代码中出现，因此无需显式写出该分支。
• 公理J、K是针对等式类型的规则（J是等式的归纳原理，K用于证明等式的唯一性），和这种处理不可能输入的能力属于不同范畴，二者没有直接关联。

内容的提问来源于stack exchange，提问作者Lunuy