为什么Agda会减少对某些参数的函数应用，而不减少对其他参数的应用？

Question

我正在使用标准库的AVL树实现中的joinˡ⁺。该函数由六个模式匹配子句定义。当我将函数应用于参数时，Agda会减少或不减少函数应用程序表达式，这取决于六个子句中哪一个与我的参数匹配。(在我看来是这样的。)

下面的代码将函数应用于与函数的第一个子句匹配的参数。这是在目标的左边平等的一面。Agda把它缩小到右手边，我可以用refl完成验证.所以这个就像预期的那样起作用。

(请注意，代码使用了标准库的1.3版本。最近的版本似乎将AVL树代码从Data.AVL移到了Data.Tree.AVL。)

module Repro2 where

open import Data.Nat using (ℕ ; suc)
open import Data.Nat.Properties using (<-strictTotalOrder)
open import Data.Product using (_,_)
open import Relation.Binary.PropositionalEquality using (_≡_ ; refl)

open import Data.AVL.Indexed <-strictTotalOrder

okay :
  ∀ {l u h} k₆ k₂ (t₁ : Tree (const ℕ) _ _ _) k₄ t₃ t₅ t₇ b →
  joinˡ⁺ {l = l} {u} {suc (suc h)} {suc h} {suc (suc h)}
    k₆ (1# , node k₂ t₁ (node {hˡ = h} {suc h} {suc h} k₄ t₃ t₅ b) ∼+) t₇ ∼-
  ≡
  (0# , node k₄ (node k₂ t₁ t₃ (max∼ b)) (node k₆ t₅ t₇ (∼max b)) ∼0)

okay k₆ k₂ t₁ k₄ t₃ t₅ t₇ b = refl

下一个示例的目标是函数定义的第二个子句。与上述不同的是，目标在这段时间内并没有减少，也就是说，joinˡ⁺不会消失。

not-okay : ∀ {l u h} k₄ k₂ (t₁ : Tree (const ℕ) _ _ _)  t₃ t₅ →
  joinˡ⁺ {l = l} {u} {suc h} {h} {suc h}
    k₄ (1# , node k₂ t₁ t₃ ∼-) t₅ ∼-
    ≡
    (0# , node k₂ t₁ (node k₄ t₃ t₅ ∼0) ∼0)

not-okay k₄ k₂ t₁ t₃ t₅ = {!!}

我遗漏了什么？

在MrO回答之后添加

MrO搞定了。我所知道的是，如果一个子句模式-匹配一个参数的子项(或整个参数)，那么我显然需要为该子项传递一个匹配的数据构造函数，以使评估器选择该子句。然而，这还不够。正如MrO所指出的，在某些情况下，我还需要传递数据构造函数，以获得其他子句(即，不只是我想要的子句)模式匹配的子项，尽管手头的子句并不关心它们。

为了探索这个(对我来说:主要的新的)洞察力，我尝试了joinˡ⁺的其余四个子句。最后一句，第6条，引出了另一种见解。

下面是第3条，它的工作原理与not-okay差不多。

clause₃ : ∀ {l u h} k₄ k₂ (t₁ : Tree (const ℕ) _ _ _) t₃ t₅ →
  joinˡ⁺ {l = l} {u} {suc h} {h} {suc h}
    k₄ (1# , node k₂ t₁ t₃ ∼0) t₅ ∼-
  ≡
  (1# , node k₂ t₁ (node k₄ t₃ t₅ ∼-) ∼+)

-- This does not work:
--   clause₃ k₄ k₂ t₁ t₃ t₅ = {!!} 

clause₃ k₄ k₂ t₁ (node k t₃ t₄ bal) t₅ = refl

第4条涉及的更多。

clause₄ : ∀ {l u h} k₂ (t₁ : Tree (const ℕ) _ _ _) t₃ →
  joinˡ⁺ {l = l} {u} {h} {h} {h}
    k₂ (1# , t₁) t₃ ∼0
  ≡
  (1# , node k₂ t₁ t₃ ∼-)

-- This does not work:
--   clause₄ k₂ t₁ t₃ = {!!}

-- This still doesn't, because of t' (or so I thought):
--   clause₄ k₂ (node k t t′ b) t₃ = {!!}

-- Surprise! This still doesn't, because of b:
--   clause₄ k₂ (node k t (leaf l<u) b) t₃ = {!!}
--   clause₄ k₂ (node k t (node k′ t′′ t′′′ b') b) t₃ = {!!}

clause₄ k₂ (node k t (leaf l<u) ∼0) t₃ = refl
clause₄ k₂ (node k t (leaf l<u) ∼-) t₃ = refl

clause₄ k₂ (node k t (node k′ t′′ t′′′ b') ∼+) t₃ = refl
clause₄ k₂ (node k t (node k′ t′′ t′′′ b') ∼0) t₃ = refl
clause₄ k₂ (node k t (node k′ t′′ t′′′ b') ∼-) t₃ = refl

第5条类似于第4条。

clause₅ : ∀ {l u h} k₂ (t₁ : Tree (const ℕ) _ _ _) t₃ →
  joinˡ⁺ {l = l} {u} {h} {suc h} {suc h}
    k₂ (1# , t₁) t₃ ∼+
  ≡
  (0# , node k₂ t₁ t₃ ∼0)

clause₅ k₂ (node k t (leaf l<u) ∼0) t₃ = refl
clause₅ k₂ (node k t (leaf l<u) ∼-) t₃ = refl

clause₅ k₂ (node k t (node k′ t'′ t′′′ b′) ∼+) t₃ = refl
clause₅ k₂ (node k t (node k′ t'′ t′′′ b′) ∼0) t₃ = refl
clause₅ k₂ (node k t (node k′ t'′ t′′′ b′) ∼-) t₃ = refl

第6条对我来说有点令人吃惊。我认为我需要在任何子句需要的地方传递数据构造函数。但MrO不是这么说的。它在这一条款中表明：

clause₆ : ∀ {l u h} k₂ (t₁ : Tree (const ℕ) _ _ _) t₃ b →
  joinˡ⁺ {l = l} {u} {h} {h} {h}
    k₂ (0# , t₁) t₃ b
  ≡
  (0# , node k₂ t₁ t₃ b)


clause₆ k₂ t₁ t₃ b = refl

比我想象的更容易:不需要额外的数据构造函数。为什么？我去阅读了Agda参考中的模式匹配部分：

https://agda.readthedocs.io/en/v2.6.1/language/function-definitions.html#case-trees

我以前读过，但完全没有照它说的去做。Agda发现该子句是通过决策树、案例树来选择的。在我看来，Agda现在似乎需要数据构造函数，只要它还没有到达案例树的叶子，也就是说，只要它还没有确定要选择哪个子句。

对于手头的函数，案例树似乎以以下问题开始：0#还是1#？至少这可以解释第6条：

• ，如果它是0#，那么我们知道它必须是第6条，不再需要数据构造函数。第6条是0#的唯一匹配项。所以，我们在一片叶子上，我们的案例树遍历结束了。

• ，如果是1#，那么我们需要做更多的匹配，即在case树中向下移动到下一个级别。在那里，我们需要另一个数据构造函数来查看。因此，我们总共需要为每个已访问的案例树级别创建一个数据构造函数。

。

至少这是我目前的心理模型，这似乎得到了关于joinˡ⁺的观察结果的支持。

为了进一步验证这个心理模型，我去修改了标准库的副本，颠倒了这六个条款的顺序。当Agda按照顺序遍历子句并在每个子句中从左到右来构建案例树时，这将给我们一个更好的案例树。

0#和1#仍然是决策树的第一层，但后面是外部平衡，然后是内部平衡。我们不需要将树分割成节点，除了现在(以前是第一个)子句，它实际上与节点匹配。

而且，事实上，事情的结果与预期的一样。下面是我修改过的标准库中与子句顺序相反的证据。

clause₁′ : ∀ {l u h} k₂ (t₁ : Tree (const ℕ) _ _ _) t₃ b →
  joinˡ⁺ {l = l} {u} {h} {h} {h}
    k₂ (0# , t₁) t₃ b
  ≡
  (0# , node k₂ t₁ t₃ b)

clause₁′ k₂ t₁ t₃ b = refl

clause₂′ : ∀ {l u h} k₂ (t₁ : Tree (const ℕ) _ _ _) t₃ →
  joinˡ⁺ {l = l} {u} {h} {suc h} {suc h}
    k₂ (1# , t₁) t₃ ∼+
  ≡
  (0# , node k₂ t₁ t₃ ∼0)

clause₂′ k₂ t₁ t₃ = refl

clause₃′ : ∀ {l u h} k₂ (t₁ : Tree (const ℕ) _ _ _) t₃ →
  joinˡ⁺ {l = l} {u} {h} {h} {h}
    k₂ (1# , t₁) t₃ ∼0
  ≡
  (1# , node k₂ t₁ t₃ ∼-)

clause₃′ k₂ t₁ t₃ = refl

clause₄′ : ∀ {l u h} k₄ k₂ (t₁ : Tree (const ℕ) _ _ _) t₃ t₅ →
  joinˡ⁺ {l = l} {u} {suc h} {h} {suc h}
    k₄ (1# , node k₂ t₁ t₃ ∼0) t₅ ∼-
  ≡
  (1# , node k₂ t₁ (node k₄ t₃ t₅ ∼-) ∼+)

clause₄′ k₄ k₂ t₁ t₃ t₅ = refl

not-okay′ : ∀ {l u h} k₄ k₂ (t₁ : Tree (const ℕ) _ _ _) t₃ t₅ →
  joinˡ⁺ {l = l} {u} {suc h} {h} {suc h}
    k₄ (1# , node k₂ t₁ t₃ ∼-) t₅ ∼-
    ≡
    (0# , node k₂ t₁ (node k₄ t₃ t₅ ∼0) ∼0)

not-okay′ k₄ k₂ t₁ t₃ t₅ = refl

okay′ :
  ∀ {l u h} k₆ k₂ (t₁ : Tree (const ℕ) _ _ _) k₄ t₃ t₅ t₇ b →
  joinˡ⁺ {l = l} {u} {suc (suc h)} {suc h} {suc (suc h)}
    k₆ (1# , node k₂ t₁ (node {hˡ = h} {suc h} {suc h} k₄ t₃ t₅ b) ∼+) t₇ ∼-
  ≡
  (0# , node k₄ (node k₂ t₁ t₃ (max∼ b)) (node k₆ t₅ t₇ (∼max b)) ∼0)

okay′ k₆ k₂ t₁ k₄ t₃ t₅ t₇ b = refl

Answer 1

为了使Agda能够减少您的表达式，需要在t₃上进行模式匹配

not-okay _ _ _ (leaf _) _ = refl
not-okay _ _ _ (node _ _ _ _) _ = refl

我对为什么需要这样做的理解如下：joinˡ⁺是根据五个参数进行归纳定义的。在每一种情况下，您都需要为Agda指定所有这些参数，以减少表达式(我的意思是Agda需要知道，对于所有这5个参数，哪些是当前给出的构造函数)。

在您的not-okay函数中，您考虑的是数量joinˡ⁺ {l = l} {u} {suc h} {h} {suc h} k₄ (1# , node k₂ t₁ t₃ ∼-) t₅ ∼-，在这种情况下，五个参数中有四个是指定的构造函数(1#、node k₂ t₁ t₃ ∼-、∼-和∼-)，而不是t₃，这是一个缺失的概念。

相反，在okay函数中，考虑的是数量joinˡ⁺ {l = l} {u} {suc (suc h)} {suc h} {suc (suc h)} k₆ (1# , node k₂ t₁ (node {hˡ = h} {suc h} {suc h} k₄ t₃ t₅ b) ∼+) t₇ ∼-，其中已经指定了所有五个元素。