HOAS と PHOAS

基本的に，λ計算を証明支援系上で形式化するのはなかなか面倒な作業になるのですが，今回は Polymorphic Higher-Order Abstract Syntax (PHOAS) を使って形式化します．

PHOAS とは HOAS の Polymorphic 版，という意味なのですが，まず HOAS とは何かというと，λ計算を以下のデータ型のようにエンコードするやり方です．

(* HOAS流のλ項．Rocq(Coq)では不正な定義． *)
Inductive term :=
| Abs : (term -> term) -> term
| App : term -> term -> term.

たとえば，λx. (λy. y) x は Abs (fun x => App (Abs (fun y => y)) x) のように書けます．
λ抽象をRocq内部のλ抽象を使って書くので，代入を定義したいときは単にRocqの関数適用を使えばよいなど，便利になります．

しかし，コード上のコメントに書いたように，上記の term の定義はRocqのpositivity conditionをみたさないため，残念ながらRocqではエラーになります．

そこでPHOASでは代わりに次のような定義を考えます．以下はRocqでエラーにならずちゃんと定義できます．

(* PHOAS流のλ項 *)
Inductive term var :=
| Var : var -> term var
| Abs : (var -> term var) -> term var
| App : term var -> term var -> term var.

Definition Term := forall var, term var.

今回の term は型引数として var という型を取ります．
その var を全称量化子で閉じたものを Term 型としています．

たとえば，先ほどの例 λx. (λy. y) x は今回は

fun var => Abs (fun x => App (Abs (fun y => Var y)) (Var x))

と書きます．

ではさらに，このλ項の定義を型付きλ項に拡張してみます．まず型を以下のように定義します．

Inductive type :=
| Nat : type
| Unit : type
| Func : type -> type -> type.

基礎型はUnit型とNat型のみにしました．
型付きλ項を定義する際，一般にはλ項はまず型なしで定義して後から型付け関係を導入するやり方もありますが，今回はRocqの依存型の力を使って，「t 型のλ項」をいっぺんに定義します．

Inductive term (var : type -> Type) : type -> Type :=
| ConstN : nat -> term var Nat 
| Tt : term var Unit
| Succ : term var Nat -> term var Nat
| Var : forall t, var t -> term var t
| Abs : forall dom ran, (var dom -> term var ran) -> term var (Func dom ran)
| App : forall dom ran, term var (Func dom ran) -> term var dom -> term var ran.

Definition Term t := forall var, term var t.

Unit型とNat型に値を持たせるためにコンストラクタに ConstN と Tt を追加してみたり，自然数上の Succ というオペレータを追加してみました．
また，今度の term の引数 var は type -> Type という関数型になりました．var t が「型 t の変数」を表す想定です．Term t が「型 t をもつ項」全体の型です．
型付きになったことにより少し複雑になりましたが，上記でwell-typedな項がいっぺんに定義できるのがPHOASの強みです．

では，この Term として定義されたλ項に対し，Rocq内部のλ項としての表示的意味論を与えます．
まずtypeのRocqの型への埋め込みを考えます．

Fixpoint typeDenote (t : type) : Type :=
  match t with
  | Nat => nat
  | Unit => unit
  | Func t1 t2 => typeDenote t1 -> typeDenote t2
  end.

これを使ってλ項の意味論を定義します．

Fixpoint termDenote (e : term typeDenote t) : typeDenote t :=
  match e with
  | ConstN n => n
  | Tt _ => tt
  | Succ e => S (termDenote e)
  | Var x => x
  | Abs f => fun x => termDenote (f x)
  | App e1 e2 => termDenote e1 (termDenote e2)
  end.

Definition TermDenote (E : Term t) := termDenote (E typeDenote).

たとえば termDenote (App (Abs (fun x => Succ (Var x))) (ConstN 1)) は 2 に簡約することが確かめられます．

shift/reset への拡張

この定義をさらにshift/resetに拡張してみます．コード全体をここに置きます．

shift/resetを含む体系では，項はそれ自身の型以外に answer type (現在のコンテクストの型)の情報を持つようになります．よって type の定義を以下のように変えます．

