# Can lambda-calculus, or other formal systems / calculi, be represented using set theory?

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.

• 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. Oct 3, 2023 at 10:14
• @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. Oct 3, 2023 at 10:19
• 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? Oct 3, 2023 at 10:22
• 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. Oct 3, 2023 at 10:39
• 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. Oct 3, 2023 at 10:40