通过trie终止检查功能

Question

我很难说服Agda终止检查fmap下面的函数,并且在a的结构上递归地定义了类似的函数Trie.A Trie是一个trie,其域是a Type,是一个由单元,产品和固定点组成的对象级类型(我省略了副产品以保持代码最小).问题似乎与我在定义中使用的类型级替换有关Trie.(表达式const (?? ?) * ?表示将替换const (?? ?)应用于类型?.)

module Temp where

   open import Data.Unit
   open import Category.Functor
   open import Function
   open import Level
   open import Relation.Binary

   -- A context is just a snoc-list.
   data Cxt {} (A : Set ) : Set  where
      ? : Cxt A
      _??_ : Cxt A ? A ? Cxt A

   -- Context membership.
   data _?_ {} {A : Set } (a : A) : Cxt A ? Set  where
      here : ? {?} ? a ? ? ?? a
      there : ? {? a?} ? a ? ? ? a ? ? ?? a?
   infix 3 _?_

   -- Well-formed types, using de Bruijn indices.
   data _? (? : Cxt ?) : Set where
      nat : ? ?
       : ? ?
      var : _ ? ? ? ? ?
      _+_ _?_ : ? ? ? ? ? ? ? ?
      ? : ? ?? _ ? ? ? ?
   infix 3 _?

   -- A closed type.
   Type : Set
   Type = ? ?

   -- Type-level substitutions and renamings.
   Sub Ren : Rel (Cxt ?) zero
   Sub ? ?? = _ ? ? ? ?? ?
   Ren ? ?? = ? {x} ? x ? ? ? x ? ??

   -- Renaming extension.
   extend? : ? {? ??} ? Ren ? ?? ? Ren (? ?? _) (?? ?? _)
   extend? ? here = here
   extend? ? (there x) = there (? x)

   -- Lift a type renaming to a type.
   _*?_ : ? {? ??} ? Ren ? ?? ? ? ? ? ?? ?
   _ *? nat = nat
   _ *?  = 
   ? *? (var x) = var (? x)
   ? *? (?? + ??) = (? *? ??) + (? *? ??)
   ? *? (?? ? ??) = (? *? ??) ? (? *? ??)
   ? *? (? ?) = ? (extend? ? *? ?)

   -- Substitution extension.
   extend : ? {? ??} ? Sub ? ?? ? Sub (? ?? _) (?? ?? _)
   extend ? here = var here
   extend ? (there x) = there *? (? x)

   -- Lift a type substitution to a type.
   _*_ : ? {? ??} ? Sub ? ?? ? ? ? ? ?? ?
   ? * nat = nat
   ? *  = 
   ? * var x = ? x
   ? * (?? + ??) = (? * ??) + (? * ??)
   ? * (?? ? ??) = (? * ??) ? (? * ??)
   ? * ? ? = ? (extend ? * ?)

   data Trie {} (A : Set ) : Type ? Set  where
      ?? : A ?  ? A
      ?_,_? : ? {?? ??} ? ?? ? A ? ?? ? A ? ?? + ?? ? A
      ?_ : ? {?? ??} ? ?? ? ?? ? A ? ?? ? ?? ? A
      roll : ? {?} ? (const (? ?) * ?) ? A ? ? ? ? A

   infixr 5 Trie
   syntax Trie A ? = ? ? A

   {-# NO_TERMINATION_CHECK #-}
   fmap : ? {a} {A B : Set a} {?} ? (A ? B) ? ? ? A ? ? ? B
   fmap f (?? x)    = ?? (f x)
   fmap f ? ?? , ?? ? = ? fmap f ?? , fmap f ?? ?
   fmap f (? ?)    = ? (fmap (fmap f) ?)
   fmap f (roll ?) = roll (fmap f ?)

fmap在每种情况下,似乎都会在一个极小的论点中进行处理; 当然,如果我删除递归类型,产品案例就没问题.另一方面,如果我删除产品,定义会处理递归类型.

在这里最简单的方法是什么？该内嵌/保险丝招看起来并不特别适用,但也许是.或者我应该寻找另一种方法来处理定义中的替换Trie？

Answer 1

内联/熔丝技巧可以(可能)以令人惊讶的方式应用.这个技巧适用于这类问题:

data Trie (A : Set) : Set where
  nil  :                     Trie A
  node : A ? List (Trie A) ? Trie A

map-trie : {A B : Set} ? (A ? B) ? Trie A ? Trie B
map-trie f nil = nil
map-trie f (node x xs) = node (f x) (map (map-trie f) xs)

此函数在结构上是递归的,但是以隐藏的方式.map只适用map-trie f于元素xs,因此map-trie应用于较小(子)尝试.但是Agda没有通过定义map来看它没有做任何时髦的事情.所以我们必须应用内联/保险丝技巧让它通过终止检查器:

map-trie : {A B : Set} ? (A ? B) ? Trie A ? Trie B
map-trie         f nil = nil
map-trie {A} {B} f (node x xs) = node (f x) (map? xs)
  where
  map? : List (Trie A) ? List (Trie B)
  map? [] = []
  map? (x ? xs) = map-trie f x ? map? xs

您的fmap函数共享相同的结构,您可以映射某种提升的函数.但是要内联什么？如果我们按照上面的例子,我们应该内联fmap.这看起来有点奇怪,但确实有效:

fmap fmap? : ? {a} {A B : Set a} {?} ? (A ? B) ? ? ? A ? ? ? B

fmap  f (?? x) = ?? (f x)
fmap  f ? ?? , ?? ? = ? fmap f ?? , fmap f ?? ?
fmap  f (? ?) = ? (fmap (fmap? f) ?)
fmap  f (roll ?) = roll (fmap f ?)

fmap? f (?? x) = ?? (f x)
fmap? f ? ?? , ?? ? = ? fmap? f ?? , fmap? f ?? ?
fmap? f (? ?) = ? (fmap? (fmap f) ?)
fmap? f (roll ?) = roll (fmap? f ?)

您可以应用另一种技术:它称为大小类型.您可以直接指定它,而不是依赖于编译器来确定somethig何时是结构递归.但是,您必须按类型索引数据类型Size,因此这种方法相当具有侵入性,无法应用于现有类型,但我认为值得一提.

在其最简单的形式中,大小类型表现为由自然数索引的类型.该索引指定结构大小的上限.您可以将其视为树高度的上限(假设数据类型是某个仿函数F的F分支树).大小版本的List外观几乎像一个Vec,例如:

data SizedList (A : Set) : ? ? Set where
  []  : ? {n} ? SizedList A n
  _?_ : ? {n} ? A ? SizedList A n ? SizedList A (suc n)

但是大小的类型添加了一些使它们更易于使用的功能.?当你不关心大小时,你有一个常数.suc被称为?和Agda实现的规则很少,例如? ? = ?.

让我们重写一下Trie使用大小类型的例子.我们需要在文件顶部的一个pragma和一个导入:

{-# OPTIONS --sized-types #-}
open import Size

这是修改后的数据类型:

data Trie (A : Set) : {i : Size} ? Set where
  nil  : ? {i}                         ? Trie A {? i}
  node : ? {i} ? A ? List (Trie A {i}) ? Trie A {? i}

如果您按map-trie原样保留该功能,终止检查程序仍会抱怨.那是因为当你没有指定任何大小时,Agda将填入无限(即无关值),我们回到了开头.

但是,我们可以标记map-trie为保持大小:

map-trie : ? {i A B} ? (A ? B) ? Trie A {i} ? Trie B {i}
map-trie f nil         = nil
map-trie f (node x xs) = node (f x) (map (map-trie f) xs)

所以,如果你给它一个Trie限制i,它也会给你另一个Trie限制i.所以map-trie永远不能做出Trie更大,只有同样大或更小.这足以让终止检查器弄清楚这map (map-trie f) xs没关系.

此技术也可以应用于您的Trie:

open import Size
  renaming (?_ to ^_)

data Trie {} (A : Set ) : {i : Size} ? Type ? Set  where
  ??    : ? {i} ? A ?
    Trie A {^ i} 
  ?_,_? : ? {i ?? ??} ? Trie A {i} ?? ? Trie A {i} ?? ?
    Trie A {^ i} (?? + ??)
  ?_    : ? {i ?? ??} ? Trie (Trie A {i} ??) {i} ?? ?
    Trie A {^ i} (?? ? ??)
  roll  : ? {i ?} ? Trie A {i} (const (? ?) * ?) ?
    Trie A {^ i} (? ?)

infixr 5 Trie
syntax Trie A ? = ? ? A

fmap : ? {i } {A B : Set } {?} ? (A ? B) ? Trie A {i} ? ? Trie B {i} ?
fmap f (?? x) = ?? (f x)
fmap f ? ?? , ?? ? = ? fmap f ?? , fmap f ?? ?
fmap f (? ?) = ? fmap (fmap f) ?
fmap f (roll ?) = roll (fmap f ?)