Dang. Stuff from yesterday led down a path that made me think I had a very tidy answer to the age-old question of "read-only access"/"contingent-access" problem. Here's a post from last year and here's one from several years ago. Today's idea didn't pan out either.

The thought was to try to define the ternary P [c]⊸ N ("P implies N if c is in the context right now") by staring at the translation clause
(P ⊸ N) @ f = ∃αφ.(f = α⊸φ) ⊗ (P @ α) ⊗ (N @ φ)
and modify it to be
(P [c]⊸ N) @ f = ∃αβφ.(f = α⊸β⊸φ) ⊗ (P @ α) ⊗ (c @ β) ⊗ (N @ β ⊸ φ)
But then if you try to prove that focusing holds, you come to a case like ↓(P [c]⊸ ↑↓N) and you can't contort

(↓(P [c]⊸ ↑↓N)) @ r = ∀θ.(P [c]⊸ ↑↓N) @ θ ⇒ (r ▷ θ)
= ∀θ.(∃αβφ.(θ = α⊸β⊸φ) ⊗ (P @ α) ⊗ (c @ β) ⊗ (↑↓N @ β ⊸ φ)) ⇒ (r ▷ θ)
⊣⊢ ∀αβφ. (P @ α) ⇒ (c @ β) ⇒ (↑↓N @ β ⊸ φ) ⇒ (r ▷ α⊸β⊸φ)
in any way to make the ↑↓N situated in a ↓↑↓N so you can Brouwer's-theorem it down to ↓N. It's exactly the (c @ β) preventing you from narrowing the scope of the ∀βφ like
∀α (P @ α) ⇒ (c @ β) ⇒ ∀βφ. (↑↓N @ β ⊸ φ) ⇒ (r ▷ α⊸β⊸φ)
and observing that
∀βφ.(↑↓N @ β ⊸ φ) ⇒ (r ▷ α⊸β⊸φ)
⊣⊢ ∀φ.(↑↓N @ φ) ⇒ (r ⊗ α ▷ φ)
= (↓↑↓N) @ (r ⊗ α)
⊣⊢ (↓N) @ (r ⊗ α)

So the best we can do is a ternary connective (P1 [c]⊸ P2) which can't focus through P2. But if you unpack the definition of this and look at the resulting inference rules, SPOILER ALERT, it works essentially the same way as
c ⊸ P1 ⊸ ↑(c ⊗ P2)
Which is the same ol' boring take-and-put-back semantics we were trying to avoid! Boo.
Tags:
• #### (no subject)

Something that's bugged me for a long time is this: How many paths, starting at the origin, taking N steps either up, down, left or right, end up at…

• #### (no subject)

Still sad that SAC seems to end up being as complicated as it is. Surely there's some deeper duality between…

• #### (no subject)

I had already been meaning to dig into JaneSt's "Incremental" library, which bills itself as a practical implementation (in ocaml) of the ideas in…

• Post a new comment

#### Error

Anonymous comments are disabled in this journal

default userpic