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
111 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
1k 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 ...
3
votes
1answer
180 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 ...
8
votes
2answers
182 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
198 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
209 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
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 ...
2
votes
1answer
75 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
54 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
139 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/...
5
votes
1answer
427 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
74 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 ...
4
votes
1answer
78 views

Why does substitution terminate?

I'm formalizing some properties of lambda calculus in Coq and I have some problems proving termination of substitution. My terms are defined as: ...
3
votes
0answers
58 views

Is the number of tests needed to know if a program computes the identity computable?

Given a $\lambda$-term $t\in \Lambda$ and an integer $k$, we say that $t$ behave likes the identity when applied to $k$ if $tk\to_\beta^*k$ (where the integer is represented as a church numeral). We ...
3
votes
1answer
56 views

Understanding a boolean expression in λ-calculus

(NOTE: This is not a homework question at at all. Rather, this was something that I thought that I understood (at least on the surface), but now appear to have no clue about, and am not currently ...
7
votes
1answer
211 views

Y combinator, function composition

I am trying to understand Y combinators. Could you please explain why the following are equivalent (Y (f ∘ g)) (f (Y (g ∘ f))) (Y is a fixed point combination)...
3
votes
1answer
63 views

How to explain/understand brackets of applicative functor [[f u1… un]]?

I am reading article about Applicative Abstract Categorial Grammars http://okmij.org/ftp/gengo/applicative-symantics/AACG.pdf and this article uses brackets [[...]] for action on terms inside ...
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.
14
votes
2answers
1k views

Solving functional equations for unknown functions in lambda calculus

Are there any techniques for solving functional equations for unknown functions in lambda calculus? Suppose I have the identity function defined extensionally as such: $I x = x$ (that is, by ...
2
votes
0answers
259 views

Practical usage of the λ-calculus self-interpreter and the self-reducer?

I came across the paper: "Efficient Self-Interpretation in Lambda Calculus" by Torben Mogensen, 1994: http://repository.readscheme.org/ftp/papers/topps/D-128.pdf It talks about the intepreter $E$ ...
1
vote
0answers
94 views

Is $(X (X X)) ((X X) X) X$ the most simple representation of the identity combinator when $X = \lambda x . x KSK$?

Let combinator $X = \lambda x . x KSK$ as described by Hankin (1994). Then $K = (X X) X$ and $S = X(X X)$. Identity combinator however seems to have much more verbose form. If $I = SKK$ then also $$...
5
votes
0answers
85 views

How could one write typing rules with variables defined at call-site?

I'm trying to write typing rules for a simple language, which is basically a lambda calculus with SSA-like $\phi$-nodes, which basically exchange formal parameters for actual parameters. For ...
44
votes
2answers
4k views

How does the Y combinator exemplify “Lambda calculus inconsistency”?

On the Wikipedia page for Fixed Point Combinators is written the rather mysterious text The Y combinator is an example of what makes the Lambda calculus inconsistent. So it should be regarded with ...
4
votes
1answer
142 views

How logic programming (especially ASP) is related to the reasoning in (first-order) logic?

How logic programming (https://en.wikipedia.org/wiki/Logic_programming, especially answer set programming) is related to the reasoning in the (first-order) logic? Maybe logic programming can be ...
3
votes
0answers
95 views

How to translate lambda calculus into (first-order, modal) logic, is it possible at all?

It is possible (using formal semantics) to translate natural language sentences into lambda expressions. So, is it possible to translate those lambda expressions into some logic, e.g. into first-order ...
5
votes
4answers
216 views

Why don't we encode church numerals like this?

I think the following encoding also works. ZERO := λf. λx. x ONE := λf. f TWO := λf. f f THREE:= λf. f (f f) Note: the original encoding is ...
4
votes
1answer
103 views

Higher order rewriting theory and critical pairs with the beta rule

In a higher-order pattern rewrite system, one specifies rewrites on beta normal forms of terms. Is it possible to have a rewrite like: $\gamma := \lambda x . F(m) \to F(\lambda x . m)$ for some ...
2
votes
1answer
121 views

Is this DO LET sugar considered pure Lambda calculus and nullipotent / side-effect-free?

I'm thinking these familiar concepts of DO and LET/LET* in the context of Lambda Calculus (...
1
vote
0answers
187 views

How to evaluate is_empty for 2-tuple lists in Lambda calculus?

This question has been handled various ways, but let me show my case. I want to find out, if the given list is empty with these constraints: ...
2
votes
1answer
90 views

Unrolling closures into SAT boolean formula

I need to verify some assertions about the minimalist Turing-complete language Jot. Many of the assertions I want to investigate are semi-deciable (co-recursively enumerable). So far it's been fairly ...
2
votes
0answers
63 views

Can't evaluate original Y combinator, two other variants do work, what do I miss?

I have made an evaluator of Lambda expressions. I tried to do Y combinator, but for some reason I can't get the original one working: $$λf.(λx.f \space (x \space x)) \space (λx.f \space (x \space x))\...
5
votes
1answer
311 views

Can lambda-calculus be used for knowledge representation?

Natural language semantics (in computational linguistics) uses lambda terms for expressing the semantics of natural language sentences. There is vast literature about combinatorial categorial grammars ...
2
votes
0answers
69 views

Examples of continuations in pure mathematics [closed]

I am not a computer scientist and have no knowledge of programming. However, I wondered continuations occur as natural and interesting mathematical structures, perhaps as algebraic or type theoretic ...
4
votes
1answer
104 views

How to express modalities in lambda calculus - are some extensions required?

Lambda calculus can be used for encoding semantics of natural language, e.g. http://yoavartzi.com/tutorial/ contains full details about semantic parsing of natural language: converting natural ...
2
votes
1answer
71 views

Lambda calculus :Will there be any x left after first substitution?

I found the following set of lemma in my lambda calculus textbook : Lemma 1.16 Let $x, y, v$ be distinct (the usual notation convention), and let no variable bound in $M$ be free in $vPQ$. Then ...
4
votes
1answer
268 views

Semantic readings of the Lambek sequent calculus

I am reading Categorial Grammar: Logical Syntax, Semantics, and Processing by Glyn Morrill and I am stuck with the Fig. 3.9: Can someone explain this set of formulas and |.| function specifically? ...
3
votes
1answer
112 views

Lambda calculus : what about the bound variables in substituting expression?

I found the following set of lemma in my lambda calculus textbook : Lemma 1.16 Let $x, y, v$ be distinct (the usual notation convention), and let no variable bound in $M$ be free in $vPQ$. Then ...
2
votes
0answers
199 views

Recursive definitions, How it is done?

I read that recursive definitions, refer to the definition of a function in that function body, cannot be done in $\lambda$-calculus, but recursion can be achieved by using $Y$ combinator. As I know, ...
1
vote
1answer
919 views

Understanding church numerals

I am learning lambda calculus as my previous questions indicate . But in a different book , namely , The structure and interpretation of computer program I cam across the concept of "church numerals "...
1
vote
1answer
397 views

When is a variable bound or free in a lambda application?

I am currently reading the book "An Introduction to Functional Programming through Lambda Calculus" (the 2011 edition) and am a bit puzzled by the definitions of free and bound variables ...
13
votes
3answers
426 views

What's the difference between a calculus and a programming language?

I think I'm pretty confused about what's called a calculus and what's called a programming language. I tend to think, and might have been told, that a calculus is a formal system for reasoning about ...
5
votes
0answers
134 views

Characterization of alpha-equivalence in languages with bindings

Following up on this post denoting $(x \leftrightarrow y)$ the permutation of $x$ and $y$ and $P[x \leftrightarrow y]$ the term obtained from the term $P$ by permuting $x$ and $y$ (so for example if $...
3
votes
1answer
193 views

Lambda calculus :difficulty in getting hang of induction and conversion

I am going through the book on lambda calculus by Hindley and Seldin . They introduce the syntactic equivalence of expressions and proving them by a technique named "induction" , which has ...
7
votes
1answer
702 views

Algorithm for deciding alpha-equivalence of terms in languages with bindings

I am interested in the alpha equivalence relation in languages with variable bindings, such as: ...
2
votes
1answer
142 views

Is the lambda calculus referentially transparent?

In an answer of this Reddit discussion somebody defines referential transparency (RT) as "a context $K[ ]$ is RT if, for all $M$ and $N$ s.t. $M = N$, then $K[M] = K[N]$". Based on this definition, ...
5
votes
0answers
165 views
2
votes
1answer
292 views

Lambda Calculus - free vs. bound variables

While I am reducing the following term, I encountered a little Problem: $$(\lambda w x. w x)(\lambda w x. w x) \rightarrow_\beta (\lambda x.(\lambda w x. w x) x)$$ Now my first question: Why is it ...
9
votes
1answer
1k views

λ -calculus : What is the most efficient in memory representation of functions?

I would like to compare performance of function encoded (Church's / Scott's) vs classically encoded (assembler / C) data structures. But before I do that I need to know how efficient is / can be ...
2
votes
0answers
119 views

Growth of non-terminating beta reductions in lambda calculus

There are some terms in lambda calculus that don't really have a normal term. My question is for a term like the following: $$T \overset{def}{=} \lambda f. (\lambda x. \; f \; (f \; (f \; x)))$$ $T$ ...
6
votes
0answers
73 views

Are there simple core languages which are consistent and expressive?

The Calculus of Constructions is a very simple core functional language with dependent types. Per curry-howard isomorphism, it could, potentially, be very useful for writing programs and proofs. It, ...

1 2 3
4
5
9