# Questions tagged [lambda-calculus]

λ-calculus is a formal system for function definition, function application and recursion which forms the mathematical basis of functional programming.

34 questions
Filter by
Sorted by
Tagged with
2k views

### Does there exist a Turing complete typed lambda calculus?

Do there exist any Turing complete typed lambda calculi? If so, what are a few examples?
7k views

### Why are functional languages Turing complete?

Perhaps my limited understanding of the subject is incorrect, but this is what I understand so far: Functional programming is based off of Lambda Calculus, formulated by Alonzo Church. Imperative ...
280 views

### Is there an always-halting, limited model of computation accepting $R$ but not $RE$?

So, I know that the halting problem is undecidable for Turing machines. The trick is that TMs can decide recursive languages, and can accept Recursively Enumerable (RE) languages. I'm wondering, is ...
2k views

### Quantum lambda calculus

Classically, there are 3 popular ways to think about computation: Turing machine, circuits, and lambda-calculus (I use this as a catch all for most functional views). All 3 have been fruitful ways to ...
639 views

2k views

### Is there an algorithm for converting Turing machines into equivalent Lambda expressions?

We know that Turing machines and Lambda Calculus are equivalent in power. And There are proofs for that, I'm sure. But is there an algorithm, a systematic way for us to convert a Turing machine into ...
619 views

### Ī»-Calculus extensions: meaning of extension symbols

When working with Ī»-Calculus I see lots of extensions that use other symbols such as ā <:Top {} ā, which are from "Types and Programming Languages" (WorldCat) by Benjamin C. Pierce. ...
425 views

### Would adding recursive named functions to Simply typed lambda calculus make it Turing complete?

Say I have Simply typed lambda calculus, and add an assignment rule: <identifier> : <type> = <abstraction> Where ...
2k views

### Prove that turing machines and the lambda calculus are equivalent

It is known that a turing machine and the lambda calculus are equivalent in power. I now want to try to prove this myself. I think proving that the lambda calculus is at least as powerful as a turing ...
593 views

### Can the Lambda Calculus or Turing Machines model signals, callbacks, sleep/wait, or buses?

I have a deep appreciation for formalisms like the Turing Machine and the $\lambda$-Calculus, and enjoy studying them and learning more about how they relate to physical computers. I am now learning ...
144 views

### Why do we distinguish between term abstraction and type abstraction in System F?

In System F, we distinguish between types and terms. Types are defined by the following BNF: \begin{align} A, B ::=&~\alpha && \text{(type variable)} \\ &|~A \rightarrow B &...
318 views

### Normal order sequencing vs applicative order sequencing

I'm trying to understand this lecture, section 2.7. Why would the normal order sequencing print out "hello" "world" and not ...
75 views

### What is a “model” of lambda calculus?

I know about the concept of the "model" of a logical proposition in the context of mathematical logic: It is a mathematical structure in which that proposition is true. However, it's not clear to me ...
384 views

### Can type information be encoded in the untyped lambda calculus?

I'm going to take the few pieces of knowledge I have about lambda calculi and ask a pair of very uninformed questions :-) Is it possible to "embed" the corners of the lambda cube within the untyped ...
113 views

### How to decide the scope of the following lambda expression?

I am having a difficulty in deciding the scope of the left-most lambda in the following expression. Ī»x.x(Ī»uv.v)(Ī»ab.a)(Ī»cd.c) I have learnt that we should put ...
56 views

### Is there a systematic way to know when to alpha-transform free variables?

So, using Church numerals, we define $3 = {\lambda} f. {\lambda}x.f(f(f(x)))$, and $4 = {\lambda} f. {\lambda}x.f(f(f(f(x))))$. We can then add with an expression like $3\ g\ (4\ g\ z)$ And ...