This project aims to synthesize λ-join-calculus behaviors using the Z3 SMT solver.

The λ-calculus is a simple programming language. The λ-join-calculus extends the λ-calculus with a join operator with respect to the Scott ordering. Let's define a behavior as the equivalence class of programs modulo the coarsest sensible equivalence relation on programs, namely Hyland and Wadsworth's H* theory of observational equivalence, corresponding to Scott's D∞ models:

M ⊑ N iff ∀ context C[ ], C[M] converges ⇒ C[N] converges
M ≡ N iff ∀ context C[ ], C[M] converges ⇔ C[N] converges 

We'll leverage Scott's types-as-closures framework that naturally arises when extending the λ-calculus with join. Closures will allow us to branch on finitely or countably many inhabitants of a type.

Our synthesis approach is:

• Input a program sketch and a set of constraints.
• Explore a space of affine normal forms refining the sketch.
• Narrow down the space of programs by checking constraints, using Z3 to weakly check satisfiability.
• Within the feasible search space, use CEGIS (Counterexample-Guided Inductive Synthesis) to synthesize a chain of increasingly feasible programs.

Our first challenge problem is to synthesize a finitary definition for the simple type constructor

A = ⨆ { <r,s> | r ◦ s ⊑ I }

where ⊑ is the Scott ordering, ⨆ is the infinitary join operator, I is the identity function, ◦ is function composition, <r,s> = (λx. x r s) is a pair, and r and s range over closed λ-join-calculus terms.

• F* authors (20??) Profiling Z3 and Solving Proof Performance Issues (html|rst)
• Michał Moskal (2009) Programming with Triggers (pdf)
• Oskari Jyrkinen, Jonáš Fiala, et al. (2023) SMT Scope (code|webapp)
• Nils Becker, Peter Müller, and Alexander J. Summers (2019) The Axiom Profiler: Understanding and Debugging SMT Quantifier Instantiations (pdf)
• Nikolaj Bjørner, Leonardo de Moura, Lev Nachmanson, and Christoph Wintersteiger (20??) Programming Z3 (html)
• Nikolaj Bjørner et. al (20??) Z3 Internals (Draft) (html)
• Nikolaj Bjørner et. al (2021) Supercharging Plant Configurations using Z3 (html)
• Leonardo de Moura, Nikolaj Bjørner (2008) Z3: An Efficient SMT Solver (pdf)
• Z3 github issues (link)