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
0
votes
0answers
14 views

Does there exist a way, within Lambda Calculus, to discover if two free variables are the same?

Using Church's $\lambda x.(\lambda y.y))$ as false and $\lambda x.(\lambda y.x))$ as true, and given two free variables $g$ and $h$: Could there exist a function $eq?$ such that $(eq?\ g\ h)$ is ...
-1
votes
0answers
10 views

Lambda Calculus - Number of reducible expressions

Working through some Lambda Calc questions but I am having trouble with ones that use multiple sets of parenthesis. Questions like the one below where there are multiple sets divided by variable terms ...
0
votes
1answer
32 views

lambda calculus beta reductions: ((((lambda f (lambda x ((f x) f))) (lambda y (lambda g (g (* y y))))) 2) (lambda a a))

My question is in continuation to lambda calculus reduction: (((lambda f (lambda x (f x))) (lambda y (* y y))) 12) given the input: ...
1
vote
1answer
51 views

lambda calculus reduction: (((lambda f (lambda x (f x))) (lambda y (* y y))) 12)

given the input (((lambda f (lambda x (f x))) (lambda y (* y y))) 12) what does this step evaluate to: lambda x (f x) I am ...
4
votes
1answer
415 views

Does the underlying computational calculus in type theories affect decidability?

I'm looking for a high-level explanation although if that isn't possible or difficult, I'd prefer references to books/papers. I understand that modern type theory is inspired by Curry-Howard ...
2
votes
0answers
30 views

Is there an abstract architecture equivalent to Von Neumann's for Lambda expressions?

In other words, was a physical implementation modelling lambda calculus (so not built on top of a Von Neumann machine) ever devised? Even if just on paper? If there was, what was it? Did we make use ...
-2
votes
0answers
35 views

Proof of lambda reductions

I am not sure how to approach this question or what exactly it is asking. Need to prove the following reductions: Need to prove those knowing that: N = λf.λc.(f (f . . .(f c)). . .) and that: ...
-2
votes
1answer
60 views

Lambda Expression Reduction

I am unable to solve the following lambda expression using both normal order (Call-by-name) and applicative order (Call-by-value) reduction. I keep getting different answers for both. This is the ...
0
votes
0answers
21 views

Lambda calculus self reducer with explicit redex selection

In "Efficient Self-Interpretation in Lambda Calculus", Mogensen presents a self-reducer in lambda calculus which leaves redex selection to the underlying reduction. Is there some example of a self-...
0
votes
1answer
35 views

Termination of Z combinator with call-by-value

I am trying to build my own λ-calculus interpreter. So far it supports both call-by-value and normal order. I now want to try recursion via fixed points. The $Y$ combinator works with normal order, ...
2
votes
0answers
18 views

Standardisation Theorem versus Leftmost reduction Theorem

According to Chris Hankin in his book (Lambda Calculus a Guide for Computer Scientists). A reduction sequence $\sigma: M_0 \to^{\Delta_0} M_1 \to^{\Delta_1}M_2 \to^{\Delta_2}\ldots $ is a standard ...
1
vote
0answers
15 views

Self reduction for fully introspective lambda calculus representations

For some representation scheme $\ulcorner \cdot \urcorner$, a self interpreter $R$ is a lambda expression where $R \ulcorner A \urcorner \underset{\beta}{=} A$, while a self reducer $E$ is a lambda ...
3
votes
0answers
64 views

Is it true that if $M : \forall \alpha . \left( \alpha \rightarrow \alpha \right)$ is a closed term then $M = \Lambda \alpha. \lambda x^{\alpha} . x$?

In system F, is every closed term $M$, which is of $\forall \alpha . \left( \alpha \rightarrow \alpha \right)$, $\alpha \beta \eta$-equivalent to $\Lambda \alpha. \lambda x^{\alpha} . x$? I have ...
2
votes
0answers
38 views

Normal Order Reduction - is Leftmost Outermost order simply Leftmost?

This is a quick question. I've been reading up on Lambda Calculus, and I see Normal Order as "outermost leftmost first", and Applicative Order described as as "innermost leftmost first". I think ...
0
votes
1answer
52 views

How to find a lambda term to complete a function?

I tried to complete this exercise but i stopped... Defining a $ \lambda $-term M such that: $$(<M,u>)<M,v> \: \simeq_{\beta} \: <M,u>$$ I chose $M=\lambda m \lambda a \lambda b \...
0
votes
0answers
41 views

in the lambda calculus with products and sums is $f : [n] \to [n]$ $\beta\eta$ equivalent to $f^{n!}$?

$\eta$-reduction is often described as arising from the desire for functions which are point-wise equal to be syntactically equal. In a simply typed calculus with products it is sufficient, but when ...
2
votes
1answer
43 views

