Stack Exchange Network

Stack Exchange network consists of 175 Q&A communities including Stack Overflow, the largest, most trusted online community for developers to learn, share their knowledge, and build their careers.

Visit Stack Exchange

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.

12
votes
0answers
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 ...
10
votes
0answers
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 ...
7
votes
0answers
133 views

Equivalence of categories of directed complete posets

In the book ``Domains and Lambda-Calculi'' by Amadio and Curien, there is the following exercise: Define an equivalence between the category of partial morphisms generated by $(\mathcal{M}_S, \textbf{...
5
votes
0answers
160 views

Injections between distinct models of the simply typed lambda calculus

Let a model of the simply typed lambda calculus be a Cartesian-closed functor from $C_T$ to Set, where $C_T$ is a free CCC (as in e.g. this reference, p. 83.) The simple case of one or two primitive ...
5
votes
0answers
112 views

Is there any elegant formalization of fractional numbers?

The question is just what is on the title, but I'll describe the context for completion: Natural numbers can be encoded quite elegantly on the Lambda Calculus as church numbers, that is, a function ...
4
votes
0answers
236 views

Relation between Cartesian Closed Category and Terminating Programs

Relation between Cartesian Closed Category and Terminating Programs. Simply Typed Lambda Calculus (STLC) is a Cartesian Closed Category (CCC), it has all products, objects that represent arrows and a ...
4
votes
0answers
668 views

Differential in lambda calculus

Introduction and Notation I'm experimenting with $\lambda$-calculus and I'm wondering about the exact semantics of common operators in calculus, specifically the differential operator. Suppose we ...
4
votes
0answers
226 views

Can all computable numeric functions on church numerals in ski-combinator calculus be expressed using only completely evaluated terms?

Let a term in ski-combinator calculus be called "complete" if every primitive is partially applied (so all S's are applied to at most two arguments, all K's to at most 1, and all I's are not applied). ...
4
votes
0answers
39 views

Extensionality of a hierarchy of functionals over $\mathbb{N}$

Let $H$ be the complete hierarchy of functionals over $\mathbb{N}$. To be precise: let the set $T$ of 'simple types' be the smallest set such that '0' $\in T$ and $(α→β) \in T$ whenever $α, β \in T$. ...
4
votes
0answers
92 views

What strongly normalizing lambda calculi exist that can be integrated with/as logic?

If I'm trying to implement a logical system for deduction based on propositional reasoning, I can start with predicates and quantifiers and functions to obtain first order logic. I can further extend ...
3
votes
0answers
38 views

Type equivalence in $\lambda\underline\omega$ under lambda abstraction

I'm going through "Type Theory and Formal Proof" by Nederpelt and Geuvers and just trying to play around with $\lambda\underline\omega$ after reading the chapter on it to better grasp the material. ...
3
votes
0answers
66 views

Head position in lambda calculus

I'm confused about what actually constitutes the head position in a lambda term. Wikipedia defines it as the $(\lambda x. A) M_1$ in: $\lambda x_1 . \ldots \lambda x_n . (\lambda x . A) M_1 M_2 \...
3
votes
0answers
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, ...
3
votes
0answers
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 ...
3
votes
0answers
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 ...
3
votes
0answers
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 ...
3
votes
0answers
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-...
3
votes
0answers
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 ...
3
votes
0answers
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 ...
3
votes
0answers
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 ...
2
votes
0answers
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. ...
2
votes
0answers
80 views

Lambda Calculus - Exercise with fixed point combinator

This is exercise 2.10(iii) from "Introduction to Lambda Calculus". We need to find an $F$ such that $F \mathbf{I} \mathbf{K} \mathbf{K} = F \mathbf{K}$ Here there is my solution: Let $\mathbf{K}_3 ...
2
votes
0answers
72 views

Lambda Calculus and naming

I see that $\lambda$-calculus let's you work with anonymous functions and names are purely local. As an example $$\lambda x.x$$ contains $x$ only as a local name. This will be replaced during ...
2
votes
0answers
147 views

Relation between Lambda calculus and SKI combinator calculus

I have played around with evaluation of Lambda terms in Lambda calculus and their counterparts using SKI combinators. While the results are extensionally equal (as they should be), there are striking ...
2
votes
0answers
55 views

Denotation in Lambda Calculus

I have the following sentence: "John offends nobody." I need to do three things. First, figure out what semantic types each node of a syntax tree refers to. Second, determine what each node in the ...
2
votes
0answers
77 views

Lambda Calculus: terms without β-normal form, but have a β-normal form when combined?

I need to find two λ-terms $A$ and $B$ where neither $A$ nor $B$ have a β-normal form, but $(A\ B)$ has a β-normal form. How would I go about doing this?
2
votes
0answers
67 views

Lambda Calculus - reduction with a shorthand term

I'm new to lambda calculus and am having trouble understand how a shorthand acts when reducing. Given: $((\lambda xy.x)(\lambda y.y))y$ What I have: since $\lambda xy.x = \lambda x.\lambda y.x$ $((...
2
votes
0answers
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 ...
2
votes
0answers
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 ...
2
votes
0answers
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 ...
2
votes
0answers
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 ...
2
votes
0answers
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 ...
2
votes
0answers
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 ...
2
votes
0answers
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 ...
2
votes
0answers
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 ...
1
vote
0answers
24 views

Can induction be proven in $\lambda C$?

Is it possible to prove induction in $\lambda C$? In other words, is the following type inhabited? $$\Pi P:\mathbf{nat} \to \ast. (P0 \land \Pi n : \mathbf{nat}. Pn \to P(\mathbf{succ}\ n)) \to \Pi n ...
1
vote
0answers
25 views

exhibiting a turing machine and a λ-term of a boolean function

I have a funtion f: BOOL ⇒ Bool, sich that f(x,y) is true when x=y and false otherwise. Im trying to exhibit a touring machine and a lambda term. for the second part I know that in boolean logic, x ⇒ ...
1
vote
0answers
36 views

beta reduction: order of substitution

Do we always apply our input to the left most term in a lamda expression? For instance, take the expressions: $λP λQ. ∀x P(x)→Q(x)$ which we can rewrite as $[λP λQ[ ∀x P(x)→Q(x)]]$ $λP. λQ. ∀x P(x)→...
1
vote
0answers
72 views

The continuation passing style transformation in the lambda calculus

I have an issue understanding the following definition (from https://tel.archives-ouvertes.fr/tel-00783245/document , p.82) of the continuation-passing style (CPS) transformation in the lambda ...
1
vote
0answers
36 views

Help express this λ-calculus function in a non-recursive form?

The function is fib = λn(IF (n<2) 1 (fib(n-1)+fib(n-2)) (if n<2 then 1, else the sum of the previous two). How do I make it non-recursive? I know it's about ...
1
vote
0answers
60 views

Confused about applicative order

Applicative order is said to be leftmost, innermost. But I often here, it means "first evaluate the arguments". Sometimes I'm confused to what actually applies in what case. Here's an example: $$(...
1
vote
0answers
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 ...
1
vote
0answers
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 ...
1
vote
0answers
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, ...
1
vote
0answers
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 ...
1
vote
0answers
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, ...
1
vote
0answers
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 ...
1
vote
0answers
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 ?
1
vote
0answers
211 views

Function notation for specifying (co)domain and mapping at once

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$$ ...
1
vote
0answers
29 views

Proving the Existence of the “Bureaucrat Term” in the Lambda Calculus

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 ...