2

我正在尝试实现一种表示无限二叉树上（可能）无限路径的类型。当前的定义类似于标准库中的Conat。

open import Size
open import Codata.Thunk

data BinaryTreePath (i : Size) : Set where
  here : BinaryTreePath i
  branchL : Thunk BinaryTreePath i → BinaryTreePath i
  branchR : Thunk BinaryTreePath i → BinaryTreePath i

zero : ∀ {i} → BinaryTreePath i
zero = branchL λ where .force → zero

infinity : ∀ {i} → BinaryTreePath i
infinity = branchR λ where .force → infinity

现在我想定义一个重复部分更长的值，例如 LRRL。我现在能写的最好的是以下（很快就会变得乏味）。

sqrt2 : ∀ {i} → BinaryTreePath i
sqrt2 =
  branchL λ where .force → branchR λ where .force → branchR λ where .force → branchL λ where .force → sqrt2

-- or --

sqrt2 : ∀ {i} → BinaryTreePath i
sqrt2 = branchL λ where
  .force → branchR λ where
    .force → branchR λ where
      .force → branchL λ where
        .force → sqrt2

目标

定义branchL'和branchR'使以下通过类型检查和终止检查。

sqrt2 : ∀ {i} → BinaryTreePath i
sqrt2 = branchL' (branchR' (branchR' (branchL' sqrt2)))

到目前为止我尝试过的事情

将部件包装在常规函数中不起作用：

branchL' : (∀ {i} → BinaryTreePath i) → (∀ {j} → BinaryTreePath j)
branchL' path = branchL λ where .force → path

zero' : ∀ {i} → BinaryTreePath i
zero' = branchL' zero'
--               ^^^^^ Termination checking failed

所以我尝试包装成一个宏，但我找不到如何构造这个术语branchL λ where .force → pathwhen pathis given as a Term。以下也不起作用：

open import Agda.Builtin.Reflection
open import Data.Unit
open import Data.List

macro
  branchL' : Term → Term → TC ⊤
  branchL' v hole = do
    path ← unquoteTC v
    term ← quoteTC (branchL λ where .force → path)
    --                                       ^^^^ error
    unify hole term

{- error message:
Cannot instantiate the metavariable _32 to solution BinaryTreePath
.j since it contains the variable .j which is not in scope of the
metavariable or irrelevant in the metavariable but relevant in the
solution
when checking that the expression path' has type BinaryTreePath .j
-}
4

1 回答 1

4

Rather than writing branchL' and branchR', may I suggest mimicking what we do in Codata.Stream to define the unfolding of a cycle?

The key idea is that we can define auxiliary functions which use Thunk in their type and thus guarantee that they are using their argument in a guarded manner.

The first step is to define a small language of Choices one can make and give it a semantics in terms of BinaryTreePath:

data Choice : Set where
  L R : Choice

choice : ∀ {i} → Choice → Thunk BinaryTreePath i → BinaryTreePath i
choice L t = branchL t
choice R t = branchR t

We can then lift this semantics to not only work for individual choices but also lists of choices:

open import Data.List

_<|_ : ∀ {i} → List Choice → BinaryTreePath i → BinaryTreePath i
[]       <| t = t
(c ∷ cs) <| t = choice c (λ where .force → cs <| t)

Now comes the crucial bit: if we have a non-empty list of choices, we know statically that the path it will lead to will be guarded.

open import Data.List.NonEmpty

_⁺&lt;|_ : ∀ {i} → List⁺ Choice → Thunk BinaryTreePath i → BinaryTreePath i
(c ∷ cs) ⁺&lt;| t = choice c (λ where .force → cs <| t .force)

Using this combinator we can seamlessly define cycle:

cycle : ∀ {i} → List⁺ Choice → BinaryTreePath i
cycle cs = cs ⁺&lt;| (λ where .force → cycle cs)

And then your example is obtained directly by using cycle:

sqrt2 : ∀ {i} → BinaryTreePath i
sqrt2 = cycle (L ∷ R ∷ R ∷ L ∷ [])

I've put the code in a self-contained gist.

于 2019-03-26T17:45:23.490 回答