粘合剂下的单原子取代 [英] Monadic substitution under binders

问题描述

在下面的Agda代码中，我有一个基于de Bruijn索引的术语语言.我可以使用通常的de Bruijn索引方式定义术语的替换，使用重命名以允许替换在活页夹下进行.

In the following Agda code, I have a term language based on de Bruijn indices. I can define substitution over terms in the usual de Bruijn indices way, using renaming to allow the substitution to proceed under a binder.

module Temp where

data Type : Set where
   unit : Type
   _⇾_ : Type → Type → Type

-- A context is a snoc-list of types.
data Cxt : Set where
   ε : Cxt
   _∷_ : Cxt → Type → Cxt

-- Context membership.
data _∈_ (τ : Type) : Cxt → Set where
   here : ∀ {Γ} → τ ∈ Γ ∷ τ
   there : ∀ {Γ τ′} → τ ∈ Γ → τ ∈ Γ ∷ τ′
infix 3 _∈_

data Term (Γ : Cxt) : Type → Set where
   var : ∀ {τ} → τ ∈ Γ → Term Γ τ
   〈〉 : Term Γ unit
   fun : ∀ {τ₁ τ₂} → Term (Γ ∷ τ₁) τ₂ → Term Γ (τ₁ ⇾ τ₂)

-- A renaming from Γ to Γ′.
Ren : Cxt → Cxt → Set
Ren Γ Γ′ = ∀ {τ} → τ ∈ Γ → τ ∈ Γ′

extend′ : ∀ {Γ Γ′ τ′} → Ren Γ Γ′ → Ren (Γ ∷ τ′) (Γ′  ∷ τ′)
extend′ f here = here
extend′ f (there x) = there (f x)

-- Apply a renaming to a term.
_*′_ : ∀ {Γ Γ′ : Cxt} {τ} → Ren Γ Γ′ → Term Γ τ → Term Γ′ τ
f *′ var x = var (f x)
f *′ 〈〉 = 〈〉
f *′ fun e = fun (extend′ f *′ e)

-- A substitution from Γ to Γ′.
Sub : Cxt → Cxt → Set
Sub Γ Γ′ = ∀ {τ} → τ ∈ Γ → Term Γ′ τ

extend : ∀ {Γ Γ′ τ} → Sub Γ Γ′ → Sub (Γ ∷ τ) (Γ′ ∷ τ)
extend θ here = var here
extend θ (there x) = there *′ θ x

-- Apply a substitution to a term.
_*_ : ∀ {Γ Γ′ : Cxt} {τ} → Sub Γ Γ′ → Term Γ τ → Term Γ′ τ
θ * var x = θ x
θ * 〈〉 = 〈〉
θ * fun a = fun (extend θ * a)

我现在想做的是将Term的类型概括为一个多态变体，这样我就可以定义一个monadic 〉〉=操作并使用该操作表达替换.这是天真的尝试:

What I would like to do now is generalise the type of Term into a polymorphic variant, so that I can define a monadic 〉〉= operation and express substitution using that. Here's naive attempt:

data Term (A : Cxt → Type → Set) (Γ : Cxt) : Type → Set where
   var : ∀ {τ} → A Γ τ → Term A Γ τ
   〈〉 : Term A Γ unit
   fun : ∀ {τ₁ τ₂} → Term A (Γ ∷ τ₁) τ₂ → Term A Γ (τ₁ ⇾ τ₂)

Sub : (Cxt → Type → Set) → Cxt → Cxt → Set
Sub A Γ Γ′ = ∀ {τ} → A Γ τ → Term A Γ′ τ

extend : ∀ {A : Cxt → Type → Set} {Γ Γ′ τ} → Sub A Γ Γ′ → Sub A (Γ ∷ τ) (Γ′ ∷ τ)
extend θ = {!!}

_〉〉=_ : ∀ {A : Cxt → Type → Set} {Γ Γ′ : Cxt} {τ} → 
       Term A Γ τ → Sub A Γ Γ′ → Term A Γ′ τ
var x 〉〉= θ = θ x
〈〉 〉〉= θ = 〈〉
fun a 〉〉= θ = fun (a 〉〉= extend θ)

这里的问题是，我不再知道如何定义extend(它将替代物转移到更深的上下文中)，因为替代物是更抽象的野兽.

The problem here is that I no longer know how to define extend (which shifts a substitution into a deeper context), because a substitution is a more abstract beast.

根据伯纳迪(Bernardy)的论文免费名称和波伊拉德:

Here's something closer, based on the paper Names for Free by Bernardy and Pouillard:

module Temp2 where

open import Data.Unit

