Episode #125 of the Stack Overflow podcast is here. We talk Tilde Club and mechanical keyboards. Listen now

Questions tagged [lambda-calculus]

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

74 questions with no upvoted or accepted answers
Filter by
Sorted by
Tagged with
21
votes
0answers
600 views

Can a calculus have incremental copying and closed scopes?

A few days ago, I proposed the Abstract Calculus, a minimal untyped language that is very similar to the Lambda Calculus, except for the main difference that substitutions are ...
10
votes
0answers
308 views

Advantages of algorithm W over algorithm J for type inference in Hindley-Milner type system

According to A modern eye on ML type inference Furthermore, for some unknown reason, W appears to have become more popular than J, even though the latter is viewed—with reason!—by Milner as ...
10
votes
0answers
132 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) ...
9
votes
0answers
118 views

Using naturality to prove $f: \forall\alpha. \alpha\times\alpha\to\alpha$ must be a projection

Suppose we have a System F term $f : \forall \alpha. \alpha\times\alpha\to\alpha$, interpreted in a parametric model which is a bicartesian closed category. I was wondering if in such context it is ...
6
votes
0answers
31 views

Unbounded-time programs in lambda calculus?

The Turing machine model has been extended to “infinitary turing machines”, which are Turing machines that can perform a countably and uncountably infinite amount of computations in finite time. Is ...
6
votes
0answers
70 views

Are there simple core languages which are consistent and expressive?

The Calculus of Constructions is a very simple core functional language with dependent types. Per curry-howard isomorphism, it could, potentially, be very useful for writing programs and proofs. It, ...
6
votes
0answers
683 views

Barendregt's Variable Convention: what does it mean?

Barendregt's Variable Convention: If $M_1,...,M_n$ occur in a certain mathematical context (e.g. definition, proof), then in these terms all bound variables are chosen to be different from the free ...
6
votes
0answers
287 views

Capture Avoiding Substitution of multiple variables at once

In articles you often find the terminus "capture avoiding substitution" that saves the author(s) from the tedious process to re-define a recursive function -including alpha-conversion and the ...
6
votes
0answers
58 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. ...
6
votes
0answers
93 views

Bounded existential polymorphism

In his "Types and Programming Languages", Pierce, at the very end, presents the most powerful system in the book: $F^{\omega}_{<:}$. He, however, does not explain how bounded existential ...
5
votes
0answers
64 views

Difference between “functional programming languages” and “lambda calculus based languages”?

In "Can programming be liberated from the Von Neumann Style?", John Backus states: The main reason FP systems are considerably simpler than either conventional languages or lambda-calculus-based ...
5
votes
0answers
81 views

How could one write typing rules with variables defined at call-site?

I'm trying to write typing rules for a simple language, which is basically a lambda calculus with SSA-like $\phi$-nodes, which basically exchange formal parameters for actual parameters. For ...
5
votes
0answers
133 views

Characterization of alpha-equivalence in languages with bindings

