Stack Exchange Network

Stack Exchange network consists of 174 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

λ-calculus is a formal system for function definition, function application and recursion which forms the mathematical basis of functional programming.

2
votes
0answers
23 views

Are there any interesting terms in pure LF or $\lambda\Pi$?

In my searching, I've seen that if Church numerals are encoded in a dependently typed Lambda calculus, that we can't derive induction or that $0 \neq 1$. I know that LF and the dependently typed ...
2
votes
3answers
41 views

How does one formally show that two lambda functions are $\alpha$ equivalent?

I was going through the following slides and I wanted to show the following: $$ \lambda x. x \equiv_{\alpha} \lambda y . y$$ formally. They define a an $\alpha$-conversion on page 15 as follows: $$ ...
2
votes
2answers
57 views

Why is it that a lambda function requiring multiple input also requires multiple functions?

So I recently discovered lambda calculus and for the most part I understand it. However, one specific part of it that I cannot understand is this: Let's say we define a very simple function $$ I := \...
9
votes
5answers
2k views

Lambda Calculus Generator

I don't know where else to ask this question, I hope this is a good place. I'm just curious to know if its possible to make a lambda calculus generator; essentially, a loop that will, given infinite ...
0
votes
1answer
29 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$$ ...
3
votes
1answer
37 views

Why does existence of predecessor imply adequacy of a numeral system?

I encountered this result when working with $\lambda$-calculus (so every element I mention here was a $\lambda$-expression there [1]), but I will express everything with, more understandable to ...
2
votes
1answer
64 views

Differences between Church and Scott encoding

I'm kind of new to lambda calculus and I found this Wikipedia article https://en.wikipedia.org/wiki/Mogensen%E2%80%93Scott_encoding The section Comparison to the Church encoding presents a short ...
1
vote
1answer
62 views

Reducing lambda expression to normal form

Can someone explain the steps to reduce $$ (\lambda n. \lambda m. \lambda f. \lambda x.\ n\ (m\ f)\ x)\ (\lambda f. \lambda x.\ f\ (f\ x))\ (\lambda f. \lambda x.\ f\ x) $$ to $\lambda y. \lambda z.\...
2
votes
2answers
281 views

Encoding (binary) trees using lambda calculus

I'm new to lambda calculus, and I read all kinds of interesting stuff about encoding data types as functions. Church booleans, numbers and lists. https://en.wikipedia.org/wiki/Church_encoding Is ...
17
votes
0answers
182 views

Can a calculus have incremental copying and closed scopes?

A few days ago, I proposed the Abstract Calculus, a minimal untyped language that is very similar to the Lambda Calculus, except for the main difference that substitutions are ...
1
vote
1answer
78 views

How to transform lambda function to multi-argument lambda function and how to rewrite or approximate terms?

I am trying to do the formal semantics (Montague grammar, abstract categorial grammar) of natural language and encode the sentence John is boss. The type system has ...
1
vote
0answers
26 views

Call-by-push-value vs Fine-grain Call-by-value

It seems to me that Fine-grain call-by-value already subsumes CBV and CBN, using lambdas as thunks. What does CBPV improve upon FG-CBV or in what way is it "better"?
2
votes
1answer
73 views

Proving Progress for STLC with Linear and Unrestricted Types

In this paper Walker presents an extension of STLC with linear and unrestricted types. The proof of type soundness is left as an exercise to the reader. I encountered difficulty when attempting to ...
3
votes
0answers
57 views

CFG for $\lambda$-calculus with minimal parentheses

The typical presentation of the syntax of the $\lambda$-calculus is as an ambiguous CFG (or BNF) like the following: $$T \rightarrow \lambda X . T \mid T ~ T \mid X \mid (T)$$ Where we permit $X$ to ...
4
votes
1answer
67 views

if an argument of a lambda only passes itself if it is further evaluated, is runtime always finite?

In order for a lambda expression to run forever, there must be at least one lambda in the expression in which an argument is passed to itself. For example the following runs forever. $$ (\lambda x.xx)...
2
votes
2answers
169 views

Confusion about the definition of de Bruijn terms in the TAPL book

I'm working through Types and Programming Languages right now, and I'm a little confused about the recursive definition given for nameless/de Bruijn terms (chapter 6, definition 6.1.2). Below is the ...
2
votes
1answer
50 views

