In programming languages, generally we do not distinguish relations and functions. Is there a better way to deal with these two concepts? [closed]

Question

When we write a mathematical formula, the rule $a=42$ (when we say let $a=42$) and testing them (when we write something like $\ldots \mathrm{if} x=42$) is written in a same equal sign. I think that both of them are representing some relation. However, while programming, we write = for the first circumstance and == for the second, and == is actually the infix representation of the equivalent testing function. Should they be treated as the same thing?

---

Previous question:

Are programming languages confounding relations and functions?

p.s. I have been asking this a few hours ago on StackOverflow, but they told me that it was on a wrong venue.

For example, the equivalent sign = has a lot of meanings, including returning a boolean value that tests whether to expressions are equal to some extent, setting up a rule that both side are equal, and assign the right side to the left side. And notations such as < and || are generally parsed as boolean operators. What's more, they do not distinguish predicates and boolean functions.

In my opinion, this is not a very elegant way to treat the 'rules'. I think notations like ≤ should be thought to be a relation, which means a≤b implies $(a,b)\in R_\leq$, where $R_\leq \subset S^2$ and $S$ is the domain of $a$ and $b$. Mathematically, ≤ is not a function at all (If it is, it should be something maps from a subset of $S^2$ to $\{True, False\}$). It is just representing some rules.

However, while programming, we generally do not realize the difference between them. We may consider k = a < b as a simpler way to write something like k = True for a<b, False otherwise. However, I believe that this makes things confusing in some circumstances, for example, the use of =.

I have seen a lot of imperative and functional language that do not seem to respect these differences. Am I correct in this point of view? Is there a better way to solve this?

Answer 1

Let $A$ be any set. Then, its powerset $\mathcal{P}(A)$ is isomorphic to the function space $A\to \mathbb{B}$ where $\mathbb{B}=\{\sf true, false\}$.

Indeed, the isomorphism is given by mapping each subset to its own characteristic function.

$$ \begin{array}{lcl} \mathcal P A & \leftrightarrow & (A \to \mathbb B) \\ X & \mapsto & \lambda a. {\sf if}\ a\in X\ {\sf then\ true\ else\ false} \\ \{a|g(a)={\sf true}\} & \leftarrow\!\shortmid & g \end{array} $$

Since relations are sets of pairs, relations too can be seen as binary functions whose codomain is $\mathbb B$.

In most programming languages, as you realized, we don't really find propositions, sets, or relations, but we instead find their isomorphic counterparts: booleans, unary boolean functions, binary (or more) boolean functions.

This choice is mostly suggested by the fact that everything we compute ultimately is represented by a few bits. It is therefore very efficient for a computer to represent the truth values associated to propositions. Further, it is convenient to be able to write e.g. b = b or (y < 5) without using a conditional. (Actually, using a conditional for that usually reveals that the programmer does not understand that boolean expressions are indeed expressions, and not special syntax that is relegated to conditional or loop guards. This phenomenon also shows up in the infamous if b==true ... where the programmer often thought that we have to use at least one boolean operator in the guard, since we usually need that.)

In programming languages, there are some theoretical contexts where we do separate propositions from booleans, though. For instance, in the calculus of inductive constructions, as implemented in Coq, we find a Prop type for propositions, and a bool type for booleans. Very roughly, this allows the programmer to deal with propositions that can not be automatically checked by the computer, e.g. $\forall a,b,c\in\mathbb N.\ (a+b)\cdot c = a\cdot c + b\cdot c$ is a Prop. Even if the computer can not check them, we can still mathematically prove them. Note that we can not turn a Prop into its bool truth value since we have no way to check $\forall n$ or $\exists n$. (Actually, there's no such a thing as its "truth value" since the logic is constructive, but I'll be silent about this.) By comparison, we get two forms of n < 4 comparisons: one which is a Prop and can be used in logic, and another one which is a bool and can be used in programs.