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

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

1 голос
/ 26 марта 2019

Я пытаюсь реализовать тип, который представляет (возможно) бесконечный путь в бесконечном двоичном дереве. В настоящее время определение напоминает определение Conat в stdlib. 

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 → 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
-}

1 Ответ

4 голосов
/ 26 марта 2019

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

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

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

Я поместил код в автономную суть.

...