Lambda-lifting and lambda-dropping

In a lambda-lifted program, all functions are defined at the toplevel. For example, consider the following definition of the addition function:

Fixpoint add_lifted (n1 n2 : nat) : nat :=
  match n1 with
    O =>
    n2
  | S n1' =>
    S (add_lifted n1' n2)
  end.

• add_lifted is defined globally;
• add_lifted is defined recursively over its first argument; and
• the second argument of add_lifted is only used in the base case.

In contrast, a lambda-dropped program has a block structure and local definitions, and it actively uses lexical scope:

Definition add_dropped (n1 n2 : nat) : nat :=
  let fix visit i :=
    match i with
      O =>
      n2
    | S i' =>
      S (visit i')
    end
  in visit n1.

• add_dropped is defined globally;
• add_dropped is not defined recursively;
• visit is defined recursively in a local block; and
• in this local block, n2 is free, since it is declared outside this block, as a formal parameter of add_dropped.

Lambda-lifted programs and lambda-lifted proofs

We only have considered lambda-lifted programs so far. Accordingly, all our theorems and lemmas are defined at the toplevel, which means that our proofs are lambda-lifted too.

Does it mean that we cannot reason about lambda-dropped programs? The answer to this rhetorical question is no.

Lambda-dropped programs and lambda-dropped proofs

In the first accompanying file, the equivalence of add_lifted and of add_dropped is proved. The two fold-unfold lemmas corresponding to add_lifted are declared globally, and the two fold-unfold lemmas corresponding to visit are declared locally. The rest of the proof is a routine induction over n1.

In the second accompanying file, two main functions are implemented with a local auxiliary recursive function. Reasoning about these main functions entails declaring local auxiliary lemmas to reason about their local auxiliary function. Due to their locality, these auxiliary lemmas are duplicated in other proofs. In contrast, these auxiliary lemmas are shared when reasoning about lambda-lifted programs, just as identical local auxiliary functions in a lambda-dropped program are shared once this program is lambda-lifted.

Conclusion

In the rest of the semester, we will continue to only consider lambda-lifted programs.

Resources

• The .v file with the equivalence of add_lifted and add_dropped (latest version: 20 Aug 2024).
• The .v file for reasoning about lambda-dropped functions (latest version: 16 Feb 2024).
• Section 8 of the tutorial about fold-unfold lemmas.

Version

Factored out of another chapter and fleshed out [20 Aug 2024]