Questions tagged [lambda-calculus]

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

Filter by
Sorted by
Tagged with
4
votes
1answer
29 views

Explain auto continue passing style transformations

Recently I saw 3 cps transformation rules, but no explanations were given. expressions: $e :=x\left|e e^{\prime}\right| \lambda x \cdot e$ rules: $$ \begin{array}{l}{[[x]]=\lambda \kappa \cdot \...
2
votes
0answers
32 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 ...
1
vote
0answers
27 views

How is knowledge of lambda calculus applicable in Computer Science and Machine Learning? [closed]

If I want to do research in computer science and machine learning, is it important to have a well-rounded understanding of lambda calculus?
4
votes
1answer
40 views

What untyped term inhabits induction on natural numbers in CoC?

Induction on Church-encoded natural numbers (which I will call indNat) can not be defined within the Calculus of Constructions. If we assumed ...
2
votes
1answer
61 views

Lambda Calculus as a branch of set theory

This answer to a question about whether C is the mother of all languages contained an interesting tidbit that I am curious about: The functional paradigm, for example, was developed mathematically (...
3
votes
1answer
38 views

Uncomputably coded model of computation

There are many different but equivalent models of computation. I assume their equivalence is shown by coding input of one model to the input of the other model and making an argument why should there ...
0
votes
1answer
44 views

Advantages of Lambda calculus over Turing machine and vice versa [closed]

What kind of advantages does Lambda calculus have over Turing machine, and vice versa?
28
votes
2answers
4k views

Is Lambda Calculus purely syntactic?

I've been reading for a few weeks about the Lambda Calculus, but I have not yet seen anything that is materially distinct from existing mathematical functions, and I want to know whether it is just a ...
0
votes
0answers
45 views

How to collect free/bound variables in Lambda Calculus?

I am building a simple interpreter for untyped lambda calculus, currently trying to implement alpha-reduction. According to this document on LC: Alpha-reduction is used to modify expressions of ...
0
votes
3answers
75 views

Is λx. a valid Lamda Calculus abstraction?

For demonstration purposes I was wondering about some very easy to grasp LC abstractions and I came to the idea of a function that simply eats its argument, and nothing more. If you apply λx. (Yes ...
0
votes
1answer
33 views

Find typing derivation of STLC term with reference types

The problem is to find the typing derivation of a term of the call-by-value STLC extended with reference types. The evaluation and typing rules for this language is given in Types and Programming ...
2
votes
2answers
56 views

Writing a grammar for lambda calculus

I'm trying to write a context-free grammar (to be feeded to lark) for parsing lambda calculus expressions. Basic version of it, as presented by most sources, looks like: ...
6
votes
1answer
87 views

Can all regular tree types be expressed as $\mu$ types?

In "Types and Programming Languages", Pierce gives a translation from recursive types ($\mu$ types) to types expressed as regular trees: possibly infinite trees, but with finitely many distinct ...
2
votes
0answers
32 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
1answer
53 views

Optimization of Church-encoded booleans in System F

I can encode booleans in pure lambda calculus like this: type Bool = forall t. t -> t -> t true : Bool = \x y -> x false : Bool = \x y -> y Is ...
4
votes
1answer
48 views

Multi-prompt delimited continuations in terms of single-prompt delimited continuations

Let's call the two languages in question (untyped lambda calculus with single or multiple prompt delimited continuations) L_delim and L_prompt. Is it possible to express multi-prompt delimited ...
10
votes
2answers
224 views

Is the SK2 calculus a complete basis, where K2 is the flipped K combinator?

Specifically, if I defined a new $K_2$ as $$K_2 = \lambda x. (\lambda y. y)$$ instead of $$K = \lambda x. (\lambda y. x)$$ would the $\{S, K_2,I\}$-calculus be a compete basis? My guess is "no," ...
1
vote
1answer
36 views

Give a computation of the expression to normal form (Lambda calculus)

Past exam question: What my understanding of B-reduction is : Find all occurrences of the parameter in the output, and replace them with the input and that is what it reduces to ...
1
vote
2answers
50 views

lambda calculus with church numerals

today I found this term in our exercises: ((^fx.f(f(f x)) ^gy.g(g y )) ^z.z + 1) (0) I am quit unaware how to solve this type of question. I know this is the church numeral 3 , 2 , the identity ...
6
votes
1answer
88 views

How do we know $\neg \neg LEM$ isn't provable in MLTT?

I've been trying (fruitlessly) to prove something which I now know is not provable. Take the following definitions: $$LEM \equiv \prod_{A : Type} \neg A \vee A$$ $$DNE \equiv \prod_{A : Type} \neg \...
4
votes
1answer
42 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 (...
1
vote
2answers
84 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 ...
4
votes
2answers
117 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\ ...
2
votes
1answer
56 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 ...
5
votes
2answers
96 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 ...
2
votes
1answer
38 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 ...
6
votes
0answers
30 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 ...
2
votes
0answers
26 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 ...
-1
votes
1answer
24 views

Reduce to Beta Form Verification

What is the normal form of the following lambda term? I'm stuck between two answers and I just wanted to know which one is correct. $$\lambda y. (\lambda x.x)\ y$$ Possible Answer 1: $\lambda x.x$ ...
1
vote
1answer
32 views

What do the symbols M and N mean in this definition of lambda terms?

I am learning lambda calculus from the book https://www.irif.fr/~mellies/mpri/mpri-ens/biblio/Selinger-Lambda-Calculus-Notes.pdf and do not understand the meaning of the following symbols. The ...
0
votes
2answers
47 views

No Lambda Normal Form

How can we show that the term $\Omega = (\lambda x.x\ x)\ (\lambda x.x\ x)$ does not have a normal form? Building on this, what is an example term different than Omega that is not normalizing (meaning ...
5
votes
0answers
58 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 ...
1
vote
1answer
55 views

What's a general rule for this little lambda calculus identity?

I've been fiddling around with a project that does some normalization of lambda calculus(-like) expressions and I stumbled upon that (λ λ ... λ n (n-1) ... 2 1) (...
4
votes
0answers
52 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 ...
1
vote
1answer
95 views

What does all uppercase letters mean?

I am reading https://www.irif.fr/~mellies/mpri/mpri-ens/biblio/Selinger-Lambda-Calculus-Notes.pdf and would like to know, what the following statement means: ...
2
votes
1answer
41 views

Church numerals without functions

This is really a second part to my first question, but I felt that this was different enough from the first part that it merited its own question. So, using Church numerals, we define $3 = {\lambda} ...
3
votes
2answers
48 views

Is there a systematic way to know when to alpha-transform free variables?

So, using Church numerals, we define $3 = {\lambda} f. {\lambda}x.f(f(f(x)))$, and $4 = {\lambda} f. {\lambda}x.f(f(f(f(x))))$. We can then add with an expression like $3\ g\ (4\ g\ z)$ And ...
3
votes
1answer
48 views

What are different ways to provide a semantics to a language?

Suppose you have 1. a grammar for terms of a language; 2. type-assignment rules, 3. a set of reduction rules. You want to prove that your language is adequate for mathematical reasoning. If I ...
1
vote
1answer
57 views

lambda expressions, parenthesis, and order of application

I am building a lambda applicator in Java, and I have uncovered a bit of misunderstanding. Either my question at the bottom is what I am asking, or something in the build-up below is wrong. Either ...
1
vote
1answer
35 views

Tailrecursive definition for a function

In an exam I took we were asked to provide a tailrecursive definition of a recursive function. I failed miserably and the provided solution makes absolutely no sense to me. If anyone could explain ...
0
votes
0answers
29 views

Computational type theorists: how do you compare terms for equality here?

I am attempting to implement Simple Type Theory in the language D. How do you compare subterms to a term $R$ for the sake of computing the covering abstractors of $R$ in $M$? By reference (class ...
1
vote
1answer
24 views

Lambda term satisfying two equations using Bohm Trees

Hi I'm trying to solve this exercise but I can't find any material online, it's not an homework I actually have sort of a solution (it looks incomplete though), but from that I can't really understand ...
0
votes
2answers
100 views

Beta reduction order in Lambda calulus

Will it be wrong to use g for reducing (λx.λy.x) first in step (2) instead of using to reduce λg? Is there a rule against it?
0
votes
1answer
58 views

is reducing to normal form simply applying beta-reduction?

See example below: reduce to normal form: (λ c . (λ a . (λ d . (λ h . (h (d (a (a (λ z y . y))) (d (a (a (λ f x . x))) (a (a (a (λ z x . x)))))) (h (a (a (λ z y . y))) (a (a (a (λ z x . x))))))) (λ ...
4
votes
1answer
75 views

Why are there two not operators in lambda calculus?

From Wikipedia: $\mathrm{true} = \lambda a. \lambda b. a$ $\mathrm{false} = \lambda a. \lambda b. b$ Because true and false choose the first or second parameter they may be combined to ...
5
votes
1answer
48 views

Find a lambda term satisfying two equations

I'm just looking for the general idea on how to approach the following problem: Find a term $\Delta=\lambda x.xUV$ such that: $\Delta\Delta=K$ $\Delta K=S$ (it's a system of 2 equations, I didn't ...
1
vote
1answer
69 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 ...
3
votes
1answer
87 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 ...
1
vote
1answer
42 views

Evaluation of $\beta$-Reduction with Parentheses in $\lambda$-Calculus

I'm studying $\lambda$-calculus, and had a question regarding an exercise I came across. I understand that $\lambda$-calculus uses three main strategies of evaluation, but I'm having trouble applying ...
1
vote
1answer
219 views

Lambda Calculus - Call-by-name AND call-by-value reduction

I have been tasked with reducing the following lambda expression: (λpq.pqp)(λab.a)(λab.b) using call-by-name and call-by-value reduction strategies. Call-by-name strategy: Left-most, outermost ...