Why is abstraction in lambda calculus called abstraction?

The term abstraction as I understand it, is used in many different contexts, but has one essential meaning, namely that it refers to the “general properties of some class of objects that doesn’t rely ...
3
votes
2answers
85 views

In Hindley-Milner system, how can I prove that let id=\x.x in id id is well-typed?

I am trying to infer the type and prove that this is well-typed: let $f =\lambda x.x$ in $f f$ Obviously the $f$ is the identity function, so it's the same as let $id =\lambda x.x$ in $id$ $id$ I ...
2
votes
0answers
20 views

Understanding First conversion rules from church's lambda bible

While going through Church's text on Lambda calculus , I cam across the first set of conversion rules . Before writing out my query I would like to put the notation that church has used for ...
0
votes
0answers
31 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?
2
votes
0answers
49 views

Term for weak head normal forms that cannot be reduced in any environment

In my understanding, a lambda expression is a normal form (NF) when it has no redexes. For instance, $\lambda x.x$ is a NF, but $(\lambda x.x)y$ is not. A lambda expression is a weak head normal form (...
1
vote
2answers
202 views

Application of lambda function in Simply Typed Lambda Calculus

I'm just getting started with STLC (Simply Typed Lambda Calculus) and I'm trying to understand an evaluation rule I've been given in some lecture notes by my professor. What it says is the following: ...
6
votes
1answer
115 views

How to model conditionals with first-class functions?

Since languages with recursible first-class functions are Turing-complete, they should be able to express anything expressible in any other programming language. Therefore, it should be possible to ...
1
vote
2answers
66 views

Term rewrite system for terms of lambda calculus?

Are there term rewrite systems, that can rewrite complex lambda term (with nested function application) into some other lambda terms, I.e. reorde function application and, possibly, introduce new ...
3
votes
0answers
31 views

Expressing definite clauses (Horn rules, logic programming) in lambda terms?

There is paper which expresses lambda terms in the terms of logic programming http://www.cse.unt.edu/~tarau/teaching/PL/docs/dbx.pdf Is there conversion in the other direction - expressing definite ...
6
votes
0answers
86 views

Advantages of algorithm W over algorithm J for type inference in Hindley-Milner type system

According to A modern eye on ML type inference Furthermore, for some unknown reason, W appears to have become more popular than J, even though the latter is viewed—with reason!—by Milner as ...
2
votes
1answer
50 views

Trying to verify the solution to a lambda calculus equation

I am going through the following introduction to lambda calculus : http://www.cse.chalmers.se/research/group/logic/TypesSS05/Extra/geuvers.pdf At page 12 , the following has been asked to prove $ \...
2
votes
1answer
77 views

Reduction of the Y combinator

The Y combinator expression is as follows: $$ Y \equiv \lambda f .(\lambda x .f(xx) )) .(\lambda x .f(xx) ) $$ Now , if I am not wrong , then this expression can be reduced by seeing this as the ...
1
vote
0answers
23 views

confusion due to the apparent difference in semantics of two beta reductions

