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
1
vote
1answer
106 views

Recognizing primitive recursion

I am trying to write a program to recognize if a given lambda calculus expression is primitive recursive. I believe that a general algorithm to do this does not exist, but I am interested in the most ...
1
vote
0answers
502 views

LL(1) grammar for the untyped lambda-calculus

What I want to do I am trying to define a LL(1) grammar of the lambda-calculus. What I did Here is the grammar: $Term \to Abs$ $Term \to App$ $Abs \to \lambda \ id \ . \ Term$ $App \to Var \ ...
1
vote
0answers
22 views

Importance of indexes in Type(i) in calculus of inductive constructions [duplicate]

So I am reading about the calculus of inductive constructions. And I see here and here that there hidden indexes that the user does not know about in the $Type$ sort. It says that they are ...
1
vote
0answers
415 views

How to get from factorial to a y-combinator?

In one of his conference talks Jim Weirich derives the applicative form of the y-combinator by refactoring a partial definition of factorial. The starting point in his talk is different than what ...
1
vote
0answers
59 views

Expressions that cannot be evaluated in normal-order?

It seems to me that when the outermost|toplevel function is itself an expression to be evaluated (i.e.: a higher-order function returning the function to be applied at top-level), then normal-order ...
1
vote
0answers
53 views

How to reduce this with all 4 of normal applicative by-name by-value?

Given mult = \x -> \y -> x*y I am trying to reduce (mult (1+2)) (2+3) with each of the strategies: normal-order ...
1
vote
0answers
698 views

Definition of zero checking expression [closed]

