How is the scope of the existential in `guard` wrong in our old version of V?

[rogerburtonpatel]

I'm not quite sure what's significant about the changes we made.

In my notes, we had for our old definition of guarded-exp:

```
guard ::= true
       |  ∃ x . guard
       |  x = exp; guard
```

In your note, you claim:

The proposal for $V$ won't work: the existential doesn't scope correctly. Let me suggest a new syntactic category:

```
guarded-exp ::= exp
             |  ∃ x . guarded-exp
             |  x = exp; guarded-exp
```

How is having exp instead of true, or reversing the order of the last two branches, a meaningful change to scope? Is there an important distinction between a guard and a guarded-exp?

[rogerburtonpatel]

After thinking on this more, I have an answer and a question.

Our old form of if ... fi with guard was

if-fi ::= if { [guard exp] } fi

With guarded-exp, we might be able to just say

if-fi ::= if { [guarded-exp] } fi

The question is, what does this evaluate to:

if exp fi

, i.e. our guarded-exp is just an exp; say, 3:

if 3 fi

This seems iffy. May be the complete wrong direction.

So, my question is: What does adding exp instead of true to guarded-exp buy us, and what happens when a guarded-exp is simply an exp in an if ... fi construct?

[nrnrnr]

What does adding exp instead of true to guarded-exp buy us?

Good question! Try translating (case n ([z z])) to V and see how far you get without it.

What happens when a guarded-exp is simply an exp in an if ... fi construct?

I'm going to let you work out the evaluation of the example you give. You can either desugar if ... fi into V and use the rules from the paper, or you can come up with direct evaluation rules for if ... fi. Direct rules will be useful, but if you find yourself stalled, just evaluate the desugaring.

[nrnrnr]

Addendum: a little concrete syntax might help here.

guarded-exp ::= ⟶ exp
             |  x = exp; guarded-exp
             |  ∃ x . guarded-exp

(And the order of the branches is insignificant.)

[rogerburtonpatel]

What does adding exp instead of true to guarded-exp buy us?

Good question! Try translating (case n ([z z])) to V and see how far you get without it.

What happens when a guarded-exp is simply an exp in an if ... fi construct?

I'm going to let you work out the evaluation of the example you give. You can either desugar if ... fi into V and use the rules from the paper, or you can come up with direct evaluation rules for if ... fi. Direct rules will be useful, but if you find yourself stalled, just evaluate the desugaring.

Just as well- from a closer look at the paper: There are no data constructors True and False; instead failure (returning zero values) plays the role of falsity.

[rogerburtonpatel]

Addendum: a little concrete syntax might help here.

guarded-exp ::= ⟶ exp
             |  x = exp; guarded-exp
             |  ∃ x . guarded-exp

(And the order of the branches is insignificant.)

I think I see! Is it that the first form by itself,⟶ exp, has an "empty condition" that always leads to the evaluation of an expression? And when placed with others:

∃ x . x = exp₁; ⟶ exp₂

we have a functional and readable equation form?

[rogerburtonpatel]

What does adding exp instead of true to guarded-exp buy us?

Good question! Try translating (case n ([z z])) to V and see how far you get without it.

I believe one can translate it as:

(case n ([z z])) ->

(if [exists z. n = z; true -> z] fi

This only uses the exists x. guard form and the x = exp; guard form, with no other exp needed. This lets us use the old

if-fi ::= if { [guard exp] } fi construct.

What am I missing?

[nrnrnr]

Addendum: a little concrete syntax might help here.

(And the order of the branches is insignificant.)

I think I see! Is it that the first form by itself,⟶ exp, has an "empty condition" that always leads to the evaluation of an expression?

Yes, that's the idea.

And when placed with others:

∃ x . x = exp₁; ⟶ exp₂

we have a functional and readable equation form?

You tell me :-)

[nrnrnr]

What does adding exp instead of true to guarded-exp buy us?

Good question! Try translating (case n ([z z])) to V and see how far you get without it.

I believe one can translate it as:

(case n ([z z])) ->

(if [exists z. n = z; true -> z] fi

This only uses the exists x. guard form and the x = exp; guard form, with no other exp needed. This lets us use the old

if-fi ::= if { [guard exp] } fi construct.

What am I missing?

You solved a problem other than the one I posed. The problem was to translate (case n ([z z])) to the old syntax—the one that does not have an exp in the base case.

[rogerburtonpatel]

What does adding exp instead of true to guarded-exp buy us?

Good question! Try translating (case n ([z z])) to V and see how far you get without it.

I believe one can translate it as: (case n ([z z])) -> (if [exists z. n = z; true -> z] fi This only uses the exists x. guard form and the x = exp; guard form, with no other exp needed. This lets us use the old if-fi ::= if { [guard exp] } fi construct. What am I missing?

You solved a problem other than the one I posed. The problem was to translate (case n ([z z])) to the old syntax—the one that does not have an exp in the base case.

Forgive me; I wasn't clear- I was attempting to translate to the old syntax. I'm failing to find the exp in the base case of the solution I gave.

Breaking down (if [exists z. n = z; true -> z] fi:

guard ::= true
       |  ∃ x . guard
       |  x = exp; guard

say this maps to

datatype guard = TRUE
       |  EXISTS of name * guard
       |  ASSIGN of name * exp * guard
with type name = string

and say our if-fi takes the form of

 IF_FI of (guard * exp) list

and with our exp having a NAME form:

datatype exp = 
...
| NAME of string
...

we have in our abstract syntax: IF_FI [(EXISTS ("z", ASSIGN ("z", NAME ("n"), TRUE)), NAME ("z"))]

Given this has no base exp case, which would be the case in the new proposed form (the only exps appear in the ASSIGN form or in the second position of the IF_FI)- what am I missing?

[nrnrnr]

Your new proposed form is isomorphic to IF_FI of guarded_exp list. But in the form you propose, in the ∃ x . guard form, the x scopes beyond the guard, which is unacceptably weird. By moving to the ∃ x . guarded-exp form (with corresponding changes elsewhere), we correct the scope of x to something sane and sensible.

[rogerburtonpatel]

I understand after our 10/19 meeting. Thank you!

For future Roger: In the true version, the existential scopes only over the guard, which is true, and it's not intuitive scope over the right-hand side (exp). Having a single guarded-exp form, with a single scope, is cleaner.