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

learn more… | top users | synonyms

3
votes
1answer
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 ...
3
votes
1answer
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)$ ...
4
votes
1answer
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 ...
2
votes
0answers
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 ...
6
votes
0answers
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) ...
7
votes
0answers
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 ...
11
votes
1answer
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 ...
4
votes
1answer
51 views

Combinator equivalent to eta conversion

In lambda calculus, one can prove that two expressions compute the same function if they are equivalent under both beta reduction and eta conversion, where eta conversion consists of eta reduction, $$ ...
2
votes
1answer
29 views

Is there an implementation of higher kinded types in typed lambda calculus?

I can see that we can do higher kinded types ( * -> *) -> * in Scala and Haskell and other languages. I'm looking for a simpler vanilla implementation of just ...
0
votes
1answer
31 views

Is function application actually a memory manipulation algorithm?

I thought about how in lambda calculus (and many implementations of functional programming languages) function (lambda) application and lambda itself, as a construct, are "primitive things", usually ...
4
votes
2answers
62 views

Lambda Calculus inductive substitution definition

I'm reading Lambda-Calculus and Combinators: An Introduction, and there's the following definition of $\lambda$-substitution: $FV(P)$ stands for the set containing all free-variables from $P$. I ...
3
votes
0answers
51 views

Normal order sequencing combinator - why does it work?

Notes on lambda calculus (part 2.7) and book Programming Distributed Computing Systems: A Foundational Approach by Varela present the sequencing combinator for normal order reduction: $$\mathit{Seq} =...
2
votes
2answers
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, ...
2
votes
0answers
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 ...
5
votes
1answer
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 ...
3
votes
0answers
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 λσ ...
60
votes
2answers
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?...
2
votes
0answers
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 ...
4
votes
1answer
51 views

Presentation of context rules for the lambda-calculus

Reading Chris Hankin's book, "An Introduction to Lambda Calculus for Computer Scientists", I learnt that the rules for reductions in the pure $\lambda$-Calculus are the $\beta$-reduction rule, $$(\...
4
votes
3answers
344 views

What is the purpose of the SKI combinator calculus(or even lambda calculus)? What are some real life examples of its use?

I understand what it is, but I don't see how it is any use for algorithms or anything. Maybe I am missing something. I need someone to give me an example of how it can be used so I can understand it ...
5
votes
2answers
125 views

Uses of the type Unit

The Unit type is a singleton type containing the constant unit. In functional languages with side effects, ...
2
votes
1answer
23 views

How can I represent state or environment in the $\lambda$-Calculus?

I have seen in different tutorials how to represent numbers and booleans in the pure $\lambda$-Calculus, and how to define some arithmetic and logic operations. But what if I want to represent other ...
5
votes
1answer
71 views

How precise is the statement “STLC is the internal language of CCCs”?

I'm studying some basic category theory in the context of type theory and came across the statement "simply typed lambda calculus is the internal language of cartesian closed categories". However ...
1
vote
2answers
58 views

How to write a closed term with this type?

X→Y →(X+Y)×Y I'm confused about how to get the type (X + Y). If I assume ...
4
votes
3answers
52 views

Is Applicative-order and Normal-order evaluation model's definition contradictory as per sicp text book?

As per this explaination, it defines applicative and normal order evaluation in one form saying: This alternative "fully expand and then reduce" evaluation method is known as normal-order ...
6
votes
2answers
232 views

Generating constraints to solve dependently-typed metavariables?

In dependent-types, Miller pattern unification is used to solve a decidable fragment of higher-order unification. This allows dependently-typed languages to contain metavariables or implicit arguments....
3
votes
1answer
47 views

premiss of reduction rule (abst) of pure type systems

$$(abst) \:\frac{\Gamma, x: t_1 \vdash t_2: t_3 \quad \Gamma \vdash (x: t_1) \to t_3: s}{\Gamma \vdash (x: t_1. t_2): (x: t_1) \to t_3}$$ In this rule, why is $(x: t_1) \to t_3$ required to be an ...
0
votes
1answer
25 views

Elimination rule for the equality type aka J axiom

