haskell - 什么是从无类型术语及其 CC 类型中恢复 CC 术语的干净算法?
问题描述
假设我有一个未键入的术语,例如:
data Term = Lam Term | App Term Term | Var Int
-- λ succ . λ zero . succ zero
c1 = (Lam (Lam (App (Var 1) (Var 0)))
-- λ succ . λ zero . succ (succ zero)
c2 = (Lam (Lam (App (Var 1) (App (Var 1) (Var 0))))
-- λ succ . λ zero . succ (succ (succ zero))
c3 = (Lam (Lam (App (Var 1) (App (Var 1) (App (Var 1) (Var 0)))))
-- λ cons . λ nil . cons 1 (cons 2 (cons 3 nil))
term_untyped = (Lam (Lam (App (App (Var 1) c1) (App (App (Var 1) c2 (App (App (Var 1) c3) Nil)
及其CC类型:
data Type = Set | All Type Type | Var Int
-- ∀ (P : *) -> ∀ (Succ : P -> P) -> ∀ (Zero : P) -> P
nat = All(Set, All(All(Var(0), Var(1)), All(Var(0), Var(1))))
-- ∀ (P : *) -> ∀ (Cons : x -> P -> P) -> ∀ (Nil : P) -> P
list x = All(Set, All(All(x, All(Var(0), Var(1))), All(Var(0), Var(0))))
-- term_type
term_type = list nat
是否有一种干净的算法可以恢复与未键入的项对应的 CC 项?IE,
data CCTerm
= Lam CCTerm CCTerm
| All CCTerm CCTerm
| App CCTerm CCTerm
| Set
| Var Int
term_typed :: Term -> CCTerm
term_typed = from_untyped term_type term_untyped
-- As the result, typed_term would be:
-- λ (P : *) ->
-- λ (Cons : ∀ (x : (∀ (Q : *) -> (Q -> Q) -> Q -> Q)) -> P -> P) ->
-- λ (Nil : P) ->
-- ( Cons (λ (Q : *) -> λ (Succ : Q -> Q) -> (Zero : Q) -> Succ Zero)
-- ( Cons (λ (Q : *) -> λ (Succ : Q -> Q) -> (Zero : Q) -> Succ (Succ Zero))
-- ( Cons (λ (Q : *) -> λ (Succ : Q -> Q) -> (Zero : Q) -> Succ (Succ (Succ Zero)))
-- Nil)))
我尝试了一些东西,但很快注意到如何传递类型并不明显。具体来说,Lam 案例似乎需要一个 forall 类型并将其附加到上下文中,App 案例的函数似乎产生了一个供参数使用的 forall 类型,而 Var 案例似乎在上下文中查询一个类型。这种不对称性使我的代码有点混乱,所以我想知道是否有明显的方法来实现它。
解决方案
您不能在输入中包含 beta redexes,因为您主要不能推断 lambdas 的类型,否则它只是标准的双向类型检查。如果知道输入的类型是正确的,那么您可以跳过转换检查。伪代码:
check : Term → Type → Cxt → CCTerm
check (λ x. t) ((x : A) → B) Γ = λ (x : A). check t B (Γ, x : A)
check t A Γ = fst (infer t Γ) -- no conv check
infer : Term → Cxt → (CCTerm, Type)
infer (λ x.t) Γ = undefined
infer x Γ = (x, lookup x Γ)
infer (t u) Γ = (t' u', B[x ↦ u'])
where (t', ((x : A) → B)) = infer t Γ
u' = check u A Γ
(将其转换为 de Bruijn 指数并可能更快地All
替换)。我觉得这有点奇怪,Star
并且All
不在 中Term
,但这些也可以微不足道地包含在其中infer
。
推荐阅读
- pyqt - pyqt - 单击 QTableWidget 标题以获得唯一列
- javascript - Javascript 减少到 PHP array_reduce
- r - 每组最后一行所需的rollsum结果
- matlab - 从 Matlab 2018 中的复选框获取值
- php - Ionic 应用 PHPSESSID 在 iOS 上的每个 HTTP 请求上都会发生变化,但在 android 上运行良好
- jenkins - 詹金斯自动部署
- visual-studio-code - VS Code:突出显示带有 SVN 扩展名的修改文件
- typescript - 尝试更新标记的联合时出现令人惊讶的类型错误
- javascript - 我只放了一个入口点,但是很多文件在 webpack 中编译
- octave - Octave - 带有 lsode 的微分方程组