λ-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

0
votes
0answers
6 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
25 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
50 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
48 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
55 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
70 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
238 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
26 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 λσ ...
56
votes
1answer
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 ...
2
votes
0answers
51 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
48 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
323 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
120 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
22 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
66 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
56 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
49 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
230 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 ...
3
votes
1answer
45 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
23 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
27 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
41 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
259 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
58 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
46 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: ...
0
votes
0answers
27 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
35 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
37 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
40 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
11 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
31 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 ...
4
votes
1answer
76 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
69 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
67 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
199 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
897 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
88 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
167 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 ...
5
votes
0answers
34 views

Is it possible to reduce functional equations to SAT?

The problem of finding a solution for functional equations can be defined as: Let A0, A1, A2... An, B0, B1, B2... Bn, X be terms of the lambda calculus, all terms known, except for X, unknown. ...
4
votes
3answers
55 views

Is there any meaning behind the classification of “λ-terms” in classes such as “church number” and “church list”?

λ-calculus terms can be informally/intuitively categorized, such as: (λ f x . (f (f (f x))))) is a church natural (3) ...
0
votes
1answer
102 views

Why are functional programs considered slower than procedural counterparts asymptotically, if the opposite appears true?

I've read and been told way too many times that functional algorithms and data structures have an obligatory O(log(N)) slowdown in respect to their procedural ...
16
votes
5answers
2k views

Why can functional languages be defined as 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 ...
8
votes
1answer
114 views

Are combinatory logic terms always larger?

So there is an algorithm to convert lambda calculus terms to combinatory logic using SK combinators. It produces things that explode in size. I would like to know more about this explosion in size. I ...
6
votes
0answers
22 views

Is there any type system which can assign a type to any halting lambda calculus term? [duplicate]

Some lambda terms, such as the church number 3: (f x -> (f (f (f x)))), are easily typeable on the simply typed lambda calculus. Others, such as ...
1
vote
1answer
74 views

Computer Programs and lambda terms without normal form

λ-calculus an ideal mathematical model in which to interpret programs. A program can be interpreted as a lambda term, and the term can have or not have a normal form. What role the terms without ...
0
votes
1answer
59 views

Can polymorphism be simulated by lazy type operators?

In the definition of lambda cubes, type polymorphism is distinguished from type operators/constructors. I have the nagging feeling that type polymorphism can be constructed through type operators ...