Hindley-Milner system with let expansion

I'm reading these slides that present Hindley-Milner type inference. In the system HM, we have the following let rule: $\dfrac{\Gamma \vdash t:S \;\; \Gamma,x:S \vdash t':T }{\Gamma \vdash \text{let} ...
2
votes
0answers
22 views

Blum complexity measure for lambda calculus

Is there a formal complexity measure for lambda expressions which satisfies the Blum axioms and measures the complexity of reducing the expression to its normal form? I assume that the complexity ...
4
votes
1answer
38 views

Zero-knowledge proof of $\beta\eta$ equality

Is there some way to give a zero-knowledge proof that two $\lambda$-terms are convertible, i.e. equal modulo $\beta\eta$? A usual (and not zero-knowledge) proof that two terms are convertible is a ...
5
votes
0answers
41 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: ...
2
votes
0answers
61 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? ...
1
vote
0answers
42 views

Equivalent terms in call-by-name but not in call-by-value

Working in the untyped lambda-calculus, I'm asked to give two terms that are equivalent in call-by-name semantics but not in call-by-value. Call $\text{fls} = \lambda x. \lambda y. y$ and $\Omega = (\...
2
votes
1answer
19 views

Finding two store typings that make the same store valid (lambda-calculus with references)

Problem 13.5.2 of Pierce's TAPL's book (page 167) asks: Can you find a context $\Gamma$, a store $\mu$ and two different store typings $\Sigma_1,\Sigma_2$ such that both $\Gamma | \Sigma_1 \vdash \...
5
votes
1answer
65 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 ...
4
votes
2answers
122 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 ...
2
votes
2answers
46 views

What is the adjunct of the evaluation morphism in a closed monodical category?

According to the nlab article about evaluation map if $X, Y \in C$, a closed monodical category then the adjunct to evaluation morphism $[X, Y]\otimes X \rightarrow Y$ is the identity morphism $[X, Y] ...
2
votes
1answer
35 views

How does the function to curry and uncurrying another function work?

The following is the code to curry or uncurry a function in Haskell: ...
1
vote
1answer
46 views

An operational semantics for lambda-calculus normal order evaluation strategy

TAPL book, page 56 reads: Under the normal order strategy, the leftmost, outermost redex is always reduced first. I understand this as a restriction of the full beta-reduction evaluation ...
2
votes
1answer
46 views

Mapping a free variable of type A to a cartesian closed category

In From Lambda Calculus to Cartesian Closed Categories, the author explains the interpretation of lambda calculus in cartesian closed category and at one point he explains how a term representing a ...
1
vote
1answer
58 views

Is monoid the category for untyped lambda calculus?

If cartesian closed categories are the model for simply typed lambda calculus, then can it be said that a monoid is a categorical model for untyped lambda calculus?
2
votes
1answer
26 views

lambda-calc program which halts on only one input

Does there exist a normal-form lambda calculus program $f$ such that $f (\lambda x . x)$ normalizes For all normal form $e \ne \lambda x . x$, $f e$ does not normalize
2
votes
1answer
61 views

How is β-reduction a 2-morphism in Category theory?

According to Categorifying CCCs: Computation as a Process, computation or β-reduction process in untyped-lambda calculus is in fact a 2-morphism in category theory. Can someone please describe me ...
2
votes
1answer
54 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 ...
0
votes
0answers
24 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. ...
4
votes
0answers
62 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 ...
3
votes
1answer
52 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 ...
4
votes
0answers
134 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 ...
3
votes
0answers
58 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.
0
votes
1answer
42 views

Could following be a counter example to Church-Rosser (Confluence) theorem?

According to the "Type Theory and Formal Proof" book, Church-Rosser theorem (confluence) is as follow: Suppose that for a given term $M$, we have $M \twoheadrightarrow_\beta N_1$ and $M\...
2
votes
1answer
61 views

Are the definitions of constructs in terms of lambda terms issues in implementation/design or uses of functional languages?

In Lambda Calculus, natural numbers, boolean values, list processing functions, recursion, if function are defined in terms of lambda terms. For example, natural numbers are defined as Church numerals,...
3
votes
2answers
89 views

What is the name of the operator that translates from $X\rightarrow(Y\rightarrow Z)$ to $Y\rightarrow(X\rightarrow Z)$?

Is there a standard name for the operator that takes a function $f:X\rightarrow(Y\rightarrow Z)$ and returns the function $f':Y\rightarrow(X\rightarrow Z)$ that satisfies, for every $y \in Y$ and $x \...
5
votes
1answer
41 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 \...
3
votes
0answers
122 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
40 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?
5
votes
1answer
67 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 ...
3
votes
1answer
80 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
44 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
52 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?
29
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
59 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 ...

1
2 3 4 5
9