Processing math: 100%

Wednesday, December 21, 2016

Take 3: Application with Subsumption for Den. Semantics of Lambda Calculus

Alan Jeffrey tweeted the following in reply to the previous post:

@jeremysiek wouldn't it be easier to change the defn of application to be
⟦MN⟧σ = { W | T ∈ ⟦M⟧σ, V ∈ ⟦N⟧σ, (V′,W) ∈ T, V′ ⊆ V }?

The idea is that, for higher order functions, if the function M is expecting to ask all the questions in the table V, then it is OK to apply M to a table V that answers more questions than V. This idea is quite natural, it is like Liskov's subsumption principle but for functions instead of objects. If this change can help us with the self application problem, then it will be preferable to the graph-o-tables approach described in the previous post because it retains the simple inductive definition of values. So let's see where this takes us!

We have the original definition of values

valuesv::=n{(v1,v1),,(vn,vn)}

and here is the denotational semantics, updated with Alan's suggestion to include the clause v2v2 in the case for application.

E[|n|](ρ)={n}E[|x|](ρ)={ρ(x)}E[|λx.e|](ρ)={Tvv.(v,v)TvE[|e|](ρ(x:=v))}E[|e1e2|](ρ)={v|Tv2v2.TE[|e1|](ρ)v2E[|e2|](ρ)v2v2(v2,v)T}

The ordering on values used above is just equality on numbers and subset on function tables.

The first thing to check is whether this semantics can handle self application at all, such as (λf.ff)(λg.42)

Example 1. 42E[|(λf.ff)(λg.42)|]()
The main work is figuring out witnesses for the function tables. We're going to need the following tables: T0=T1={(,42)}T2={(T1,42)}

Here's the proof, working top-down, or goal driven. The important use of subsumption is the T1 below.

  • T2E[|(λf.ff)|]()
    So we need to show: 42E[|ff|](f:=T1)
    • T1E[|f|](f:=T1)
    • T1E[|f|](f:=T1)
    • T1
    • (,42)T1
  • T1E[|(λg.42)|]()
    So we need to show 42E[|42|](g:=), which is immediate.
  • T1T1
  • (T1,42)T2

Good, so this semantics can handle a simple use of self application. How about factorial? Instead of considering factorial of 3, as in the previous post, we'll go further this time and consider factorial of an arbitrary number n.

Example 2. We shall compute the factorial of n using the strict version of the Y combinator, that is, the Z combinator. Mλx.f(λv.(xx)v)Zλf.MMFλn.ifn=0then1elsen×r(n1)Hλr.FfactZH

We shall show that n!E[|factn|]()
For this example we need very many tables, but fortunately there are just a few patterns. To capture these patterns, be define the following table-producing functions. TF(n)={(n,n!)}TH(n)={(,TF(0)),(TF(0),TF(1)),,(TF(n1),TF(n))}TM(n)={if n=0{(TM(n),TF(n))}TM(n)if n=1+nTZ(n)={(TH(n),TF(n))}
TF(n) is a fragment of the factorial function, for the one input n. TH(n) maps each TF(i) to TF(i+1) for up to i+1=n. TM(n) is the heart of the matter, and what makes the self application work. It maps successively larger versions of itself to fragments of the factorial function, that is TM(n)={TM(0)TF(0)TM(1)TF(1)TM(n1)TF(n1)}
For example, here is TM(4):

The tables TM enable self application because we have the following two crucial properties:
  1. TM(n)TM(1+n)
  2. (TM(n),TF(n))TM(1+n)
The main lemma's that we prove are

Lemma 1. If nk, then TM(1+n)E[|M|](f:=TH(k)).

Lemma 2. TZ(n)E[|Z|]()

If you're curious about the details for the complete proof of n!E[|factn|]() you can take a look at the proof in Isabelle that I've written here.

This is all quite promising! Next we look at the proof of soundness with respect to the big step semantics.

Soundness with Respect to the Big-Step Semantics

The proof of soundness is quite similar to that of the first version, as the relation between the denotational and big-step values remains the same. However, the following two technical lemmas are needed to handle subsumption.

Lemma (Related Table Subsumption) If TT and Tλx.e,ρ, then Tλx.e,ρ.
The proof is by induction on T.

Lemma (Related Value Subsumption) If v1v and v2v, then v2v.
The proof is by case analysis, using the previous lemma when the values are function tables.

Theorem (Soundness).
If vE[|e|](ρ) and ρρ, then ρev and vv for some v.

The mechanization of soundness in Isabelle is here.

No comments:

Post a Comment