Skip to content

README.md

Latest commit

 

History

History
81 lines (55 loc) · 6.02 KB

README.md

File metadata and controls

81 lines (55 loc) · 6.02 KB
Raw

Lambda Lifting in Lean

This project accompanies the paper "Simple Lambda Lifting: Formalisation in Lean and a new efficient algorithm". It contains machine-checked proofs for some of the theorems from the paper (formalised using the Lean 4 proof assistant) and an implementation of the algorithm described in the paper.

The full reference for the paper is:

Tom Levy and Steve Reeves. 2026. Simple Lambda Lifting: Formalisation in Lean and a new efficient algorithm. In IEEE/ACM 14th International Conference on Formal Methods in Software Engineering (FormaliSE '26), April 12–13, 2026, Rio de Janeiro, Brazil. ACM, New York, NY, USA, 12 pages. https://doi.org/10.1145/3793656.3793692

Background

Lambda lifting is a technique used in compilers to convert nested function definitions to top-level function definitions. It was introduced by Johnsson in [1], which describes an O(n³) algorithm. The basic idea is to eliminate references to free variables by inserting "extraneous parameters" and corresponding extraneous arguments.

Computing the necessary extraneous parameters is not trivial; further, we want to find the minimal required set for efficiency. A series of papers [2, 3, 4] has led to an O(n²) algorithm, however it is complex.

This project demonstrates a simple O(n²) algorithm for computing the minimal extraneous parameters. (More precisely, the time complexity of the algorithm is linear in the size of the lifted program, which is at most O(n²).)

A formal lambda lifting specification was given by Fischbach and Hannan in [5]. We formalise this specification in Lean 4, and use that to prove some properties and test our algorithm on generated test cases.

[1]: Thomas Johnsson. 1985. 🔒Lambda lifting: Transforming programs to recursive equations. In Functional Programming Languages and Computer Architecture. Springer Berlin Heidelberg.
[2]: Olivier Danvy and Ulrik P. Schultz. 2002. 🔒Lambda-lifting in quadratic time. In International Symposium on Functional and Logic Programming (pp. 134-151). Springer Berlin Heidelberg.
[3]: Marco T. Morazán and Barbara Mucha. 2006. Improved Graph-Based Lambda Lifting. In Software Engineering Research and Practice, SERP 2006 (pp. 896-902).
[4]: Marco T. Morazán and Ulrik P. Schultz. 2008. 🔒Optimal Lambda Lifting in Quadratic Time. In Implementation and Application of Functional Languages, IFL 2007 (pp. 37-56). Springer Berlin Heidelberg.
[5]: Adam Fischbach and John Hannan. 2003. Specification and correctness of lambda lifting. Journal of Functional Programming 13, 3 (2003), 509–543.

Building and running the project

The project requires Lean 4.31.0, which can be installed from https://lean-lang.org/install/. Alternatively, the project also includes a Dockerfile for use with Docker Engine; see the comments in that file for the commands to build the container.

Once Lean is installed, the project can be built using the standard Lean command lake build. If the build completes successfully, it means all the proofs were checked successfully.

The command lake exe lambdalifting can be used to test the algorithm on generated test cases. By default, only the algorithm from the paper and a version of Johnsson's algorithm are executed; the other implementations can be tested by uncommenting the relevant lines in Main.lean near the start of main.

The project contains some optional Haskell (.hs) source files in the "foreign" directory (described below). These files can be compiled using GHC, for example using the following command (using Docker for reproducibility and static linking for archival purposes):

docker run --rm -v ./foreign:/foreign haskell:9.14.1 \
  ghc -optl-static -no-keep-hi-files -no-keep-o-files foreign/johnsson.hs

Source code organisation

The source code is organised into three libraries, an executable, and some "foreign" (non-Lean) code:

  • "LambdaLifting" contains the bulk of the code.
  • "Examples" contains some small examples with manual proofs and examples from the literature.
  • "Figures" contains code from the figures in the paper (to check that the code compiles).
  • "Main.lean" is the source code for the executable "lambdalifting" which runs the generated examples.
  • "foreign" contains some implementations of algorithms from the literature, written in languages other than Lean. They can be tested from Lean by uncommenting the relevant lines in Main.lean as mentioned above.

The library "LambdaLifting" is organised into several modules:

  • "LeanUtil" contains general-purpose Lean utilities (such as a zip' function, assertions, and theorems about List and Vector).
  • "AssocListExtras" contains extensions to Lean's built-in type Lean.AssocList.
  • "Util" contains utilities specific to the project (such as AST transformations).
  • "Core" contains the abstract syntax tree (AST) and type system (from Fischbach–Hannan), and a type checking procedure.
  • "FischbachHannan" contains the translation of the Fischbach–Hannan specification, some basic theorems about it, and a (partial) decision procedure.
  • "Johnsson" contains a specification of "Johnsson-style" lifting, based on Johnsson's approach. The file "LambdaLifting/Johnsson/Theorems.lean" proves two key theorems: the sufficient conditions for Johnsson-style lifting, and that the Johnsson-style lifting specification satisfies the Fischbach–Hannan specification. Additionally, the file "LambdaLifting/Johnsson/Algorithm.lean" contains a Lean translation of Johnsson's algorithm.
  • "CompleteLifting" specifies the conditions for eliminating all non-local variable references (along with a decision procedure).
  • "Generate" generates valid programs for testing.
  • Finally, "Algorithm.lean" contains the implementation of Algorithm 1 from the paper "Simple Lambda Lifting".

SPDX-License-Identifier: MIT