1
$\begingroup$

I hope this question makes sense, but I was wondering if there are other models of computation similar to lambda calculus that you can use to build up axiomatic mathematical and logical fundamentals like numbers, operators, arithmetic functions and such?

$\endgroup$
5
$\begingroup$

Yes, there are many models of computation, and of those many are extensions or modifications of the $\lambda$-calculus. You may wish to learn about partial combinatory algebras, which are very general models of computation, of which the $\lambda$-calculus is an example. Every partial combinatory algebra has a $\lambda$-like notation for defining functions. They encompass examples such as: $\lambda$-calculus, Turing machines, Turing machines with oracles, topological models of computation, PCF, etc.

Many models of computation can be seen as extensions or modifications of the $\lambda$-calculus. Let us consider the simply typed $\lambda$-calculus augmented with various features:

  1. System T is $\lambda$-calculus with natural numbers and primitive recursion. It is not Turing complete.
  2. The aforementioned PCF is $\lambda$-calculus extended with natural numbers and general recursion. It is Turing complete.
  3. There are many extensions of PCF, for instance PCF++ can perform parallel computations, PCF+catch can throw and catch exceptiosn, PCF+quote can disasemble code into source code, etc. These are all different computation models based on the $\lambda$-calculus.
  4. In another direction, we can extend the $\lambda$-calculus with more powerful types, for instance System F is a $\lambda$-calculus with polymorphic types. It is quite powerful but not Turing complete.

All of this is just scratching a rich theory of models of computation and functional programming languages (which is what extensions of $\lambda$-calculus are, more or less). If you are interested in the topic, you can start by reading some books on the principles of programming langauges (for practical aspects), or some books on realizability theory (for theoretical aspects).

$\endgroup$
  • $\begingroup$ What are the few non-lambda-calculus models that could fit to the criterion of computable? Is there other "method" than some sort of function notation or turing machinery? $\endgroup$ – MarkokraM Apr 2 at 18:12
  • $\begingroup$ There are many many models of computation. If you would like to know more about the topic, I am afraid you will have to study it. For this purpose I included many links in my answer. I suggest you follow them, as I cannot explain everything here. $\endgroup$ – Andrej Bauer Apr 2 at 20:10
  • $\begingroup$ So, do you mean that these other systems are not conceptualized / named and cannot be listed easily? In the original question, I'm particularly asking for other systems than obviously LC related, so in the answer I'm expected to see them rather than LC modifications. $\endgroup$ – MarkokraM Apr 5 at 10:10
  • $\begingroup$ What I am saying is that you should read the existing literature. Start by chasing the links that I provided. There is a whole world of models of computation out there which does not fit into this answer. $\endgroup$ – Andrej Bauer Apr 5 at 11:36
3
$\begingroup$

Historically, Church, Kleene, and perhaps others argued for recursive functions to capture mathematical reasoning. Godel instead posed mathematical reasoning as syntax in logical symbols. There is a story, as told by Wadler, (here if the link still works) that Church showed Godel their different notion were equivalent, causing Godel to remark that therefore neither model expresses mathematical reasoning accurately. Turing added a further formulation that any "Turing complete" machine could reproduce both Godel's model and Church's model. ...so... insofas $\lambda$-calculus is just a syntax for evaluating functions there isn't really any strength here that couldn't for example be achieved by strings in a Turing Machine or strings in PHP. As long as a computational model is Turing complete at least there should be an equivalent way to do all computations. This is roughly the statement of today's "Turing-Church Thesis". Belief in whether this capture mathematical sophistication is a personal choice, but it says that you really can't invent a Turing complete programming model that can't do math. So in that sense the answer to your question is almost every programming language.

Even so, some languages that leverage mathematical axioms (Idris, Agda), theorem proving etc. actually try to restrict you to "total functions" meaning all inputs have an output in finite time (no infinite recursions). Those are actually less powerful than say C or PHP in that they are not Turing complete. But as Edwin Brady is happy to remind people, it is still likely that most interested programs such as "Pac-man" can be written in total languages.

