代表头部正常lambda演算AST中的固定点

Question

考虑在类型检查期间获得的以下标准化术语表示:

data Normal a
  = Neutral (Neutral a)
  | Type
  | Pi (Normal a) (Normal (Maybe a))
  | Abstract (Normal (Maybe a))

data Neutral a
  = Variable a
  | Apply (Neutral a) (Normal a)

我希望能够在此框架中表示一个修复点,或者至少以保留其head-normal属性的方式,这对于实现替换和定义相等非常方便.

起初,我想过使用微积分本身定义的固定点组合子.但是,Y组合器是不可能的,因为这个术语表示我不能将lambda应用于lambda.Z组合器接近我想要的,但假设结果是一个函数.

如果我只是简单地进行图形缩减,我会将结与Haskell本身联系起来,导致一个懒惰的无限语法树.但是,由于这是用于依赖类型检查器,我需要能够在术语上测试定义相等 - 它会以这种方式陷入无限循环.