Following up on this post denoting $(x \leftrightarrow y)$ the permutation of $x$ and $y$ and $P[x \leftrightarrow y]$ the term obtained from the term $P$ by permuting $x$ and $y$ (so for example if $...
5
votes
0answers
164 views
5
votes
0answers
403 views

Test cases for λ-Calculus

For testing automated theorem provers we have Seventy-Five Problems for Testing Automatic Theorem Provers by Pelletier. Are there any such standard/well regarded tests for a λ-calculus that verify ...
4
votes
0answers
46 views

Does type-1 lambda calculus exist?

I'm interested in the intersection of linguistics and computer science, I've been reading on Chomsky hierarchy, and would like to know if there exist lambda calculus types that are equivalent to the ...
4
votes
0answers
47 views

How shall I understand the definitions of `let` expression?

let as used in programming languages is defined in lambda calculus as per https://en.wikipedia.org/wiki/Let_expression#Let_definition_defined_from_lambda_calculus ...
4
votes
0answers
62 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 ...
4
votes
0answers
744 views

Examples of the axes of the lambda cube

The Wikipedia article https://en.m.wikipedia.org/wiki/Lambda_cube is difficult to assimilate. I think examples (code snippets) that demonstrate each refinement might help clarify. For instance, a ...
4
votes
0answers
496 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 ...
4
votes
0answers
36 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 ...
4
votes
0answers
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 ...
3
votes
0answers
49 views

Calculus of constructions, type-in-type and recursion

Does adding type-in-type to the calculus of constructions lead to (general) recursion? Such that one can write the Y combinator.
3
votes
0answers
71 views

Type inference for System F-omega

There have been some nice papers about simple type inference for System F: "HMF: Simple Type Inference for First-Class Polymorphism", "Practical type inference for arbitrary-rank types", and "Complete ...
3
votes
1answer
106 views

Efficient algorithm to determine if a lambda calculus term is equivalent to one without a given free variable

Consider the following problem: given a lambda calculus term $t$ and free variable $v$ determine whether $\phi(t,v)$, where $\phi(t,v) := \exists t'. t' \equiv t \land v \notin FV(t')$. This problem ...
3
votes
0answers
189 views

CFG for $\lambda$-calculus with minimal parentheses

The typical presentation of the syntax of the $\lambda$-calculus is as an ambiguous CFG (or BNF) like the following: $$T \rightarrow \lambda X . T \mid T ~ T \mid X \mid (T)$$ Where we permit $X$ to ...
3
votes
0answers
45 views

Expressing definite clauses (Horn rules, logic programming) in lambda terms?

There is paper which expresses lambda terms in the terms of logic programming http://www.cse.unt.edu/~tarau/teaching/PL/docs/dbx.pdf Is there conversion in the other direction - expressing definite ...
3
votes
0answers
120 views

Semantic parsing with Grammatical Framework - is this possible?

So far I have learned about categorial grammars, type logical grammars and formal semantics of natural language, the relevant tools are Cornell Semantic Parsing Framework https://github.com/clic-lab/...
3
votes
0answers
58 views

Is the number of tests needed to know if a program computes the identity computable?

Given a $\lambda$-term $t\in \Lambda$ and an integer $k$, we say that $t$ behave likes the identity when applied to $k$ if $tk\to_\beta^*k$ (where the integer is represented as a church numeral). We ...
3
votes
0answers
88 views

How to translate lambda calculus into (first-order, modal) logic, is it possible at all?

It is possible (using formal semantics) to translate natural language sentences into lambda expressions. So, is it possible to translate those lambda expressions into some logic, e.g. into first-order ...
3
votes
0answers
144 views

$\lambda$-terms equal modulo $\alpha$-renaming, is this an equivalence relation?

Want to clarify few things. It is said that two $\lambda$-terms are equal up to renaming of bound variables, such as $\lambda x.x$ equals $\lambda y.y$, so I think it is a relation actually, about ...
3
votes
0answers
115 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 λσ ...
3
votes
0answers
201 views

How does this addition for Church numerals work with Y combinator?

I am currently preparing for an exam. In one of the old exams, you have to create a $\lambda$ expression $add$ that can add two church numerals. But the church numerals are not the usual ones, but ...
3
votes
0answers
45 views

How do stable functions 1 => 1 relate to Bool?

One way to interpret the (simply typed) lambda calculus is via coherence spaces (Proofs and Types, chapter 8). For example, we can consider the space containing token element ($\mathbf{1}$) and the ...
3
votes
0answers
154 views

Is there any programming system that enables reversible computations?

Better explained with examples, I need a programming system with the following characteristics: ...
2
votes
0answers
19 views

Is $\Gamma \vdash x x : T$ possible in the simply typed lambda calculus?

Is $\Gamma \vdash x x : T$ possible? This problem appears on page 104 of Benjamin Pierce's "Types and Programming Languages". My conclusion is that it is was the case then we would get $x: T_1 \to ...
2
votes
0answers
36 views

Are isomorphic (untyped) lambda expressions semantically equivalent?

"Isomorphic" is defined as having the same shape of syntax trees and the same bindings of variables. However, the variable names might be completely different. In other words, it is to say that we ...
2
votes
0answers
30 views

Construct a lambda term from a Böhm tree

Given an acyclic graph, how can I build a lambda calculus term such that this graph is the term's Böhm tree? If the Böhm tree is a finite tree (so the result is a strongly normalizing term). If the ...
2
votes
1answer
87 views

Elegant algorithm to semi-decide if two lambda calculus terms are equivalent

Given two lambda terms $t_1$ and $t_2$, it is semi-decidable if they are equivalent (i.e. can be rewritten as each other using alpha, beta, and eta conversions). An algorithm to do this is to try ...
2
votes
0answers
52 views

Are there any interesting terms in pure LF or $\lambda\Pi$?

In my searching, I've seen that if Church numerals are encoded in a dependently typed Lambda calculus, that we can't derive induction or that $0 \neq 1$. I know that LF and the dependently typed ...
2
votes
0answers
35 views

Understanding First conversion rules from church's lambda bible

While going through Church's text on Lambda calculus , I cam across the first set of conversion rules . Before writing out my query I would like to put the notation that church has used for ...
2
votes
0answers
61 views

Term for weak head normal forms that cannot be reduced in any environment

In my understanding, a lambda expression is a normal form (NF) when it has no redexes. For instance, $\lambda x.x$ is a NF, but $(\lambda x.x)y$ is not. A lambda expression is a weak head normal form (...
2
votes
0answers
52 views

Automatic learning/discovery of logics

Are there efforts to automatically discover new logics? Logics are simple structures - they have formal language, deduction rules, semantics and certain properties that are proved or discarded for ...
2
votes
0answers
66 views

Lambda calculus closure expansion

The set of lambda calculus expressions $Expr$ is generated by the grammar $$ Expr \ni e ::= x \mid \lambda x\ldotp e \mid e_1 e_2 $$ We can define an interpreter without explicit substitution by ...
2
votes
0answers
185 views

Practical usage of the λ-calculus self-interpreter and the self-reducer?

I came across the paper: "Efficient Self-Interpretation in Lambda Calculus" by Torben Mogensen, 1994: http://repository.readscheme.org/ftp/papers/topps/D-128.pdf It talks about the intepreter $E$ ...
2
votes
0answers
59 views

Can't evaluate original Y combinator, two other variants do work, what do I miss?

I have made an evaluator of Lambda expressions. I tried to do Y combinator, but for some reason I can't get the original one working: $$λf.(λx.f \space (x \space x)) \space (λx.f \space (x \space x))\...
2
votes
0answers
195 views

Recursive definitions, How it is done?

I read that recursive definitions, refer to the definition of a function in that function body, cannot be done in $\lambda$-calculus, but recursion can be achieved by using $Y$ combinator. As I know, ...
2
votes
0answers
99 views

Growth of non-terminating beta reductions in lambda calculus

There are some terms in lambda calculus that don't really have a normal term. My question is for a term like the following: $$T \overset{def}{=} \lambda f. (\lambda x. \; f \; (f \; (f \; x)))$$ $T$ ...
2
votes
0answers
29 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 ...
2
votes
0answers
236 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} =...