1

I am trying to understand some of the mathematical underpinnings of computing, and I've gotten stuck on functions and stackframes. For example, consider the following bit of code that is executed during a program:

{
  // Stackframe S
  a = 1        // <= type Int
  b = true     // <= type Bool
  c = f(a, b)  // <= type F, the type returned by f

// Now use a, b, and c... }

where I've added braces to denote the entirety of the stackframe $S$. After the function $f$ is invoked (where $f: \mathrm{Int} \times \mathrm{Bool} \rightarrow F$) the variables $a$, $b$, and $c$ exist and can be used. From a set-theoretic point of view, it appears that the following relations hold:

\begin{eqnarray} 1. \qquad a & \in &\mathrm{Int} &\wedge& S \\ 2. \qquad b & \in &\mathrm{Bool} &\wedge& S \\ 3. \qquad c & \in & F &\wedge& S \end{eqnarray}

However, this doesn't quite seem right to me. The invocation of f(a, b) appears to suggest the following:

\begin{eqnarray} 4. \qquad f &:& (\mathrm{Int} \wedge S) &\times& (\mathrm{Bool} \wedge S) &\rightarrow& F \wedge (?) \text{, or} \\ 5. \qquad f &:& (\mathrm{Int} \times \mathrm{Bool}) &\wedge& (S \times S) &\rightarrow& F \wedge (?) \end{eqnarray}

Due to symmetry considerations, the question mark should presumably be replaced with $S \times S$, but according to relation 3 above, it appears that it should be simply $S$. So what has happened here? Have I made a false assumption on what is going on whenever the function $f$ is applied on arguments from restricted domains? Or is another operation going on that simply "collapses" the $S \times S$ set to $S$?

Asaf Karagila
  • 393,674
  • By writing $a\in\mathrm{Int}\wedge S$, you are mixing up two things. It is the value of $a$ that can be regarded as an element of $\mathrm{Int}$, but it's the name $a$ that can be (in some sense) regarded as an element of a stack frame. – Stefan Dec 18 '23 at 20:11
  • @Stefan--okay, so there's an indirection from $a$ to the value of $a$, but does that fundamentally alter the question? Suppose my set is simply $S = {1, true, f_1}$, where $f_1$ is some value returned by the function $f$. The first argument to $f$ will be $\in \mathrm{Int} \wedge S$, and so on. – Kyle Knoepfel Dec 18 '23 at 20:42
  • Stackframe is not really a set. Variable's type is also not a set. Finally invokable functions (or more precisely: subroutines) are not really mathematical functions. You mix all those things, why? There is no need to do that, each of those things has its own description. Either way the question mark should be replaced with S, that's the only reasonable choice here. I'm not sure what those "symmetry considerations" are. – freakish Dec 18 '23 at 21:23
  • In computer science, one would say that $S$ is a tuple (hence a cartesian product of sets), rather than a set. Mixing values coming from $a, b, c$ is too unprecise. Cf. "Type theory" in https://en.m.wikipedia.org/wiki/Tuple – Jean-Armand Moroni Dec 18 '23 at 21:27
  • @freakish and Jean-Armand Moroni, um, yeah, I know there are CS-based definitions of what these things are (I've been a professional programmer for 10 years). I'm asking about the mathematical connections--and there are many of them (e.g. type and category theory). If my set-based description of stackframes and subroutines is off, can you provide a better description? – Kyle Knoepfel Dec 18 '23 at 21:40
  • Why do you think you need a better description beyond what CS and related theories provide? What is wrong or missing in the standard approach? By the way, you may want to read about stack machine, it is one of the possible models of stackframe. – freakish Dec 18 '23 at 21:42
  • @freakish, I am tasked with developing a data-processing software framework that is starting to look a lot like E. Codd's relational model. The user stores their data in a "table", and they register operations to apply to that data. I intended $S$ to more-or-less represent the table, because that is how the users currently think. But it's looking like the analogies between the stackframe and the relational model table are too weak to be useful. – Kyle Knoepfel Dec 18 '23 at 22:09
  • Yeah, this doesn't sound like a correct way. Without knowing details, perhaps you just need to write a workflow framework? – freakish Dec 19 '23 at 11:19

0 Answers0