通过(一元)JOIN和FMAP进行终止检查替换 [英] Termination-checking substitution via (monadic) join and fmap

问题描述

我使用的是大小类型，并且有一个类型化术语的替换函数，该函数用于终止检查我是否直接给出定义，但如果我通过(一元)联接和FMAP将其分解，则不会。

{-# OPTIONS --sized-types #-}

module Subst where

   open import Size

要显示问题，只需有单位和就足够了。我的数据类型为Trie和Term，并且我在Term内部使用Term同域Term的TRIES，作为SUM消除形式的一部分。

   data Type : Set where
      𝟏 : Type
      _+_ : Type → Type → Type

   postulate Cxt : Set → Set

   -- Every value in the trie is typed in a context obtained by extending Γ.
   data Trie (A : Cxt Type → Set) : {ι : Size} → Type → Cxt Type → Set where
      〈〉 : ∀ {ι Γ} → A Γ → Trie A {↑ ι} 𝟏 Γ
     〔_,_〕 : ∀ {ι τ₁ τ₂ Γ} → 
              Trie A {ι} τ₁ Γ → Trie A {ι} τ₂ Γ → Trie A {↑ ι} (τ₁ + τ₂) Γ

   -- The elimination form for + types is a trie whose values are terms.
   data Term (A : Cxt Type → Type → Set) : {ι : Size} → 
             Cxt Type → Type → Set where
      var : ∀ {ι Γ τ} → A Γ τ → Term A {↑ ι} Γ τ
      inl : ∀ {ι Γ τ₁ τ₂} → Term A {ι} Γ τ₁ → Term A {↑ ι} Γ (τ₁ + τ₂)
      match_as_ : ∀ {ι Γ τ τ′} → Term A {ι} Γ τ → 
                  Trie (λ Γ → Term A {ι} Γ τ′) {ι} τ Γ  → Term A {↑ ι} Γ τ′

现在，如果我直接将替换定义为术语(相互与替换INTO尝试使用codomainTerm)，则定义终止-检查，即使没有大小索引。

   -- Define substitution directly.
   _*_ : ∀ {A Γ Γ′ τ} → (∀ {τ} → A Γ τ → Term A Γ′ τ) → Term A Γ τ → Term A Γ′ τ
   _*ᵀ_ : ∀ {A Γ Γ′ τ τ′} → (∀ {τ} → A Γ τ → Term A Γ′ τ) →
          Trie (λ Γ → Term A Γ τ) τ′ Γ → Trie (λ Γ → Term A Γ τ) τ′ Γ′

   θ * var x = θ x
   θ * inl e = inl (θ * e)
   θ * (match e as κ) = match (θ * e) as (θ *ᵀ κ)

   θ *ᵀ 〈〉 x = 〈〉 (θ * x)
   θ *ᵀ 〔 κ₁ , κ₂ 〕 = 〔 θ *ᵀ κ₁ , θ *ᵀ κ₂ 〕

然而，Trie和Term是函数式，所以自然希望用<$>(FMAP)和join来定义替换，后者将术语的一个项折叠成一个项。请注意，<$>及其对应的尝试是保持大小不变的，实际上，我们需要使用反映这一点的大小索引，以便AGDA满足它的终止。

   -- Size-preserving fmap.
   _<$>ᵀ_ : ∀ {ι 𝒂 τ Γ Γ′} {A B : Cxt Type → Set 𝒂} → 
            (A Γ → B Γ′) → Trie A {ι} τ Γ → Trie B {ι} τ Γ′
   f <$>ᵀ (〈〉 x) = 〈〉 (f x)
   f <$>ᵀ 〔 σ₁ , σ₂ 〕 = 〔 f <$>ᵀ σ₁ , f <$>ᵀ σ₂ 〕

   _<$>_ : ∀ {ι A B Γ Γ′ τ} → 
           (∀ {τ} → A Γ τ → B Γ′ τ) → Term A {ι} Γ τ → Term B {ι} Γ′ τ
   f <$> var x = var (f x)
   f <$> inl e = inl (f <$> e)
   f <$> match e as κ = match f <$> e as ((λ e → f <$> e) <$>ᵀ κ)

   -- Monadic multiplication.
   join : ∀ {A Γ τ} → Term (Term A) Γ τ → Term A Γ τ
   join (var e) = e
   join (inl e) = inl (join e)
   join (match e as κ) = match join e as (join <$>ᵀ κ)

   -- Now substitution is easily defined in terms of join and fmap.
   _*′_ : ∀ {A Γ Γ′ τ} → (∀ {τ} → A Γ τ → Term A Γ′ τ) → Term A Γ τ → Term A Γ′ τ
   θ *′ e = join (θ <$> e)

不幸的是join不进行终止检查，我不确定是否可以使用大小指数来说服AGDA相信它可以。直观地说，很明显，如果你有一棵最大深度为ι的树，并用最大深度为ι‘的树替换它的叶子，你就得到了一棵最大深度为(ι+ι’)的树。但我不认为这是一种你可以用大小的字体建立起来的东西，或者如果你可以的话，它是否会有帮助。请注意，在没有通过join <$>ᵀ相互递归到TRIES的情况下，函数终止检查正常。

有没有办法让这个相互递归版本的join终止检查，或者我坚持显式地编写替换？

推荐答案

赋予join以下类型：

join : ∀ {ι A Γ τ} → Term (Term A) {ι} Γ τ → Term A Γ τ

(摘自上述gallais' comment)。

这篇关于通过(一元)JOIN和FMAP进行终止检查替换的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！