Agda: упрощение рекурсивных определений с использованием Thunk

Я пытаюсь реализовать тип, представляющий (возможно) бесконечный путь в бесконечном двоичном дереве. В настоящее время определение напоминает определение 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

Теперь я хочу определить значение, которое имеет более длинные повторяющиеся части, например. ЛРРЛ. Лучшее, что я могу написать прямо сейчас, это следующее (что быстро становится утомительным).

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 → path, когда path задается как 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
-}

codata agda
person Bubbler    schedule 25.03.2019    source источник

Ответы (1)


arrow_upward
4
arrow_downward

Вместо того, чтобы писать branchL' и branchR', могу я предложить имитировать то, что мы делаем в Codata.Stream определить развертывание цикла?

Ключевая идея заключается в том, что мы можем определить вспомогательные функции, которые используют Thunk в своем типе, и, таким образом, гарантировать, что они используют свой аргумент защищенным образом.

Первый шаг — определить небольшой язык Choice, который можно создать, и придать ему семантику в терминах 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

Затем мы можем расширить эту семантику, чтобы она работала не только для отдельных вариантов, но и для списков вариантов:

open import Data.List

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

Теперь самое важное: если у нас есть непустой список вариантов, мы знаем статически, что путь, к которому он приведет, будет защищен.

open import Data.List.NonEmpty

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

Используя этот комбинатор, мы можем легко определить cycle:

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

И тогда ваш пример получается напрямую с помощью цикла:

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

Я поместил код в самостоятельный список.

person gallais    schedule 26.03.2019