Let us consider the following lambda expression : $ (\lambda func.\lambda arg$ $( func$ $ arg)$ $\lambda x.x)$ so $ (\lambda func.\lambda arg$ $( func$ $ arg)$ $\lambda x.x)$ can be seen as $ (\...
2
votes
1answer
53 views

Rigorous reason against the seemingly wrong way of substitution

Let us consider the lambda calculus expression . $ (\lambda func.\lambda arg$ $( func$ $ arg)$ $\lambda x.x)$ Now $\lambda x.x$ is seen as an argument . How to decide which bound variable should the ...
3
votes
1answer
78 views

Understanding Applicative Evaluation Order with the Z-Combinator

I am trying to understand how the Z-combinator (Y-combinator for applicative order languages) definition came about. As Python is applicative I am using Python for this. So I know Python's evaluation ...
2
votes
1answer
34 views

An explanation for Barendregt use of Y combinator in an equation

I am going through the following lecture notes on lambda calculus by Barendregt and Barendsen : http://www.cse.chalmers.se/research/group/logic/TypesSS05/Extra/geuvers.pdf Here at page 12 , after ...
2
votes
1answer
50 views

Doing beta reduction while constructing the boolean expression in lambda calculus

I am going through beta reduction in lambda calculus . And beta reduction to my understanding is an act of substitution like in the following : $ (\lambda x.P) M $ is said to be beta reduced to : $...
5
votes
2answers
254 views

$\lambda$-calculus, is there encoding of for or while?

In $\lambda$-calculus, we can encode arithmetic, numbers, booleans, and even compute factorials of numbers, as shown here. Is there encoding of "for" or "while"?
2
votes
1answer
54 views

How is this lamda function beeing executed in an example for the Y combinator

I have spent a few hours now trying to understand how the Y Combinator is working and how it allows us to construct recursive functions with higher order functions. I have been going through this ...
4
votes
1answer
129 views

Some points about type checking of simply typed $\lambda$-calculus?

type checking I was preparing examples of type checking in simply typed $\lambda$-calculus. I wanted to explain it to my audience in the way of implementation. And I found a bit tricky point in the ...
3
votes
1answer
81 views

Abstractions in call-by-push-value

In "Call-by-push-value: A subsuming paradigm." (Levy, Paul Blain. Springer, Dordrecht, 2003. 27-47) terms of the lambda calculus get split in to values and computations, with the slogan "A value is, a ...
4
votes
2answers
64 views

Composition of handler types in algebraic effects and handlers

In the paper "An introduction to algebraic effects and handlers" (Pretnar, Matija. Electronic Notes in Theoretical Computer Science 319 (2015): 19-35), handlers get a handler type that looks like a ...
1
vote
1answer
62 views

It is possible to write any program (i.e. Turing complete) with just one single expression?

So I'm currently taking discrete math II at my university and I came across a somewhat philosophical question (so I apologize if this is question is hard to answer precisely) of whether mathematicians ...
4
votes
1answer
322 views

How do I arrive at the multiplication function in lambda calculus?

I'm familiar with how Church numerals are defined in the lambda calculus, i.e. as functions that take two arguments and apply the first argument $n$ times to the second. Then I have the successor and ...
2
votes
1answer
109 views

explaining $\lambda$-calculus/functional programming to someone used to Turing machines/procedural programming?

I have the following background: I have experience with object-oriented programming languages I find Turing machines and the concept of a "procedure" very intuitive. Yet I'm interested to ...
7
votes
2answers
91 views

Ackerman hierarchy for higher order primitive recursion in System T

Gödel defines in his System T primitive recursion over higher types. I found notes from Girard where he explains the implementation of System T on top of simply typed lambda calculus. On page 50 he ...
5
votes
1answer
131 views

Lambda calculus as the language of universal logic - connectives vs functions in lambda calculus?

I am reading http://okmij.org/ftp/gengo/applicative-symantics/AACG1.pdf and there is defined language TL (see last row in the table on page 4). It seems to me from this definition of TL, that lambda ...
3
votes
2answers
120 views

How to reduce Untyped λ-Calculus to Normal Form?

I have an assignment to do which involves reducing an Untyped λ-Calculus expression to Normal Form. I am struggling to come to terms with Lambda Calculus though. For example, one small part of the ...
0
votes
1answer
26 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 ...
2
votes
1answer
64 views

Why models of computation are primarily focused on machines?

It seems a lot of courses (like this and this) on theory/models of computation (and even formal languages) cover DFA, NDFA, PDA, and TM in the order of increasing computational power. This of course ...
2
votes
0answers
46 views

Automatic learning/discovery of logics

Are there efforts to automatically discover new logics? Logics are simple structures - they have formal language, deduction rules, semantics and certain properties that are proved or discarded for ...
3
votes
0answers
63 views

Semantic parsing with Grammatical Framework - is this possible?

So far I have learned about categorial grammars, type logical grammars and formal semantics of natural language, the relevant tools are Cornell Semantic Parsing Framework https://github.com/clic-lab/...
4
votes
1answer
152 views

Mathematical proofs implemented purely by Lambda Calculus

I've seen often stated that Lambda Calculus can be used for mathematical proofing but I haven't yet seen any example how it is actually used for the task. Is there a simple example, lambda ...
2
votes
0answers
44 views

Lambda calculus closure expansion

The set of lambda calculus expressions $Expr$ is generated by the grammar $$ Expr \ni e ::= x \mid \lambda x\ldotp e \mid e_1 e_2 $$ We can define an interpreter without explicit substitution by ...