I was going through these notes and they have the following operator on partial functions:

$$ \mathcal F^{k}(\bot)(\sigma) = \left\{ \begin{array}{ll} \alpha( [\![s]\!]\sigma ) & [\![b]\!]\sigma=true \\ \sigma & [\![b]\!]\sigma=false \\ \bot & [\![b]\!]\sigma=\bot \end{array} \right. $$

and supposedly it gives the following definition somehow (which ends up being the right denotation for while loops)

$$ \mathcal F^{k}(\bot)(\sigma) = \left\{ \begin{array}{ll} [\![s]\!]^i & \mbox{if $ \exists i \in [0,k)$ s.t. $ [\![b]\!] [\![s]\!]^i \sigma = false,\ [\![b]\!] [\![s]\!]^j \sigma = true,\ j \in [0,i) $}\\ \bot & \mbox{ o.w. } \end{array} \right. $$

the proof by induction is shouldn't be hard. However, it feels that it doesn't really answer the question for me intuitively because I could do the induction mechanically without understanding what is going on. Why isn't the definition something like:

$$ f(\sigma,i) = [\![s]\!]^i\sigma$$

then the induction is easy:

$$ f(\sigma,0) = [\![s]\!]^0\sigma = \sigma$$

then the inductive step:

$$ f(\sigma,k+1) = f \circ f{\circ}^k(\sigma)= f \circ[\![s]\!]^{k}\sigma$$

but also notice $f = [\![s]\!]^1\sigma$ by strong induction:

$$ f(\sigma,k+1) = [\![s]\!]^{k+1}\sigma$$

as required. But that doesn't seem at all to be the sort of argument being used (assuming what I wrote is right). Did I miss something?

  • $\begingroup$ The quantifier is misplaced, as usual in such definitions. This is due to lack of reasonable notation for what needs to be expressed. $\endgroup$ – Andrej Bauer Oct 8 '18 at 6:22
  • $\begingroup$ Is that supposed to be the formula at page 160? If so, you didn't copy it exactly. Your first equation indeed confuses me, while the one in the notes is reasonable. (Further, please add a page number to the reference: trying to find what formula you mean in a long document is not pleasant) $\endgroup$ – chi Oct 8 '18 at 12:26

The existential quantifier is misplaced. This is due to lack of reasonable notation for what needs to be expressed, namely: "if there is $i$ safisfying condition $C$, then use that $i$", where we make sure that at most one such $i$ exists. It would be better to write (and by the way, you might appreciate LaTeX's cases environment): $$ \mathcal F^{k}(\bot)(\sigma) = \begin{cases} [\![s]\!]^i & \text{if $i < k$ and $[\![b]\!] [\![s]\!]^i \sigma = \text{false}$ and, for all $j < i$, $[\![b]\!] [\![s]\!]^j \sigma = true$}\\ \bot & \text{otherwise} \end{cases} $$ It may be helpful to look at a simpler definition. Suppose we want a function $f : \mathbb{N} \to \mathbb{N}$ which maps an odd number to zero and an even number to half of itself. The following is a reasonable definition: \begin{align*} f(2 n) &= n\\ f(2 n + 1) &= 0 \end{align*} as is the following (where $m$ and $n$ range over natural numbers): $$ f(m) = \begin{cases} n & \text{if $m = 2 n$,}\\ 0 & \text{otherwise.} \end{cases}$$ The point is that precisely one branch applies, and in a unique way, as there can be at most one $n$ satisfying the condition $m = 2 n$. However, the following is not a reasonable definition: $$ f(m) = \begin{cases} n & \text{if $\exists n \in \mathbb{N} \,.\, m = 2 n$,}\\ 0 & \text{otherwise.} \end{cases}$$ The problem is that the $n$ outside the $\exists$ quantifier is completely unspecified. This is so because the $n$ inside the $\exists$ quantifier is bound and can therefore be renamed at will: $$ f(m) = \begin{cases} n & \text{if $\exists k \in \mathbb{N} \,.\, m = 2 k$,}\\ 0 & \text{otherwise.} \end{cases}$$ (And we do not rename the outer $n$ because it is not in the scope of $\exists$.) This makes it clear that the existential quantifier has no place there. It is important to understand variable bindings. In the above definition of $f$, the variable $n$ is bound in the entire case, not just in the condition.

From a very formal point of view, the map $f$ is defined here as a relation explaining how an argument of $f$ is related to its value. A definition of the form $$f(m) = \begin{cases} e_1(m,n) & \text{if $\phi_1(m,n)$} \\ e_2(m,n) & \text{if $\phi_2(m,n)$} \end{cases} $$ is equivalent to $$f(m) = \text{the $v$ such that $\psi(m,v)$} $$ where $$\psi(m,v) \iff (\exists n \,.\, \phi_1(m,n) \land v = e_1(m,n)) \lor (\exists n \,.\, \phi_2(m,n) \land v = e_2(m,n))$$ Now the quantifiers are justified. By the way, we could have used $\forall$ instead: $$\psi(m,v) \iff (\forall n \,.\, \phi_1(m,n) \Rightarrow v = e_1(m,n)) \land (\forall n \,.\, \phi_2(m,n) \Rightarrow v = e_2(m,n)).$$

| cite | improve this answer | |
  • $\begingroup$ It's strange that you say there's no reasonable notation and then immediately write is using perfectly reasonable notation... $\endgroup$ – David Richerby Oct 8 '18 at 7:06
  • $\begingroup$ I find my own notation a bit unreasonable because it does not protect us from typos. That is, nowhere does it explicitly introduce the bound variable, and that's prone to errors. (Imagine allowing several bound instead of just one, and then mistyping one of them.) $\endgroup$ – Andrej Bauer Oct 8 '18 at 8:48
  • 1
    $\begingroup$ Do you think that pulling the "if" outside the defintion of $\mathcal{F}$ and writing something like "If there is some $i$ such that..., then $\mathcal{F}=i$; otherwise, $\mathcal{F}=\bot$" helps? $\endgroup$ – David Richerby Oct 8 '18 at 8:54
  • $\begingroup$ That's what is usually done informally. I am trying to think how this would be done in a proof assistant. Machines are completely unforgiving. I suppose it would be best to simply introduce a definite description operator (but there's still the issue of having to deal with partiallity). $\endgroup$ – Andrej Bauer Oct 8 '18 at 8:56
  • $\begingroup$ Can you define an "unwrapping" operator such that $\mathrm{unwrap}(\{x\})=x$ and $\mathrm{unwrap}(Y)=\bot$ if $|Y|\neq 1$? Then you could define $\mathcal{F} =\mathrm{unwrap}(\{[\![s]\!]^i\mid \text{false at }i\text{ and true at all }j<i\})$. $\endgroup$ – David Richerby Oct 8 '18 at 9:02

The intuition is that the loop terminates at the $i$th iteration if the loop condition is false at that iteration but true at all earlier ones. If the loop condition is never false, then the loop doesn't terminate and the denotation is $\bot$.

However, it's written down wrongly. What it says is (and please pardon me for throwing away all the notation and working by analogy):

  • The answer is $i$ if there exists some $i$ such that the loop condition becomes false at the $i$th iteration;
  • otherwise, the answer is $\bot$.

The problem is that the variable $i$ only has meaning within the scope of "there exists some $i$ such that...", and it's referred to outside that scope. So what's written is equivalent to "The answer is $i$ if there exists some $q$ such that the loop condition becomes false at the $q$th iteration", to which the obvious response is "What's $i$?"

What it should say is:

  • If there is some $i$ such that the loop condition becomes false at the $i$th iteration, the answer is $i$;
  • otherwise, the answer is $\bot$.
| cite | improve this answer | |
  • $\begingroup$ It seems odd to say "the loop exists". Would it not make more sense to say that "the loop terminates"? Or something else, but surely not that it "exists". It exists allright, see: while b do s done. $\endgroup$ – Andrej Bauer Oct 8 '18 at 6:23
  • $\begingroup$ @AndrejBauer It says "exits", not "exists". But, sure, I'll replace it with "terminates" to avoid the misreading. $\endgroup$ – David Richerby Oct 8 '18 at 7:03
  • $\begingroup$ Oops, I apologize. That's all right, you keep it "exits" and I'll get new glasses. I am still capable of misreading terminates as termites. $\endgroup$ – Andrej Bauer Oct 8 '18 at 8:49
  • $\begingroup$ Hmm. "Ends"? :-D $\endgroup$ – David Richerby Oct 8 '18 at 8:52

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.