# Tagged Questions

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

33 views

### call by value: what is a value?

In the 'call by value' evaluation of lambda-calculus, I am bit confused with 'value'. On page 57 of the book Types and Programming languages, it is said: The definition of call by value, in ...
39 views

### Common name for inverse of beta reduction

For some transformation, I am currently working on, it is useful to "pull out" subexpressions and replacing them with variables. i.e. $\textbf{transform}(42 + 3 * 4) = (\lambda x. 42 + x) (3*4)$ ...
44 views

### How can I study the nature of the structure of evaluation of function in lambda calculus?

I am specifically focusing on lambda calculus, following this paper: A Tutorial Introduction to the Lambda Calculus. Suppose we have three functions that represent the natural numbers 0 and 1, and a ...
12 views

### The range of functions defined by pure lambda terms

Consider a full set-theoretic model of the simply typed $\lambda$-calculus with infinite base types. Say that an element in this model is pure if it is the semantic value of some closed pure term in ...
48 views

### When can you “invert” an equation in the lambda calculus

Suppose that $M$ is a full model of the simply typed lambda calculus. Suppose each base type is infinite. Now suppose that $f$ and $g$ are two functions in $M$ (not necessarily in the same domain) ...
64 views

### Basis sets for combinator calculus

It is well known that the S and K combinators form a basis set for combinator calculus, in the sense that all other combinators can be expressed in terms of them. There is also Curry's B, C, K, W ...
112 views

### What functions can combinator calculus expressions compute?

A combinator expression (let's say in the SK basis) can be thought of as a function that maps combinator calculus expressions to combinator calculus expressions. That is, one can think of an ...
51 views

64 views

### Lambda Calculus Argument Delimiter

So I've been looking into lambda calculus on and off for months simply trying to understand the numerical system and the successor function. I understand that it's basically just argument evaluation, ...
85 views

### How does this left-associative recursive descent parser work?

For personal enlightenment, I'm trying to write a recursive descent parser for lambda calculus without abstraction, i.e., just identifiers and function application. The BNF grammar that describes the ...
241 views

### Why injection into sum type apparently leads to ambiguity?

I have been reading Benjamin Pierce's Types and Programming Languages, plus a couple of course notes on type systems and typed $\lambda$-calculus, and there is one thing I don't get: it seems that ...
32 views

### Efficient explicit-substitution calculus

I've been looking at various calculus with explicit substitutions for efficient implementation of normalisation of terms in the lambda calculus. AFAICT there are basically two approaches: the λσ ...
6k views

### What does the “Lambda” in “Lambda calculus” stand for?

I've been reading about Lambda calculus recently but strangely I can't find an explanation for why it is called "Lambda" or where the expression comes from. Can anyone explain the origins of the term?...
60 views

### What are the simplest known algorithms to compute PI?

There are many algorithms that compute PI. Some are obviously complex, involving huge formulas and constants. Some formulas are not that complex, but involve operators such as ...
51 views

79 views

### Do Self Types make the Calculus of Inductive Constructions obsolete?

Self Types are an extension of the Calculus of Constructions [1] that allow the language to express algebraic datatypes encoded through the Scott Encoding. The Scott Encoding provides one the ability ...
71 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 &...
74 views

### Error in solution in Types and Programming Languages?

I'm reading Types and Programming Languages and trying to understand the solution to exercise 5.2.4 on untyped lambda calculus / Church numerals: Define a term for raising one number to the power ...
210 views

### Can every program be parallelized infinitely and automatically?

In my previous question ( Can Turing machines be converted into equivalent Lambda Calculus expressions with a systematic approach? ), I got the answer that it is indeed possible. And as I have read ...
915 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 ...
90 views

### Which calculus is based on first-order functions and is Turing complete?

Which calculus is based on first-order functions and is Turing complete? I know of calculi which are Turing complete, but based on higher-order functions: Lambda calculus SKI combinator calculus ...