<p>Background: I'm a fresh grad student looking into interesting ideas I have. I do not have any theoretical computer science background beyond basic Theory of Computation stuff from undergrad.</p>
<p>If I have some kind of computer program or software system, and this system can be represented in lambda-calculus or some other formal system / calculus used for computation, can I then represent this computer program or software system using set theory? In other words, can I convert the calculus into set theory?</p>
<p>If so, then I would appreciate some resources/textbooks on this.</p>

CC BY-SA 4.0
2023-10-03T10:14:11.583Z
The question is a bit unclear on what it means to *represent* a calculus. Clearly, all of the well-known computational calculi (like Turing-machines, $\lambda$ or $\pi$ or Ambient) can be given via their operational semantics. And those  an be given by inductive rules which can be expressed in set theory by ordinal induction, see P. Aczel, *An Introduction to Inductive Definitions*. But this is trivial, so that's probably not what the question is about.
Martin Berger
CC BY-SA 4.0
2023-10-03T10:19:20.653Z
@MartinBerger For instance, if a computer program is represented using lambda-calculus (or some other calculus used for computation), then I want to be able to represent that computer program in terms of sets, elements of sets, relations, etc.
The Pointer
CC BY-SA 4.0
2023-10-03T10:22:49.757Z
You still have not defined what "to represent" means. I imagine that you want to use set theory for computational calculi, in the same way that set theory has been used to ground other mathematical fields. The answer is: yes you can, and indeed that's what Church, Kleene or Turing had in mind when they invented their foundational calculi. Where do you see difficulties?
Martin Berger
CC BY-SA 4.0
2023-10-03T10:28:34.967Z
@MartinBerger For instance, if we have a program that does something with some functions, perhaps I can represent the functions as individual sets $A$, $B$, $C$, $\dots$, each perhaps consisting of other sets to represent things like fields, parameters, etc., and then represent their interactions with each other using relations.
The Pointer
CC BY-SA 4.0
2023-10-03T10:39:54.740Z
I think what you may mean is denotational semantics, where you map syntax (programs) to other mathematical structures so that
the latter explains, in some sense, the former. This has been heavily studied. And there are indeed limitations how one can
do this naively, see e.g.
J. C. Reynolds, *Polymorphism is not Set-Theoretic* and
A. M. Pitts, *Polymorphism is set-theoretic, constructively*.
Martin Berger
CC BY-SA 4.0
2023-10-03T10:40:55.393Z
In order get an introduction to the field of operational and denotational semantics, I recommend G. Winskel, *The Formal Semantics of Programming Languages: An Introduction* which is very accessible.
Martin Berger
<lambda-calculus><set-theory><formal-systems>
Can lambda-calculus, or other formal systems / calculi, be represented using set theory?
The Pointer
# Can lambda-calculus, or other formal systems / calculi, be represented using set theory?

(Asked by: username_0 on 2023-10-03)

Background: I'm a fresh grad student looking into interesting ideas I have. I do not have any theoretical computer science background beyond basic Theory of Computation stuff from undergrad.

If I have some kind of computer program or software system, and this system can be represented in lambda-calculus or some other formal system / calculus used for computation, can I then represent this computer program or software system using set theory? In other words, can I convert the calculus into set theory?

If so, then I would appreciate some resources/textbooks on this.

**Tags:** lambda-calculus, set-theory, formal-systems
> **Comments:**
> **username_1**: The question is a bit unclear on what it means to *represent* a calculus. Clearly, all of the well-known computational calculi (like Turing-machines, $\lambda$ or $\pi$ or Ambient) can be given via their operational semantics. And those  an be given by inductive rules which can be expressed in set theory by ordinal induction, see P. Aczel, *An Introduction to Inductive Definitions*. But this is trivial, so that's probably not what the question is about.  
> **username_0**: @MartinBerger For instance, if a computer program is represented using lambda-calculus (or some other calculus used for computation), then I want to be able to represent that computer program in terms of sets, elements of sets, relations, etc.  
> **username_1**: You still have not defined what "to represent" means. I imagine that you want to use set theory for computational calculi, in the same way that set theory has been used to ground other mathematical fields. The answer is: yes you can, and indeed that's what Church, Kleene or Turing had in mind when they invented their foundational calculi. Where do you see difficulties?  
> **username_0**: @MartinBerger For instance, if we have a program that does something with some functions, perhaps I can represent the functions as individual sets $A$, $B$, $C$, $\dots$, each perhaps consisting of other sets to represent things like fields, parameters, etc., and then represent their interactions with each other using relations.  
> **username_1**: I think what you may mean is denotational semantics, where you map syntax (programs) to other mathematical structures so that the latter explains, in some sense, the former. This has been heavily studied. And there are indeed limitations how one can do this naively, see e.g. J. C. Reynolds, *Polymorphism is not Set-Theoretic* and A. M. Pitts, *Polymorphism is set-theoretic, constructively*.  
> **username_1**: In order get an introduction to the field of operational and denotational semantics, I recommend G. Winskel, *The Formal Semantics of Programming Languages: An Introduction* which is very accessible.  

---

## 0 answers

