# Questions tagged [lambda-calculus]

Church's formal system used in computatability, programming languages and proof theory to represent effective functions, programs and their computation, and proofs.

265 questions
Filter by
Sorted by
Tagged with
142 views

### Connection between strong normalization of the simply typed λ-calculus, and cut elimination for propositional logic

What is the precise connection between: strong normalization of the simply typed $\lambda$-calculus, and cut elimination for (intuitionistic) propositional logic (limited to implication) in “sequent ...
42 views

### Variable opening in locally-nameless representation

Although similar to a previously unanswered question, my query focuses on a different aspect of normalization. I'm trying to adjust the proof of strong normalization of STLC, given in Jeremy Avigad's ...
357 views

### Locally-nameless normalization

This paper on locally-nameless (Charguéraud, Arthur: The locally nameless representation, Journal of Automated Reasoning (2012): 1-46) describes how to perform beta-reduction by "opening", but it's ...
79 views

### Can lambda-calculus, or other formal systems / calculi, be represented using set theory?

Background: I'm a fresh grad student looking into interesting ideas I have. I do not have any theoretical computer science background beyond basic Theory of Computation stuff from undergrad. If I have ...
74 views

### What is the type of the lambda term $\lambda a.a(\lambda yt.t)(ya)$?

I was given an exercise that asked me to assign a simple type to the lambda term: $$\lambda a.a(\lambda yt.t)(ya)$$ but I couldn't find one, furthermore, the lambda term seems untypable to me ...
124 views

### Locally nameless representation implementation

ORIGINAL: I am programming a functional compiler and found out about locally nameless representation (using de brujin indeces for bound variables and names for free variables). I just don't understand ...
156 views

415 views

### Regular languages in lambda calculus

With Turing machines, by imposing certain restrictions on the form of the transition function, one can get a machine that accepts only regular languages. I am wondering what is the counterpart in ...
83 views

### Nominal Tree Languages i.e. with Binders and Infinite Symbols?

I'm wondering if there has been any research done into automata that accept languages of trees that can bind arbitrary variables, and are considered equal under alpha equivalence. I've found so far: ...
1k views

### Can typed lambda calculi express *all* algorithms below a given complexity?

I know that the complexity of most varieties of typed lambda calculi without the Y combinator primitive is bounded, i.e. only functions of bounded complexity can be expressed, with the bound becoming ...
1 vote
67 views

171 views

### Intuitive way to handle variable binding

Suppose we have an algebraic datatype parameterised by a type variable name, e.g. ...
79 views

### Expressive power of lambda-calculus with restricted application

Consider a syntactic restriction of the (untyped) $\lambda$-calculus in which an application cannot have another application as an immediate subterm. More precisely, restricted terms ($R,S,...$) and ...
64 views

### Are there any references for this theorem of Lercher?

Let $\Delta = \lambda x.(x)x$ and consider $\Omega = (\Delta)\Delta$. Then $\Omega$ is exactly the only $\lambda$-term of the form $(\lambda x.t)v$ such that $(\lambda x.t)v=t\{v\ /\ x\}$. Does ...
88 views

### Can a normal form term be extensionally equivalent to a term with no WHNF?

For convenience I'm using using the combinators SKIBCMTV I notice that it's possible to have a normal-form term extensionally equivalent to a term which has no normal form: ...
163 views

### What is wrong with the "obvious" approach to function extensionality by providing context-aware rewrites?

There is an obvious, dirty and probably wrong approach that allows one to prove function extensionality in a straight-forward manner: provide an equality primitive with a context-aware rewrite. For ...