I'm implementing a interpreter for lambda calculus, and now I want to add the equality type. The introduction rule for it is easy, but the elimination rule is rather obscure for me. I found this ...
0
votes
1answer
35 views

Lambda Calculus Reduction Examples

I'm still trying to get the hang of lambda calculus: I completed simplified some of these already but am lost on the last two. I did so far: \begin{align*} (\lambda x.x)y &\to y\\ (\lambda ...
0
votes
1answer
29 views

Why does λz.zq reduce to q?

The way I see it, it should not be further reducible. I'm thinking λz.zq is like lambda z: z(q) # Python, not lambda calc ...
3
votes
1answer
49 views

Iota combinator and implicational propositional calculus

There is are two esoteric languages with minimally functionally complete operators, iota and jot, that are closely related to SK combinators. I'm attempting to understand the relationship between ...
8
votes
2answers
270 views

Universal/existential quantification?

I'm struggling to understand the purpose of universal and existential quantification of types. I'm playing around with writing a toy language based on the calculus of constructions. I've been reading ...
1
vote
1answer
64 views

Recognizing primitive recursion

I am trying to write a program to recognize if a given lambda calculus expression is primitive recursive. I believe that a general algorithm to do this does not exist, but I am interested in the most ...
1
vote
1answer
54 views

primitive recursion in the lambda calculus

I am having trouble finding out what a primitive subset of the lambda calculus would look like. I reference primitive recursion as shown here: "https://en.wikipedia.org/wiki/...
0
votes
0answers
32 views

Poly-variadic Y combinator

I have written a lambda calculus interpreter, and it seems to work. I cant find the combinator for something I want though. I want to be able to define an arbitrary number of mutually recursive ...
1
vote
1answer
38 views

primitive recursion on untyped lambda calculus

Does a definition of primitive recursion exist for the untyped lambda calculus? Does the definition of primitive recursion require typing for natural numbers? The only definitions I can find are for ...
0
votes
1answer
44 views

Given a λ-term, can I decide which machine model I need to express it?

I am having a hard time figuring out the specific relationship, of various things in computability. So we have a hierarchy of machines, with a (real life) upper bound of Turing machines, moving on ...
2
votes
1answer
42 views

Is an expression in normal form if terminates on normal order but not applicative?

Just wondering if something like this... (λx. y)((λx. (x x))(λx. (x x))) Would be considered to be in normal form since it terminates with y if done by normal ...
3
votes
1answer
41 views

Conditionals with normal order evaluation

From what I've read, conditionals (like the cond statement in lisp) do not need to be primitive if normal order evaluation is used. Using lambda calculus and normal order evaluation, how can you ...
0
votes
0answers
41 views

Constructing a Turing Machine with Lambda Calculus

I'm interested in the implementation of a Turing Machine (deterministic) in Lambda Calculus. How should I proceed to do this? I am not sure on how to start since I must represent the state and ...
1
vote
0answers
15 views

What is the intuition behind a λ-term being EAL-Typeable?

λ-terms can be split in two categories: EAL and non-EAL typeable terms. It is known not only that EAL-typeable terms can be reduced to normal form in polynomial time, but that the reduction can be ...
1
vote
1answer
34 views

Application Ambiguity in Untyped Lambda Calculus

So, untyped lambda calculus has the following formal grammar for its terms: $$e::= x \mid \lambda x . e \mid e_1 e_2$$ Usually this is presented in some ML-esque language as (using de Bruijn indices)...
4
votes
1answer
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 ...
2
votes
1answer
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 &...
5
votes
1answer
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 ...
4
votes
3answers
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 ...
5
votes
3answers
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 ...
2
votes
2answers
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 ...
6
votes
1answer
176 views

Can a functional language be homoiconic?

According to the wikipedia page on homoiconicity: In a homoiconic language the primary representation of programs is also a data structure in a primitive type of the language itself. I was ...
4
votes
0answers
20 views

Computational complexity of emulating (untyped) λ-calculus with a queue machine

I am looking for bounds - both lower and upper - on the time, spacial, and state/symbol (i.e. number of states and symbols required) complexity of simulating the (untyped) λ-calculus with a queue ...