Inductive type : Type :=
| Nat : type
| Unit : type
| Func : type -> type -> type -> type -> type.

Func t s a b で answer type 付きの関数型 t / a -> s / b を表します．わかりやすいように Notation を使いましょう．

Notation "t / a --> s / b" := (Func t s a b) (at level 40, a at next level, s at next level).

項の定義は以下になります．

Inductive value (var : type -> Type) : type -> Type :=
| Var : forall t, var t -> value var t
| ConstN : nat -> value var Nat
| Tt : value var Unit
| Abs : forall dom ran a b, (var dom -> term var ran a b) -> value var (Func dom ran a b)
with term (var : type -> Type) : type -> type -> type -> Type :=
| Val : forall t a, value var t -> term var t a a
| Succ : forall a b, term var Nat a b ->  term var Nat a b
| App : forall dom ran a b c d, term var (dom / a --> ran / b) c d -> term var dom b c -> term var ran a d
| Shift : forall t a b c x, (var (t / x --> a / x) -> term var c c b) -> term var t a b
| Reset : forall c t a, term var c c t -> term var t a a.

Definition Value t := forall var, value var t.
Definition Term t a b := forall var, term var t a b.

まず，今回は変数，定数，λ抽象は value として term とは分けた型の要素としています．
Term t a b は，型 t を持つ項で，answer type を a から b へ変化させるようなものからなる型です．

こうやって定義した項に対して，shift/resetを持たない言語へのCPS変換を与えます．CPS変換はこの論文の定義に則ります．
まず，ターゲット言語の定義は以下のようにします．

Inductive ttype : Type :=
| TNat : ttype
| TUnit : ttype
| TFunc : ttype -> ttype -> ttype.

Inductive tterm (var : ttype -> Type) : ttype -> Type :=
| TConstN : nat -> tterm var TNat
| TTt : tterm var TUnit
| TSucc : tterm var TNat -> tterm var TNat
| TVar : forall t, var t -> tterm var t
| TAbs : forall dom ran, (var dom -> tterm var ran) -> tterm var (TFunc dom ran)
| TApp : forall dom ran, tterm var (TFunc dom ran) -> tterm var dom -> tterm var ran
| TLet : forall t1 t2, tterm var t1 -> (var t1 -> tterm var t2) -> tterm var t2.

Notation "a --> b" := (TFunc a b) (at level 40).

Notation "'λ' x ==> e" := (TAbs (fun x => e)) (at level 30).

Notation "x @@ y" := (TApp x y) (at level 29).

Notation "'tlet' x :== e1 'in' e2" := (TLet e2 (fun x => e1)) (at level 35).

前の節で定義した term とほとんど同じですが，以降の簡単のために let 式を入れました．
また，読みやすさのために関数型 Func a b は a --> b，λ抽象 Abs (fun x => e) は λ x ==> e，関数適用 App x y は x @@ y，let式 TLet e2 (fun x => e1) は tlet x :== e1 in e2 と書けるようにしています．

この上でCPS変換を上記論文に則ってそのまま定義します．

(** CPS translation *)
Fixpoint cps_type (t : type) : ttype :=
  match t with
  | Nat => TNat
  | Unit => TUnit
  | a / c --> b / d => cps_type a --> ((cps_type b --> cps_type c) --> cps_type d)
  end.
  
Fixpoint cps_value var t (v : value (fun s => var (cps_type s)) t) : tterm var (cps_type t) :=
  match v with
  | Var x => TVar x
  | ConstN n => TConstN n
  | Tt => TTt _
  | Abs f => TAbs (fun x => cps_term _ (f x))
  end
