How to turn the behaviour of a pythonic function into a proper formal notation

32 Views Asked by At

Coming from a python function I would like to describe a certain behavior in a more formal and general way:

Suppose I have a set of $n$ data points $X = \lbrace x_{1}, ..., x_{n} \rbrace$ where each data point $x \in X$ has a certain time and a certain location. For each data point, I would like to find all other data points which are in a certain temporal and spatial distance. My current attempt looks like this: $$ \text{ValidPoints(x)}=\lbrace z \in X \mid x \ne z \land \text{TimeDifference(x, z)} <= \mathbf{t} \land \text{Distance(x, z)} <= \mathbf{d} \rbrace $$ where $\mathbf{t}$ is a certain temporal and $\mathbf{d}$ a certain spatial threshold (for instance: $\mathbf{t} = 10 \ days$ and $\mathbf{d} = 600 \ meters$).

Is this a notation I could use? Also, do I have to define the functions $\text{TimeDifference}$ and $\text{Distance}$? If so, would I define them prior to $\text{ValidPoints}$ or afterward? Would something like "$\text{TimeDifference}(t_{1}, t_{2})$ is defined as the temporal difference between two data points in minutes" be sufficient?

Thank you very much in advance!