0
$\begingroup$

I'm writing a lengthy proof in which I am stating the proof in prose and then in mathematical symbols.

But I don't know the notation to define a symbol that meets certain constraints. In the following example I've used min and max to get around my problem in two of the definitions, but in the definition of s, I am reverting to the TLA+ notation.

Let $c$ be the first process to join that has a value. Let $c$ be in the cell $C$ of the leader $s$, and let $n$ be the leader of the next cell. \begin{eqnarray*} & c \overset{\Delta}{=}& \min(\{p \in P : v[p] \in V\})\\ & s \overset{\Delta}{=}& CHOOSE\;p \in S : p \in Cell(s)\\ & C \overset{\Delta}{=}& Cell(s)\\ & n \overset{\Delta}{=}& \max(\{p \in S : p < s\}) \end{eqnarray*}

I have never seen the CHOOSE notation outside the TLA+ ecosystem. What other ways of defining $s$ are there?

As an aside, I've also defined $\min$ in TLA+ using CHOOSE ($\max$ is similar):

$$\min(S) \overset{\Delta}{=} CHOOSE\;x \in S : \forall y \in S : x \leq y$$

$\endgroup$
3
  • $\begingroup$ Is there a unique $s\in S$ such that $c\in Cell(s)$? $\endgroup$ Commented Sep 13, 2013 at 22:27
  • $\begingroup$ Yes in this case there is a unique s that matches that predicate (see also the min example). $\endgroup$ Commented Sep 13, 2013 at 22:30
  • $\begingroup$ Thinking back in all the uses I've seen of CHOOSE, it doesn't have to be unique. But in all the cases that I am using, it is unique. $\endgroup$ Commented Sep 13, 2013 at 22:33

1 Answer 1

1
$\begingroup$

You can use the iota quantifier from logic, though you’ll have to define it, since most mathematicians probably aren’t familiar with it: $\iota x\varphi(x)$ is the unique $x$ such that $\varphi(x)$, if there is such an $x$, and $\varnothing$ otherwise. In your case,

$$s\overset{\Delta}{=}\iota p\in S\big(p\in Cell(s)\big)\;.$$

$\endgroup$
2
  • $\begingroup$ That's cool. How would I do it if it were not unique? $\endgroup$ Commented Sep 13, 2013 at 23:30
  • $\begingroup$ @Michael: I don’t think that I’ve seen a notation for ‘let $x$ be an arbitrary element of $X$’, which is really what you’re asking for in that case. (And I’d not actually use one even if I knew one: plain English is much clearer.) $\endgroup$ Commented Sep 13, 2013 at 23:34

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .