Questions tagged [lambda-calculus]
λ-calculus is a formal system for function definition, function application and recursion which forms the mathematical basis of functional programming.
408
questions
5
votes
0answers
39 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
57 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
36 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
17 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
49 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
110 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
43 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
29 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
35 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 ...
1
vote
0answers
30 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
42 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
47 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
47 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
22 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
55 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
50 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
55 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
54 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
35 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
85 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
88 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
39 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
51 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
77 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
42 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
51 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
51 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
83 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
37 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
137 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
92 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
37 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
61 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
103 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
247 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
38 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
63 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
112 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
45 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
90 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
136 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
57 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
106 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
41 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
32 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
33 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 ...
asked Feb 23 at 12:49
Gilles 'SO- stop being evil'
37.4k7 gold badges100 silver badges166 bronze badges
