Ligical Framework minilf0

Scala の Dotty の研究のソースを読んでて気になるプログラムがあったのですが、何やってるのかさっぱり分からなかったのです。
どうも、凄そうなのでリファクタリングしまくって本質的な部分だけを取り出してみました。
どうも依存型をさらっとHOASのようなテクニックを使って実装してしまい、命題なども書けるようにしたもののようです。
よく分かっていないのですけど、変形してみたソースを以下に示します:

どうも、Logical Framework というもののようです。

package minilf0

object Test extends App {
  abstract sealed class LF
  case object Sort extends LF
  case class Var(c: LF, s: String) extends LF
  case class Forall(a: LF, f: LF=>LF) extends LF
  case class App(x: LF, y: LF) extends LF
  def show(t:LF,n:Int=0):String = t match {
    case Var(_,s)=>s
    case Forall(a,f)=>val x = Var(a,('A'+n).toChar.toString)
                      "{"+show(x,n+1)+":"+show(ty(x),n+1)+"}"+show(f(x),n+1)
    case App(x,y)=>"("+show(x,n)+" "+show(y,n)+")"
    case Sort => "sort"
  }
  def ty(t:LF):LF = t match {
    case Var(c,_)=>c
    case Forall(a,f)=>Forall(a, u=>ty(f(u)))
    case App(x,y)=>ap(ty(x),y)
    case Sort => Sort
  }
  def ap(t:LF,x:LF):LF = t match {
    case Forall(a,f)=> f(x)
    case _=>App(t,x)
  }
  def inst(t:LF, s:String): LF = t match {
    case Forall(a,f)=> Forall(a, u=>inst(f(u),"("+s+" "+show(u)+")"))
    case t=>Var(t,s)
  }

  /* ペアノ自然数の例 */
  /*
    typ : sort ::= nat
    nat : typ ::= z | s nat

    -------------- (t-z)
    z : nat

    n : nat
    -------------- (t-s)
    s n : nat
  */
  val typ = inst(Sort,"typ")
  val nat = inst(typ, "nat")
  println("nat = "+show(nat))
  val z = inst(nat,"z")
  val s = inst(Forall(nat,{N=>nat}),"s")

  println("s = "+show(s))

  println(show(ap(s,z)) + " : " + show(ty(ap(s,z))))

  println("---")

  /*
  lte : nat -> nat -> typ

  a: nat
  --------------- (lte-z)
  lte z a

  n1:nat   n2:nat
  lte n1 n2
  ----------------- (lte-s)
  lte (s n1) (s n2)
  */
  val lte = inst(Forall(nat,{A=>Forall(nat,{B=>typ})}),"lte") 

  println("lte   = " + show(lte) + " : " + show(ty(lte)))

  val lte_z = inst(Forall(nat,{A=>ap(ap(lte,z),A)}),"lte-z")
  println("lte_z = " + show(lte_z))
  val lte_s = inst(Forall(nat,{N1=>Forall(nat,{N2=>
                  Forall(ap(ap(lte,N1),N2),{
                    LTE=>ap(ap(lte,ap(s,N1)),ap(s,N2))
                  })
              })}),"lte-s")
  println("lte_s = " + show(lte_s))
  println("---")
  /*
    lte_refl : ∀(n:nat) lte n n

    ---------------------- (lte-refl-z)
    lte_refl z (lte_z z)

    n:nat  lte1:lte n n
    sub:lte_s n n lte1
    ---------------------- (lte-refl-s)
    lte_refl (s n) sub

  */
  val lte_refl = inst(Forall(nat,{n=>
                   Forall(ap(ap(lte,n),n),{lte=>typ})
                 }), "lte-refl")

  val lte_refl_z = inst(ap(ap(lte_refl,z),ap(lte_z,z)),"lte-refl-z")
  val lte_refl_s = inst(Forall(nat,{n=>
    Forall(ap(ap(lte,n),n),{lte1=>
      val sub = ap(ap(ap(lte_s,n),n),lte1)
      ap(ap(lte_refl,ap(s,n)),sub) 
    })
  }),"lte-refl-s")

  println("lte_refl   = "+show(lte_refl))
  println("lte_refl_z = "+show(lte_refl_z))
  println("lte_refl_s = "+show(lte_refl_s))
  println("---")

  println("lte_z z = " + show(ap(lte_z,z)))
  println("lte_z z : " + show(ty(ap(lte_z,z))))
  println("lte     = " + show(lte))
  println("lte z z = " + show(ap(ap(lte,z),z)))

  println("---")

  /* 部分型 */
  /*
    typ : sort ::= typ
    tpe : typ ::= int | bool | top | bot | arrow tpe tpe

    sub_tp : tpe -> tpe -> typ

    ---------------- (sub-tp-int)
    sub_tp int int

    ---------------- (sub-tp-bool)
    sub_tp bool bool

    t: tpe
    ---------------- (sub-tp-top)
    sub_tp t top

    t: tpe
    ---------------- (sub-tp-bot)
    sub_tp bot t

    t1:tpe   t2:tpe   t3:tpe   t4:tpe
    subtp t3 t1            subtp t2 t4
    ---------------------------------- (sub-tp-arrow)
    sub_tp (arrow t1 t2) (arrow t3 t4)

  */
  val tpe    = inst(typ,"tpe")

  val int    = inst(tpe,"int")
  val bool   = inst(tpe,"bool")
  val top    = inst(tpe,"top")
  val bot    = inst(tpe,"bot")
  val arrow  = inst(Forall(tpe,{T1=>Forall(tpe,{T2=>tpe})}),"arrow")

  val sub_tp        = inst(Forall(tpe,{T1=>Forall(tpe,{T2=>typ})}),"sub-tp")

  val sub_tp_int    = inst(ap(ap(sub_tp,int),int),"sub-tp-int")
  val sub_tp_bool   = inst(ap(ap(sub_tp,bool),bool),"sub-tp-bool")
  val sub_tp_top    = inst(Forall(tpe,{T=>ap(ap(sub_tp,T),top)}),"sub-tp-top")
  val sub_tp_bot    = inst(Forall(tpe,{T=>ap(ap(sub_tp,bot),T)}),"sub-tp-bot")
  val sub_tp_arrow  =
    Forall(tpe,{T1=>Forall(tpe,{T2=>Forall(tpe,{T3=>Forall(tpe,{T4=> 
      Forall(ap(ap(sub_tp,T3),T1),{ST31=>
        Forall(ap(ap(sub_tp,T2),T4),{ST24=>
          ap(ap(sub_tp,ap(ap(arrow,T1),T2)),ap(ap(arrow,T3),T4))
        })
      })
    })})})})
}