POPL Tutorial/cps-problem2

Problem 2: Elimination of Administrative Redices

Rather than introducing the administrative redices of explicitly introducing and eliminating continuations (see POPL Tutorial/cps-problem), we can simply use the function from values to computations itself wherever we previously used a continuation. Therefore, the new definition of the CPS language is obtained by replacing all instances of ccont A with (cvalue A -> contra).

%sort tp %.
%term o tp %.
%term => %pi tp %-> tp %-> tp %.
%prec %right 3 => %.
%sort exp {_ tp} %.
%sort value {_ tp} %.
%term app %pi (exp (A => B)) %-> (exp A) %-> (exp B) %.
%term lam %pi (%pi (value A) %-> (exp B)) %-> (value (A => B)) %.
%term ret %pi (value A) %-> (exp A) %.
%block sourceb [A tp] {x value A}%.
%worlds (sourceb) (exp _) (value _) %.
%sort contra %.
%sort cvalue {_ tp} %.
%term capp %pi (cvalue (A => B)) %-> (cvalue A) %-> (%pi (cvalue B) %-> contra) %-> contra %.
%term clam
  %pi (%pi (cvalue A) %-> (%pi (cvalue B) %-> contra) %-> contra)
  %-> (cvalue (A => B)) %.
%block targetb1 [A tp] {x cvalue A}%.
%block targetb2 [A tp] {y %pi (cvalue A) %-> contra}%.
%worlds (targetb1 targetb2) (contra) (cvalue _) %.

Notice that we no longer need terms for continuations as they are implicitly represented by the functions from values to contradictions.

For this problem, write the translation to this version of the CPS language:

%sort cps {_ value A} {_ cvalue A} %.
%mode cps %in %out %.
%sort cpse {_ exp A} {_ %pi (%pi (cvalue A) %-> contra) %-> contra} %.
%mode cpse %in %out %.

The code for this problem should be similar to the code from the previous problem except that the introduction of continuations with cfalsei and their elimination with throw is replaced by STELF function introduction and application.