Standard notation for building records from sets

115 Views Asked by At

Tuples: Tuples are of the form $(v_1, \dots, v_n)$. The are indexed by natural numbers, which means that we can access its elements by $(v_1, \dots, v_n)(i)=v_i$. One way to create a set of tuples from sets $S_1, \dots, S_n$ is by this notation: $\prod_{i=1}^n S_i$

My question: Now, I want to achieve the same for records. Records are of the form $(x_1=v_1, \dots, x_n=v_n)$, where $x_1, \dots, x_n$ are variable names. We can access its elements by those variable names: $(x_1=v_1, \dots, x_n=v_n)(x_i)=v_i$.

How can I now create a set of records from some sets? In particular, if I have sets $S_1, \dots, S_n$, what is the standard notation for $\{ (x_1=v_1, \dots, x_n=v_n) \mid \forall i \in [n]: v_i \in S_i \}$?

A possible solution: I guess it would help to embed sets $S$ into tuples by something like $(x=S) := \{(x=v) \mid v \in S\}$. Then, I could use $\prod_{i=1}^n (x_i=S_i)$ to achieve what I want.

But is this the standard way? Or are there better ways?

Edit: Some context: I want to give semantics to a programming language. For this, it is convenient to model the set of states by a set of records. If I have a state $\sigma$ and want to evaluate a variable $x$ in that state, I can simply use that variable's name, as in $\sigma(x)$.

2

There are 2 best solutions below

2
On BEST ANSWER

A record can be considered a function defined on the set of variable names. So you would define the set $I =\{x_1, \dots,x_n\}$ of variable names and write $S_x$ for the set of values the variable $x$ can take. The set of records is written $\prod_{x\in I} S_x$. For a record $r$ in this set, you can use $r(x)$ or $r_x$ for the value of the entry $x$.

The notation $(x_1 = v_1,\dots,x_n=v_n)$ for a record would not be standard, but you could certainly define it. (I would use something like $(x_1\mapsto v_1,\dots,x_n\mapsto v_n)$ instead.) If your variable names are ordered (as they implicitly are by their names $x_1$,$x_2$, etc. you might also get away with the shorthand $(v_1,\dots,v_n)$, leaving the variable names implicit.

1
On

The notion of a "variable name" seems a lot to me like a random variable, which is a function from a set of outcomes $\Omega$ to a set of real numbers. So each variable $x_k$ would be a function $x_k:\Omega\to\mathbb R$, i.e. you'd have a rule that tells you the value of $x_k(\omega)$ for each $\omega\in\Omega$.

Given sets $S_1,...,S_n$, your desired set is expressed as

$$\{\omega\in\Omega:(x_1(\omega),...,x_n(\omega))\in S_1\times\ldots S_n\}$$