Questions tagged [lambda-calculus]

For questions on the formal system in mathematical logic for expressing computation using abstract notions of functions and combining them through binding and substitution.

103 questions
634 views

Why can't we formalize the lambda calculus in first order logic?

I'm reading through Hindley and Seldin's book about the lambda calculus and combinatory logic. In the book, the authors express that, though combinatory logic can be expressed as an equational theory ...
418 views

Fixed points in computability and logic

I asked this question on CS.SE, too: https://cstheory.stackexchange.com/questions/27322/fixed-points-in-computability-and-logic I would like to understand better the relation between fixed point ...
133 views

54 views

Lambda Calculus: Evaluating Functions

I have to evaluate two lambda functions. I have done so and will explain how I did. I'm wondering that if it is noticed that I made a mistake someone might say so. I do not want answers; but hints, ...
58 views

Can we rule out candidate single-axiom bases for HI via Curry-Howard?

The motivation for this question begins with an answer elsewhere which references Dolph Ulrich's list of single-axiom bases and unresolved candidate single-axiom bases for implicational intuitionistic ...
123 views

Some modal principles (related to monads) and the deduction theorem (in Propositional Lax Logic)

I have two questions. Suppose we have a Hilbert style axiomatic intuitionistic propositional calculus which we supplement with a modal operator $\bigcirc$ (see the bottom of the question for the ...
122 views

Construct successor function with combinators with only 2 variables

For a Uni project I try to build complex lambda expressions with combinators that use only two (bound) variables. For example I managed to create IF-THEN-ELSE $(λp.λa.λb.p a b)$ by using three ...
112 views

What is the root of first class object in programming languages?

What is the root of "first class object" of programming languages? (Also see https://en.wikipedia.org/wiki/First-class_function, and https://stackoverflow.com/questions/245192/what-are-first-class-...
53 views

Find recursively enumerable theory $\mathcal{T}_3$ such that $\mathcal{T}_1 \subsetneq \mathcal{T}_3\subsetneq \mathcal{T}_2$.

I am trying to solve the following problem: Let $\mathcal{T}_1, \mathcal{T}_2$ be recursively enumerable $\lambda$-theories such that $\mathcal{T}_1 \subsetneq \mathcal{T}_2$. Show that there ...
149 views

What is the desirable function identification when setting up arrows in the category of types?

My question is which functions can not be allowed in a statically typed programming language, so that the "canonical" category is less coarse than what you get if you define it's arrows to be ...
226 views

Is there an algorithm to separate lambda calculus terms using Böhm's theorem?

Böhm's theorem says that given lambda terms $r$ and $s$ with non-equivalent normal forms, there exists $\vec{a}$ terms such that $r\vec{a}=t$ and $s\vec{a}=f$. I'm finding it hard to determine what ...
46 views

Transformations similar to Curry/Uncurry

The currying operator transforms a function of the form $(A\times B)\rightarrow C$ into an equivalent one of the form $A\rightarrow(B\rightarrow C)$. The uncurrying operator goes the other way round. ...
80 views

534 views

Concurrent Neural Network - Enabling Currying

Currently, neural networks can be trained in a parallel fashion and I read a couple of very good research papers on it. I am trying to implement neural networks that can take concurrent input and ...
115 views

lambda calculus nesting order

I don't understand if there is a proper ordering to nested functions in lambda calculus and, if so, what that is. Regardless of the order in which they are nested, if the same reduction strategy is ...
309 views

Equivalence of Turing Machines and Lambda Calculus

Based on the Church Turing Thesis, we conjecture that Turing Machines are the "correct," model of computation. It is well known that they are equivalent to the Lambda Calculus, another model of ...
241 views

A kind of reverse Church-Rosser

In the $\lambda$-calculus. Proposition: For any terms $M$,$N$ such that $M =_\beta N$, there is a term $L$ such that $L \twoheadrightarrow_\beta M$ and $L \twoheadrightarrow_\beta N$. Is this true ...
491 views

When does renaming bound variables require a fresh variable?

Suppose that $E_1$ and $E_2$ are two $\alpha$-equivalent first-order logic formulas (or $\lambda$-terms), and let $V$ be the set of all variables (free and bound) used in $E_1$ or $E_2$. Is it ...
78 views

Deriving the fixed point for $\omega$ (i.e. $\lambda x.xx$) and proving it to be so

I am studying the simply typed $\lambda$-calculus, and I am struggling a bit with really understanding fixed-points and the $\mathbf Y$ combinator. I have read or skimmed all the questions on here ...
236 views

How far can-I rewrite in lambda functions?

I am quite new with the lambda calculus. I am experimenting lambda-calculus proofs through the coq proof assistant, but the question I have is not related to coq (I guess). However, I'm going to use ...
1k views

Associative, commutative properties and identity elements of non-binary functions

I'm making a compiler (for a new language) wich supports AC unification via pattern matching. The matching algorithms already works but i'm having trouble with the logical and mathematical aspects of ...
24 views

41 views

Lambda Calculus: Types, Denotations & Evaluations

I have a sentence: "Ann introduces Marie to Jacob.' (I don't know how to do the syntax tree in Latex, I apologize if it looks awful). I need to do three things. First, determine the types associated ...
187 views

Lambda Calculus substitution

I am trying to wrap my head around substitution in lambda calculus and not sure if I am heading in the right direction. For example, $[(\lambda y.xy)/x](x(\lambda x.yx))$ Here, we must substitute ...
101 views

lambda-calculus proof of the identity substitution

given a $\lambda \text{-}$term $M$, how does one prove that the identity substitution on $M$ results in $M$ ? That is:$$[x/x] M \equiv M$$ Should I go for the cases, trying to prove for $M$ atomic, ...
168 views

how to represent free variables within lambda-calculus expression

Given I have the expression $\lambda x (y(\lambda y(xy)))$, I know that $x$ is a bound variable because of the initial $\lambda x$, but I'm not sure how I could express the $y$ since it is free before ...
65 views

Reading Simply Typed lambda-calculus's PAT-Interpretation of 'sends proof to proof'

I have seen this figure of speech in multiple places. But to be specific, in the book 'Type Theory and Formal Proof: An Introduction' we have the following example which derives a type judgement, ...
92 views

completeness and soundness in $\lambda$-caclulus

I many times encountered the concept of soundness and completeness in proof related articles, such as type system, logic. description of these two concepts in logic I had a discussion recently and ...
93 views

Is lambda-calculus built over ZFC theory?

I would like to know if lambda-calculus have been built using ZFC theory ? Or if it is not, on what kind of theory lambda-calculus is based on ?
I am looking for conventions of spelling out a function type together with a mapping. I have found some possibilities: using intermediate words: $$f \colon R \to R\ \text{where}\ x \mapsto x^2$$ ...
From pg. 35 of Lambda Calculus and Combinators An Introduction: Corollary 3.3.1 in $\lambda$ and $CL$: for every $Z$ and $n \ge 0$, the equation $$xy_1 \ldots y_n = Z$$ can be solved ...