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?

  • $\begingroup$ There are no relations in most programming languages (on the language level, at least), only operators in expressions. So I don't see that there's anything to confound; it's your expectations that don't match how programming languages work. $\endgroup$ – Raphael Oct 14 '17 at 10:48
  • $\begingroup$ @Raphael I am not talking about what ‘most’ programming languages do. It is just an idea that we should treat the two things differently, so that the complete foundation of programming might be clearer, or simplier. $\endgroup$ – fantasie Oct 14 '17 at 10:53
  • $\begingroup$ Yes, but you're suggesting it's in any way unclear. I don't think it is. Many languages have (almost) formal semantics. You only get confused if you think C <= should mean the same as mathematical $\leq$. That's why I'm saying your expectations are the issue. Programming languages are not equivalent to the language of mathematics. $\endgroup$ – Raphael Oct 14 '17 at 10:55
  • 2
    $\begingroup$ Mathematics doesn't have mutable state, so it doesn't have to bother with this. (You always say "let $a = 1$", not only "$a = 1$"; you are asserting that $a=1$ holds true, not assigning anything.) In the areas that do bother (study of semantics in TCS), often $x \leftarrow y$ is used for updates aka "assignments". Some early programming languages used :=, too. And, just to skrew with us, different PLs mean different things by ==, and some have === to compensate. $\endgroup$ – Raphael Oct 14 '17 at 11:15
  • 3
    $\begingroup$ But what's your question? It looks like you're trying to kick off a discussion about your opinions of programming language design; that's not what we do, here. $\endgroup$ – David Richerby Oct 14 '17 at 14:26

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.

  • $\begingroup$ Thanks. I edited my question as they advised me to, but I think that your answer is not affected. Do you mean that there relations are isomorphic to boolean functions, so they are the same except for some small differences? And is that you would prefer boolean functions to propositions in real applications? $\endgroup$ – fantasie Oct 14 '17 at 16:12
  • $\begingroup$ I think that we are not necessarily to deduce first-order in that way. Just show that predicates and functions are different things, and there may be further syntactic developments. $\endgroup$ – fantasie Oct 14 '17 at 16:18

Not the answer you're looking for? Browse other questions tagged or ask your own question.