Questions tagged [lambda-calculus]

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

408 questions
Filter by
Sorted by
Tagged with
39 views

Rules for consistency with mutual inductive families?

I'm trying to use a proof assistant to define a type and a relation that are mutually dependent on each other: ...
57 views

Lambda terms forming non-abelian groups

I was wondering what kind of groups could be constructed with Lambda terms, where the group operation is application? For example, $a* b =c$ would mean $ab\to_{\beta}^{*} c$. Is this even possible? ...
36 views

49 views

What is meant by a full abstract model of a lambda-calculus like language?

The simply typed lambda-calculus with numbers and fix has long been a favorite experimental subject for programming language researchers, since it is the simplest language in which a range of subtle ...
110 views

What is meant when we say that divergence is the only side-effect of the lambda-calculus?

In the simply typed lambda-calculus, I was told that behavioral equivalence is taken in terms of divergence because "divergence is the only side-effect of such language". How should I understand ...
43 views

22 views

Is it possible to deduce type from the lambda form?

I was continuing the exploration of lambda world this summer. When I take a look at the simply typed lambda calculus, it looks like there is no use for usual chuch numerals and boolean forms anymore. ...
55 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 ...
50 views

Is this lambda abstraction created as a generator of a recursive function?

In lambda calculus, a recursive function $f$ is obtained by $$f = Y g$$ where $Y$ is the Y combinator and $g$ is the generator of $f$ i.e. $f$ is a fixed point of $g$ i.e. $f == g f$. In The ...
55 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 ...
54 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.
35 views

41 views

45 views

Why 'let' can not be reduce to a lambda application in (extended) Calculus of Constructions

I do not understand the difference highlighted in the chapter 2.5 of the book Theorem Proving in Lean: Notice that the meaning of the expression let a := t1 in t2 is very similar to the meaning of (...
90 views

What are the other language models of computation similar to lambda calculus?

I hope this question makes sense, but I was wondering if there are other models of computation similar to lambda calculus that you can use to build up axiomatic mathematical and logical fundamentals ...
136 views

Check if a lambda constructor is well-typed

In basic type inference for 𝜆-calculus with parametric polymorphism à la Hindley–Milner, when can we say that we cannot give a type to a lambda constructor? For example (λx.λy.y(x\ ...
57 views

Variable Capturing With Repetition of Variable Name

I am very confused as to which variables are captured by which λ in the example below: (λa.λb.(λa.a)aba)(ab) I am new to lambda calculus and the repetition of ...
106 views

Are there lambda-calculus functions which always output booleans, but are not constant functions?

In labmda calculus, true = $\lambda x,y.x$ and false = $\lambda x,y.y$. Is there a term $f$ such that for any other term $x$, $f x$ normalizes to true or false BUT $f$ does not have the same output ...
41 views

Must a function in lambda-calculus which inputs a boolean function be defined in a certian way?

This question is my best attempt to get at a more general question about what one can get from terms in the lambda calculus. Using the church encoding, we define booleans by \$\texttt{true} = \lambda ...