data _▹_ (A : Set) (V : Set) : Set where
   here : V → A ▹ V
   there : A → A ▹ V

data Term (A : Set) : Set where
   var : A → Term A
   〈〉 : Term A
   fun : Term (A ▹ ⊤) → Term A

Ren : Set → Set → Set
Ren Γ Γ′ = Γ → Γ′

extend′ : ∀ {Γ Γ′ V : Set} → Ren Γ Γ′ → Ren (Γ ▹ V) (Γ′ ▹ V)
extend′ f (here x) = here x
extend′ f (there x) = there (f x)

Sub : Set → Set → Set
Sub Γ Γ′ = Γ → Term Γ′

_<$>_ : ∀ {Γ Γ′ : Set} → Ren Γ Γ′ → Term Γ → Term Γ′
f <$> var x = var (f x)
f <$> 〈〉 = 〈〉
f <$> fun e = fun (extend′ f <$> e)

extend : ∀ {Γ Γ′ V : Set} → Sub Γ Γ′ → Sub (Γ ▹ V) (Γ′ ▹ V)
extend θ (here x) = var (here x)
extend θ (there x) = there <$> θ x

_〉〉=_ : ∀ {Γ Γ′ : Set} → Term Γ → Sub Γ Γ′ → Term Γ′
var x 〉〉= θ = θ x
〈〉 〉〉= θ = 〈〉
fun a 〉〉= θ = fun (a 〉〉= extend θ)

这里的想法是以明确抽象的方式对上下文扩展的想法进行建模，即使在多态环境中，也允许为重命名和替换定义extend.

The idea here is to model the idea of context extension in an explicitly abstract way, allowing extend to be defined for renamings and substitutions even in the polymorphic setting.

不幸的是，我似乎太愚蠢了，无法理解如何扩展这种方法，从而使术语由Type参数化，就像我在上面的第一次尝试中那样.我想以〉〉 ==结尾，(大约)具有以下类型:

Unfortunately, I seem to be too stupid to understand how to extend this approach so that terms are parameterised by a Type, as they are in my first attempt above. I would like to end up with 〉〉= having (approximately) the following type:

_〉〉=_ : ∀ {Γ Γ′ : Set} {τ} → Term Γ τ → (Sub Γ Γ′) → Term Γ′ τ

有人能指出我正确的方向吗?

Can anyone point me in the right direction?

推荐答案

类似下面的内容?重要的是如何表示变量.答案是，在类型设置中，变量需要按类型索引.如果您进行更改，那么或多或少都会发生...

Something like the following perhaps? The important thing is how you represent variables. The answer is that in a typed setting, variables need to be indexed by a type. If you make that change, everything more or less follows...

module Temp2 where

open import Data.Unit
open import Data.Empty
open import Relation.Binary.PropositionalEquality

data Type : Set where
   unit : Type
   _⟶_ : Type → Type → Type

data _▹_ (A : Type → Set) (V : Type → Set) (t : Type) : Set where
   here : V t → (A ▹ V) t
   there : A t → (A ▹ V) t

data Term (A : Type → Set) : Type → Set where
   var : ∀ {t} → A t → Term A t
   〈〉 : Term A unit
   fun : ∀ {t : Type} {T : Type} → Term (A ▹ (_≡_ T)) t → Term A (T ⟶ t)

Ren : (Type → Set) → (Type → Set) → Set
Ren Γ Γ′ = ∀ {t} → Γ t → Γ′ t

extend′ : ∀ {Γ Γ′ V : Type → Set} → Ren Γ Γ′ → Ren (Γ ▹ V) (Γ′ ▹ V)
extend′ f (here x) = here x
extend′ f (there x) = there (f x)

Sub : (Type → Set) → (Type → Set) → Set
Sub Γ Γ′ = ∀ {t} → Γ t → Term Γ′ t

_<$>_ : ∀ {Γ Γ′ : Type → Set} {t} → Ren Γ Γ′ → Term Γ t → Term Γ′ t
f <$> var x = var (f x)
f <$> 〈〉 = 〈〉
f <$> fun e = fun (extend′ f <$> e)

extend : ∀ {Γ Γ′ V : Type → Set} → Sub Γ Γ′ → Sub (Γ ▹ V) (Γ′ ▹ V)
extend θ (here x) = var (here x)
extend θ (there x) = there <$> θ x

_〉〉=_ : ∀ {Γ Γ′ : Type → Set} {t} → Term Γ t → Sub Γ Γ′ → Term Γ′ t
var x 〉〉= θ = θ x
〈〉 〉〉= θ = 〈〉
fun a 〉〉= θ = fun (a 〉〉= extend θ)

这篇关于粘合剂下的单原子取代的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！