关于G-集合的指数半环命名及相关G-类型系统构造的技术咨询

嘿，我来聊聊你问的这个问题——有没有专门的名字来称呼G-集合构成的指数半环？结合你提到的G-类型系统类比，我整理了相关的思路和构造细节：

核心问题：G-集合的指数半环命名 #

其实这个构造并没有像Burnside环那样有一个完全标准化的单一名称，在代数和类型论文献里，它通常被描述为带指数结构的G-集合半环，或者更精确地说，是Burnside半环的指数扩张。因为它本质上是在经典Burnside半环（仅包含有限G-集合的直和与积）的基础上，添加了指数对象（也就是函数空间）后得到的结构。

G-类型系统与Burnside半环的对应关系 #

你提到的普通类型系统和集合的类比，完全可以自然推广到带群作用的场景：

• 普通类型对应集合，而G-类型对应带有G群作用的集合（G-集合），且群作用要兼容所有类型构造器（+、×、→等）。
• Burnside半环本身就很像一个只有积（×）和余积（+）的简单类型系统：
  • 不可约传递G-集合（也就是G的有限传递作用）类比于“原始类型”，它们是构成所有G-类型的基础单元。
  • 余积（+）的构造：A+B = { (S^+, 1, a, (A, B)) : a ∈ A } ∪ { (S^+, 2, b, (A, B)) : b ∈ B }，群作用直接作用在底层元素上：
    $$g \triangleright (S^+, 1, a, (A, B))) = (S^+, 1, g \triangleright a, (A, B))$$
    $$g \triangleright (S^+, 2, b, (A, B)) = (S^+, 2, g \triangleright b, (A, B))$$
  • 积（×）的构造：A × B = { (S^×, a, b, (A, B)) : a ∈ A ∧ b ∈ B }，群作用同样逐元素作用：
    $$ g \triangleright (S^\times, a, b, (A, B)) = (S^\times, g \triangleright a, g \triangleright b, (A, B)) $$

添加指数构造器：扩展为带函数类型的G-类型系统 #

要得到类似简单类型λ演算的结构，只需要添加指数类型A → B（即从A到B的函数空间）。这里的群作用定义需要注意函数的共轭性质：

• 函数空间的群作用定义：g ▷ (S^→, { ⋯ (a, b) ⋯ }, (A, B)) = (S^→, { ⋯ (g ▷ a, g⁻¹ ▷ b) ⋯ }, (A, B))
• 用λ表达式来写更直观：g ▷ λx. f(x) = λx. g ▷ f(g⁻¹ ▷ x)

验证这个定义的合理性 #

我们可以通过两种等价的函数形式来验证这个定义的一致性：

1. 对于f : A × B → C：
   $$
   g \triangleright (f : A \times B \to C) \
   = g \triangleright (\lambda (a, b). c(a, b)) \
   = \lambda (a, b). g \triangleright c(g^{-1} \triangleright a, g^{-1} \triangleright b)
   $$
2. 对于柯里化后的h : A → B → C：
   $$
   g \triangleright ( h : A \to B \to C ) \
   = g \triangleright (\lambda a. \lambda b. c(a, b)) \
   = \lambda a. g \triangleright (\lambda b. c(g^{-1} \triangleright a, b)) \
   = \lambda a. \lambda b. g \triangleright c(g^{-1} \triangleright a, g^{-1} \triangleright b)
   $$
   两种形式得到的结果完全一致，说明这个群作用的定义是兼容柯里化规则的。

另外，这个定义也能正确处理恒等函数：
$$
g \triangleright \text{id} \
= g \triangleright (\lambda x. x) \
= \lambda x. g \triangleright g^{-1} \triangleright x \
= \lambda x. x
$$

备注：内容来源于stack exchange，提问作者Greg Nisbet