Talk:Reformulating languages to use hypothetical judgements
From The Twelf Project
Thanks Dan, very useful.
Here's two other inductive properties of complete development:
First, ==> is not only deterministic, but total: for every M there is some X s.t. M ==> X.
Second, ==> completes any =>:
cd_pr_triangle: (M ==> N) -> (M => L) -> (L => N).
These two properties give an easy proof that => has the diamond property: put two of these triangles together along their ==> side.
Rpollack 17:04, 28 February 2008 (EST)
- Cool. I know there's a proof of CR in the Twelf examples directory, but I think it proves diamond for parallel reduction directly. If I get a chance, I'll Twelf these theorems up and then maybe turn this page into a case study instead of a tutorial. Drl 16:08, 3 March 2008 (EST)
- Done, but not commented yet: Church-Rosser via Complete Development.
Drl 10:34, 4 March 2008 (EST)
How about improving the rule ==>/beta to:
==>/beta : (app (lam M) N) ==> M' N'
<- (lam M) ==> (lam M')
<- N ==> N'.
This simplifies the proof of "sound" too.
Rpollack 15:34, 29 February 2008 (EST)
- Good idea---it makes sense to localize the binding here. I've seen situations where this move actually gives you less information (e.g., a typed beta-reduction rule in a calculus with a definitional equality rule---you can't invert the derivation of (lam M : A -> B) to get a hypothetical), but for this tutorial it makes sense. Drl 16:08, 3 March 2008 (EST)
- Actually, there's one downside to this reformulation: in the original version, Twelf can prove => total automatically, but in the new version, it gets tripped up by the inversion that if (lam M) => N then N is (lam N1). I changed the definition back because I want to let Twelf prove this totality for me in Church-Rosser via Complete Development, and I want the code here to stay synchronized with that. Drl 10:34, 4 March 2008 (EST)