with cps_term var t a b (e : term (fun s => var (cps_type s)) t a b)
  : tterm var ((cps_type t --> cps_type a) --> cps_type b) :=
       match e with
       | Val v =>  (λ k ==> TVar k @@ cps_value _ v)
       | Succ e' =>
           (λ k ==> cps_term _ e' @@ (λ n ==> TVar k @@ TSucc (TVar n)))
       | App e1 e2 =>
           (λ k ==>
              cps_term _ e1 @@
              (λ m ==>
                 cps_term _ e2 @@
                 (λ n ==> (TVar m @@ TVar n) @@ TVar k)))
       | Shift _ _ f =>
           (λ k ==>
              tlet k'' :== cps_term _ (f k'') @@ (λ m ==> TVar m) in
             ((λ n ==> (λ k' ==> TVar k' @@ (TVar k @@ TVar n)))))
       | Reset _ e =>
           TAbs (fun k => TApp (TVar k) (TApp (cps_term _ e) (TAbs (fun m => TVar m))))
       end.

Definition CPS_Term t a b (e : Term t a b) :
  TTerm ((cps_type t --> cps_type a) --> cps_type b) :=
  fun var => cps_term var (e _).

この関数は複雑なので読まなくてもいいですが，大事なのはソース言語の Term t a b が CPS 変換によってターゲット言語の TTerm ((cps_type t --> cps_type a) --> cps_type b) と型を保存して定義できていることです．
PHOASを使って，CPS変換が型を保存することが自動的に示されたわけです．

いくつか具体例を見てみます．
まず，ソース言語のλ抽象と関数適用にも Notation を導入し，λs x : t ==> e や x @ y のように書けるようにします．

Notation "'λs' x : t ==> e" := (Abs (fun (x:t) => e)) (at level 30, x at next level).

Notation "x @ y" := (App x y) (at level 29).

たとえば Shift k. (λ(_ : Unit). k 0) という(ソース言語の)項は以下のように書けます．

Example foo A B : Term _ _ _ :=
  fun (var : type -> Type) =>
    Shift A B (fun k => Val (λs _ : var Unit ==> Val (Var k) @ Val (ConstN 0))).
    
Check foo.
(*
 foo : forall A B : type, Term Nat A (Unit / B --> A / B)
*)

Checkコマンドで示したRocqの型推論の結果(コメントの中)が想定するものと合っていることを確かめます．
k の返り値の型を A とすると，まず，k 0 (コードでは Val (Var k) @ (Val (ConstN 0)))の部分は answer type を変化させないため，任意の B で Term A B B 型を持つはずです．
それに λ(_ : Unit) を付けた λ(_ : Unit). k 0 は Value (Unit / B --> A / B) になり，
さらにそれに Shift k を付けた全体の項は answer type を A から Unit / B --> A / B に変化させるため，Term Nat A (Unit / B --> A / B) と正しく型が推論されていることが分かります．

この foo を使って Reset (Succ foo) という項を考えます．つまり，全体では Reset (Succ (Shift k. (λ(_ : Unit). k 0)) です．

Example bar B C : Term _ _ _ :=
  fun (var : type -> Type) =>
    Reset C (Succ (foo _ B var)).
Check bar.
(*
  bar : forall B C : type, Term (Unit / B --> Nat / B) C C
 *)

この bar を B := Unit, C := Unit とした上でCPS変換してみます．

Example bar' B C := CPS_Term (bar B C).

Eval compute in (TTermDenote (bar' Unit Unit)).
(*
     = fun x : (unit -> (nat -> unit) -> unit) -> unit =>
       x (fun (_ : unit) (x0 : nat -> unit) => x0 1)
*)

TTermDenote は前の節と同様に定義した表示的意味論です．CPS変換した結果がちゃんとRocqのλ項として出てきました．

おわりに

PHOASを用いてshift/resetを含むλ計算のCPS変換をRocqで実装してみました．明示的には何も証明していませんが，PHOASを使ったことにより，CPS変換が型を保存することが自動的に示されました．
実はこのコードを書いたのは結構前なのですが，(answer typeなど何も知らない状態から始めて)コードを書くのにかかった時間は数時間程度です．

ソース言語のほうの簡約規則もRocqで定義しようかと思ったのですが，PHOASでやろうとするとコンテクストも型付きになることになり，面倒そうだったので今はやっていません．
型システムの性質の形式証明を楽にやる方法を探りたいものです．