Let $T\equiv\lambda xy.x$ $F\equiv\lambda xy.y$ Numbers are represented as: $0\equiv\lambda sz.z$ $1\equiv\lambda sz.s(z)$ $2\equiv\lambda sz.s(s(z))$ $N\equiv\lambda sz.\underbrace{s(s( ... (s(}_\...
0
votes
3answers
92 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
52 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\...
0
votes
2answers
473 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
2answers
123 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 ...
0
votes
1answer
73 views

Class of languages that are equivalent to the lambda calculus

It is well known that all computable functions can be expressed as terms of the lambda calculus and computed according to its rules. It is also more or less obvious that many classical formal ...
0
votes
1answer
82 views

Language Features Not Translatable into Lambda Calculus

Haskell is said to be a pure language because the language features are directly translatable into lambda calculus. My question is: for languages considered to be non-pure functional languages (e.g. ...
0
votes
1answer
82 views

$\lambda x. \lambda x.x$ vs $\lambda y. \lambda x.x$

Several times, I saw $\lambda$-terms such as $\lambda x. \lambda x.x$, where $x$ is bound by the inner lambda, which I agree. why not just write it as $\lambda y. \lambda x.x$, so it is clear and ...
0
votes
1answer
405 views

Order of argument application in lambda calculus

I encountered the following exercise in a textbook about logic: $\lambda x \lambda Y(Y(x))(j)(M)$ It seems that the expected result from the textbook should be $M(j)$, since there were some type ...
0
votes
1answer
131 views

Is paradox recognition paradoxical or not paradoxical?

Russell's paradox: The set that contains all the sets that do not contain themselves. Does it contain itself? It contains itself if and only if it does not contain itself. Russell's paradox for the ...
0
votes
1answer
39 views

Why does λz.zq reduce to q?

The way I see it, it should not be further reducible. I'm thinking λz.zq is like lambda z: z(q) # Python, not lambda calc ...
0
votes
1answer
99 views

having issue with numbers in Polymorphic Lambda Calculus

It is said that Church Numbers are encoded as following ...
0
votes
1answer
67 views

Given a λ-term, can I decide which machine model I need to express it?

I am having a hard time figuring out the specific relationship, of various things in computability. So we have a hierarchy of machines, with a (real life) upper bound of Turing machines, moving on ...
0
votes
1answer
196 views

Lambda Calculus Reduction

I am a little confused to reduce these lambda calculus expressions. I am instructed to give applicative and normal order reductions for these expressions. $(a):$ $$(\lambda x. (\,(\lambda y.(* 2 y)\...
0
votes
1answer
54 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: ...
0
votes
1answer
53 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
1answer
83 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?
0
votes
1answer
47 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 ...
0
votes
1answer
117 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))))))) (λ ...
0
votes
2answers
184 views

Multiple inputs in lambda calculus (Confusing example)

In a programming class I take, we briefly (very briefly) touched lambda calculus. I think I have a pretty good grasp of the basics now, but one example given I just don't understand. Am I missing ...
0
votes
1answer
39 views

How to find a function in Lambda Calculus?

Yesterday I have been trying to complete this exercise. I have to find: $$ ((map)l)t \simeq \lambda k \lambda x ((k)(t)t_1)....((k)(t)t_n)x $$ where $$l=\lambda k \lambda x ((k)t_1)....((k)t_n)x$$ ...
0
votes
1answer
89 views

Can polymorphism be simulated by lazy type operators?

In the definition of lambda cubes, type polymorphism is distinguished from type operators/constructors. I have the nagging feeling that type polymorphism can be constructed through type operators ...
0
votes
1answer
27 views

Can the lambda functions in Church numbers be swapped?

I've learned that one can represent natural numbers with lambda calculus like this: \begin{align*} c_0 &= \lambda s. \lambda z. z\\ c_1 &= \lambda s. \lambda z. s~z\\ c_2 &= \lambda s. \...
0
votes
1answer
58 views

Verify the type of a lambda expression

I need to verify the type for the lambda expression: $\lambda f.\lambda x.f (f x)$ My method gives me: $(a\rightarrow c)\rightarrow b\rightarrow c$ Im trying to define it in Haskell (on Hugs) like ...
0
votes
1answer
70 views

Which redexes are there in $\lambda s. \lambda z. (\lambda u. z)(\lambda v. v)$? How to substitute arguments?

I'm having difficulties understanding lambda calculus, specially identifying what's a redex. Which redexes are there in $\lambda s. \lambda z. (\lambda u. z)(\lambda v. v)$? The book uses $(\lambda u....
0
votes
1answer
211 views

Free and bound variables in a lambda-calculus term

For this term: $\lambda x.(f (g x))$, what are the free and bound variables? I'm confused as to how to expand this so it will be easier to see. If I expand this will it be $\lambda x. \lambda f....
0
votes
0answers
29 views

How does this dependently-typed boolean elimination function work?

In the companion code to A Tutorial Implementation of a Dependently Typed Lambda Calculus - prelude.lp - there is a rather intimidating definition of a ...
0
votes
0answers
17 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 ...
0
votes
0answers
25 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
43 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, ...
0
votes
0answers
42 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 ...
0
votes
0answers
62 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
1answer
366 views

Handling epsilon productions in recursive descent parsing

I am working on a recursive descent parser for lambda calculus. In my grammar, after removing left-recursion, I am left with the following two productions: ...
0
votes
1answer
123 views

Is this a correct grammar for untyped lambda calculus?

I am trying to write a recursive-descent parser for untyped lambda calculus. While researching the way of formulating the grammar, I managed to put together something like this: ...
0
votes
0answers
61 views

how to build logical representation from dependency tree

I'm trying to build logical representation from dependency tree with python. i created the tree with stanford parser. How can I derive logical presentation from it using Lambda-calculus?
0
votes
1answer
36 views

Is my lambda calculus reduction correct and final form valid in simply typed lambda calc?

I'm looking at some lambda calculus at the moment and came across this question: 0:R 1:R plus: R->R->R (lambda f:T . lambda g:U . (f 0) (g 0)) (plus 1) (plus (plus 1 1)) Is it well typed given ...
0
votes
0answers
32 views

How does it demonstrate that the computational model of rewriting is adequate?

How can I demonstrate that the computational model of rewriting is adequate? For example, with it, it is possible to compute any computable function.
0
votes
0answers
97 views

Reasonable definition of beta-equivalence in big-step semantics

Assume, an extension of the lambda calculus with terms $t$ and values $v$ is defined in big-step operational semantics with evaluation relation $t \Downarrow v$. It is intuitive to assume that $\beta$...
0
votes
0answers
138 views

what is the connection between evaluation context and call by value?

I been reading about $\lambda$-calculus and related stuff, but I got some confusions which i want to clarify. The call by value reduction is expressed with two rules $$ \frac{e_1 \rightarrow e_1'}{...
0
votes
0answers
230 views

Constructing a Turing Machine with Lambda Calculus

I'm interested in the implementation of a Turing Machine (deterministic) in Lambda Calculus. How should I proceed to do this? I am not sure on how to start since I must represent the state and ...
0
votes
1answer
125 views

What is a preterm parser?

I am working with HOL-Light parser and keeping seeing references to preterm parser. What is a preterm parser? The most informative statement I find is from the HOL-Light reference for the ...
-1
votes
1answer
25 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
votes
1answer
412 views

Encoding of integer arithmetic counting using Lambda calculus [duplicate]

Does anyone know a way of showing an encoding of integer arithmetic counting using Lambda Calculus? Any references related to this would be much appreciated.
-2
votes
1answer
30 views

Lambda calculus simplification excercise

Below is the lambda expression which I am finding difficult to reduce i.e. I am not able to understand how to go about this problem. (λx.λy.yx)z (λw.w) I am lost with this. if anyone could lead me in ...

1
6 7 8
9
10