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,v′1),…,(vn,v′n)}and here is the denotational semantics, updated with Alan's suggestion to include the clause v′2⊑v2 in the case for application.
E[|n|](ρ)={n}E[|x|](ρ)={ρ(x)}E[|λx.e|](ρ)={T∣∀vv′.(v,v′)∈T⇒v′∈E[|e|](ρ(x:=v))}E[|e1e2|](ρ)={v|∃Tv2v′2.T∈E[|e1|](ρ)∧v2∈E[|e2|](ρ)∧v′2⊑v2∧(v′2,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. 42∈E[|(λ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)}
- T2∈E[|(λf.ff)|](∅)
So we need to show: 42∈E[|ff|](f:=T1)- T1∈E[|f|](f:=T1)
- T1∈E[|f|](f:=T1)
- ∅⊑T1
- (∅,42)∈T1
- T1∈E[|(λg.42)|](∅)
So we need to show 42∈E[|42|](g:=∅), which is immediate. - T1⊑T1
- (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(n−1)H≡λr.Ffact≡ZH
- TM(n)⊑TM(1+n)
- (TM(n),TF(n))∈TM(1+n)
Lemma 1. If n≤k, 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 T′⊆T and T≈⟨λx.e,ρ⟩,
then T′≈⟨λx.e,ρ⟩.
The proof is by induction on T′.
Lemma (Related Value Subsumption)
If v1≈v′ and v2⊑v′, then v2≈v′.
The proof is by case analysis, using the previous lemma when the
values are function tables.
Theorem (Soundness).
If v∈E[|e|](ρ) and ρ≈ρ′,
then ρ′⊢e⇓v′
and v≈v′ for some v′.
The mechanization of soundness in Isabelle is here.
No comments:
Post a Comment