# Questions tagged [lambda-calculus]

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

437 questions
Filter by
Sorted by
Tagged with
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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/...
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 ...
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 ...
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: ...
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 ...
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 ...
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)...
63 views

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.
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 ...
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$ ...
94 views

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 ...
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 ...
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 ...
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 ...
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? ...
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 ...
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, ...
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 "...
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 ...
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 ...