Formalizing three dots

Suppose $G$ is a semigroup with an operation $f : G\times G \rightarrow G$ (written multiplicatively as “ $\cdot$ “), $a : \mathbb{N} \rightarrow G$ is a sequence of elements of $G$ and $\Lambda \subseteq \mathbb{N}$ is a finite set of natural numbers. We want to define the product of elements $a_i$ given by the indices coming from $\Lambda$ , i.e. the element expressed by the formula $\prod_{i\in \Lambda} a_i$ .

It is easy to explain to a human what we want by using the “three dots” notation. Namely, if $\Lambda = \{i_0, i_1, ... , i_{n-1}\}$ , then by $\prod_{i\in \Lambda} a_i$ we mean $a_{i_0} \cdot a_{i_1} \cdot ... \cdot a_{i_{n-1}}$ . However, this will not work with a machine. When doing machine verifiable mathematics we actually have to define what we mean.

In IsarMathLib we are able to define a product of a list of elements of a semigroup using the the notion of Fold. So, if $a: \{0, 1, ... , n-1\} \rightarrow G$ we know what is $\prod a = \prod_{i=0}^{n-1} a_i$ . How can we generalize it for any finite set of indices?

Let’s look at the three dots in the expression $\Lambda = \{i_0, i_1, ... , i_{n-1}\}$ . This is a list of natural numbers, which can be understood as a function $\sigma : \{0, 1, ... , n-1\} \rightarrow \mathbb{N}$ . In ZF set theory for a natural number $n\in\mathbb{N}$ we have $n = \{0, 1, ... , n-1\}$ so we can write $\sigma : n \rightarrow \mathbb{N}$ . We want to list the numbers from $\Lambda$ in the increasing order, so really $\sigma$ is an order isomorphism from $n$ to $\Lambda$ . The key fact that we can rely on is that for linear order relations each two finite sets that have the same number of elements are order isomorphic and the isomorphism is unique. This allows to define the enumeration of a finite set $\Lambda$ of natural numbers as the unique order isomorphism between the number of elements of $\Lambda$ and $\Lambda$ , i.e. $\bigcup ord\_iso (|\Lambda |,r_\mathbb{N},\Lambda ,r_\mathbb{N} )$ . Here $ord\_iso(A,r,B,R)$ is the set of order isomorphisms between a set $A$ ordered by relation $r$ and set $B$ ordered by relation $R$ , $|\Lambda|$ is the number of elements in $\Lambda$ (which is a natural number for finite sets) and $r_\mathbb{N}$ is the (natural linear) order relation on natural numbers. We are using the formula $\bigcup\{x\} = x$ to extract the only element from a singleton.
This way we can reduce a product over a finite set of indices to the product over a list by defining $\prod_{i\in \Lambda} a_i = \prod a \circ \sigma$ , where $\sigma : |\Lambda | \rightarrow \Lambda$ is the unique enumeration of the set $\Lambda$ .
And to do that we need to prove that any two finite linearly ordered sets admit a unique order isomorphism. That was quite unexpected.

About these ads

Tags: formalized mathematics

This entry was posted on August 24, 2008 at 5:04 pm and is filed under news, Proofs. You can follow any responses to this entry through the RSS 2.0 feed. You can leave a response, or trackback from your own site.

10 Responses to “Formalizing three dots”

IsarMathLib version 1.6.5 relased « Formalized Mathematics Says:
September 27, 2008 at 12:54 am | Reply
[...] with the same number of elements are order-isomorphic and the isomorphism is unique. I have written previously on the motivation for this. The theorem was surprisingly tedious to prove and required about 50 [...]
pdf23ds Says:
March 20, 2009 at 2:47 am | Reply
It looks like you still have more work to do to formalize something like

(lambda x1 … xn. f(x1, …, xn)) == (lambda x1. (lambda x2. (… (lambda xn. f(x1, …, x2)) …)).

(Seen here.)

BTW, I responded to your comment at my site.
slawekk Says:
March 20, 2009 at 9:14 pm | Reply
Note that IsarMathLib is is based on ZF set theory, not lambda calculus. I don’t know lambda calculus, so I can’t even think about some sort of analogous statement in set theory. But I always wanted to learn something about l. c., so thanks for the link.
pdf23ds Says:
March 20, 2009 at 10:41 pm | Reply
I think the idiom is general to all nested structures, of which there are plenty in ZF. For instance, if I wanted to talk about the representation of the natural n, I could write the set (using underscore as subscript, 0 as empty set)

{_1 {_2 … {_n 0 } … } }
slawekk Says:
March 20, 2009 at 11:24 pm | Reply
But the expression (in the first comment) you wrote is an identity between two forms of such nested structure. Could you write what would be such identity for the natural numbers? Perhaps one more example (with functions?) so that I can have a better feel for the analogy?
pdf23ds Says:
March 21, 2009 at 12:28 am | Reply
Hmm. I’m not sure if this is what you’re looking for, but I suppose one could define a function to convert a natural number to a pair of natural numbers, like so:

f(n) ==

f({_1 {_2 … {_n 0 } … } }) ==

Where a pair is defined appropriately.
pdf23ds Says:
March 21, 2009 at 1:40 am | Reply
Oh my, it looks like my angle brakets were all eaten and such.
slawekk Says:
March 21, 2009 at 12:45 pm | Reply
It is best to use LaTeX markup like this: (dollar sign)latex some formula (dollar sign).
The dollar sign should be without parentheses of course and there should be no space between the opening dollar sign and the “latex” word.
pdf23ds Says:
March 21, 2009 at 3:09 pm | Reply
Hmm, I’m not so familiar with latex, but I’ll give it a shot.

$f(n) \equiv \langle n, 2n\rangle$

$f(\lbrace_1 \lbrace_2 \cdots \lbrace_n \varnothing \rbrace \cdots \rbrace \rbrace) \equiv \langle \lbrace_1 \lbrace_2 \cdots \lbrace_n \varnothing \rbrace \cdots \rbrace \rbrace , \lbrace_1 \lbrace_2 \cdots \lbrace_n \lbrace_1 \lbrace_2 \cdots \lbrace_n \varnothing \rbrace \cdots \rbrace \rbrace \rbrace \cdots \rbrace \rbrace$

You can delete the superfluous comments. (No preview!)
slawekk Says:
March 21, 2009 at 6:45 pm | Reply
I see what you mean. But what would it mean to formalize this? Normally it would mean “invent a notation for this that doesn’t use three dots and prove some properties that informally would be written with three dots”. For example instead of (informal)
$a_0 + a_1 + ... + a_{n-1} + a_n = a_n + a_0 + a_1 + ... + a_{n-1}$ we could have formal notation $\sum_n a$ that would replace $a_0+ a_1 + ... + a_{n-1}$ and prove something like $\sum_{n+1} a= a_n + \sum_n a$ .

In case of natural numbers such thing is already done in Isabelle/ZF. Natural numbers are defined in the way standard for ZF set theory as sets built from the empty set with the nested structure like you write in your comment. There are lots of theorems proven about those sets (natural numbers).

Formalized Mathematics

Formalizing three dots

Like this:

10 Responses to “Formalizing three dots”

Leave a Reply Cancel reply

Follow “Formalized Mathematics”