I think the spirit of you question is to spark a list of programming abstractions related to mathematical reasoning. To that I would say beyond the syntax of $\lambda$-calculus the following are essential for making any mathematical reasoning readable and thereby useable.

  • A good way to distinguish values/varaibles, from functions, from relations. This could be a set theory or a type theory. In vogue today are dependent types (or path-dependent as in Scala if thats what you can get). Mathematics however is still largely in the set groove so there is a need to translate. But however the model it needs to be clear that there are elements to input to a function, and that the elements together can be collected into different clumps (sets or types) and that we can impose relationships between the elements in clumps (equivalence, partial orders etc.)
  • Good type inference. Math doesn't say what $x$ or $2$ is everytime it uses it in an equation, it would be too hard to get going or to read. The programming language has to be able to figure that out on its own from context. To me type inference means that with very little writing the reader and the programming language can tell whether we intend a value/varaible/function/ or relation, and place it if need be within a constrained context, such as a set or type.
  • Implicit context -- similar to type inference, we need not only the types but the functions to be self-evident from context even if their exact syntax can be found elsewhere with different meaning. This is more than type checking. E.g. $x*y*z$ needs to have the type inference tell you what $*$ means, but it also needs to be clear that this could be treated as $(x*y)*z$ or as $x*(y*z)$ which is an axiom on $*$ you wouldn't bother to expressly mention but would be critical to some type-checking. So implicit context to me is the addition of theory given by the axioms. It is ok (and necessary) that this theory be constructive, i.e. a language is only required to invoke theorems it has already proved. But it should largely on its own look up what is already known, perhaps with hints (often called "tactics").

Given all that, its quite fun to explore, and many languages now can handle this. But I would say still so far none do such a great job. So far most systems are reasonably good at axioms in 1st order logic. E.g. equations that have to hold such as Length(List1 cat List 2)=Lenght(List1) + Length(List2). That really is far short of high-level reasoning about numbers.

A programming languages still can't reason well about relations, e.g. quotients, homotopies, and equivalences. As a simple exercise consider how you would write a program that produced the field $\mathbb{Z}/p$ for a prime $p$. How would you prove non-zero elements have inverses? Its a simple mathematical expression to state $(\forall x)(x\neq 0\Rightarrow (\exists y)(xy=1))$. But somewhere down the line you have to hide a proof that $p$ is prime (here I mean $p$ is a variable to your dependently typed $\mathbb{Z}/p$). After AKS that can be done but not at all trivially in the type system. Without this you wont get to build say linear algebra over finite fields or prove some RSA system is correct etc.

As a larger point, most languages hope to express objects with equivalent types as normal forms, and then compare normal forms. This can be incredibly expensive computationally. And if your language is Turing complete it can actually be impossible.

$\endgroup$
  • $\begingroup$ From a short question you got my point very well. Surely most of the computer languages with anonymous functions provides the same model than LC only with syntactical differences. So I was looking for something different. Absractions you gave, however, suit well to the question. How fundamental is the substitution method? Isnt it the core of the computability? Math equations are often about simlifying and replacing symbols. Is this the only way to go? Also, could category theory help with revealing what is happening behind the equality sign in math equations? $\endgroup$ – MarkokraM Mar 25 at 19:08
  • 1
    $\begingroup$ Can you please provide a source for the claim that "Church developed recursive functions (with $\lambda$-calculus as a notation) to capture mathematical reasoning"? I think you are inventing history here, as recursive functions were not the primary motivation for the invention of the $\lambda$-calculus. $\endgroup$ – Andrej Bauer Mar 25 at 20:09
  • $\begingroup$ True, I should not have assigned intent like this to Church's $\lambda$-calculus, nor been so non-academic about the timeline. I will edit. But you caused me try and recall where I heard this anecdote, it was by Wadler, and I can do no better than to point to his research on the history here. $\endgroup$ – Algeboy Mar 25 at 20:28
  • $\begingroup$ @MarkokraM, I work on computational aglebra and it's great to have some help from the language/compiler, but no I'd say most steps look nothing like basic substitutions. A lot of linear and polynomial solving happens instead. Most major progress in that domain you get from better algorithms, not so much different data structures or programming languages. But indeed, you program faster and with fewer errors in expressive languages. $\endgroup$ – Algeboy Mar 25 at 20:50

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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