# Questions tagged [lambda-calculus]

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

549 questions
Filter by
Sorted by
Tagged with
33 views

### What are some visual representations of the lambda calculus?

I'm building some teaching tools for teaching the lambda calculus and would like some kind of visual representation of it. I've looked at Alligator Eggs and while it is something very similar to what ...
1 vote
57 views

### (how) is assignment or binding possible in purely functional languages?

i can't seem to find much info on the following question: how (if at all) is the fixing of names to values (by binding or assignment) possible in a purely functional system like the lambda calculus? i'...
57 views

52 views

### If type theory is one of the foundation of Haskell, why can't you call a function in itself?

Consider this following Lambda expression: $$\lambda s. (s \text{ } s )$$ This function applies it's arguement to it's arguement. If this is a valid lambda expression, wouldn't it also be allowed in ...
52 views

### How to find a term that proves a given proposition?

I'm reading this book, and there's something basic that I don't exactly get. The authors say that every common noun is declared to be a type. For example, $Human:Type$. Then, they give an example of ... 1 vote
44 views

### Finding an inhabitant of $\Pi x: A.\Pi y:B(x). \ast$

Let $\ast$ stand for "type" and $\square$ stand for "kind" so that $\ast:\square$. Suppose I want to find an inhabitant of $\Pi x: A.\Pi y:B(x). \ast$. The derivation rules are ... 30 views

### Where can I find a list of logics with their corresponding calculus and computation phenomena?

I was watching some lectures by Prof. Pfenning on Proof Theory. Between 5:30 and 15:00, he gave a list for some different kinds of judgments along with their calculus and computation phenomena that ...
72 views

### Goedel's theorem, halting problem and irreducible complexity

I have a vague idea on the tip of my mind that I can only convey through examples. Gödel's theorem states that some systems (ZFC, for example) are always incomplete in the sense that new axioms (which ...
1 vote
57 views

### How does "+" operator fit into the formal grammar of $\lambda$-calculus?

In Wikipedia I found out that the formal grammar of $\lambda$-calculus is the following: ...
1 vote
52 views

### How is the direct product of the functions (A -> B) * (C -> D) equivalent to the function (A * C) -> (B * D)? Is there an error here?

In the simply typed lambda calculus we have type algebra - types can be added, multiplied and exponentiated, where addition corresponds to the sum type, multiplication to the product type, and ...
1 vote
52 views

### On the logical and categorical interpretation of lambda calculi and type systems

There is a well-known Curry-Howard-Lambek correspondence between certain type systems, proof calculi and categories. Some variants of Barendregt's pure type systems have the property of strong ...
24 views

### Finding a closed term $t_2$ such that $t_2(λx.x)ss$ = $t_2s$

I'm trying to construct a closed term $t_2$ such that for each closed term $s$, $t_2(λx.x)ss$ = $t_2s$ I know that to solve equations of the shape $. . . u . . .$ = $. . . u . . .$, I'm meant to to ...
1 vote
36 views

### Example of preservation failing in Java - follow up question

This is a follow-up question to my previous question I have been reading this post and it comes up with the following example showing how Java type system is unsound: ...
1 vote
131 views

### Example of progress and preservation failing in a commonly used programming language like Java

I am wondering if my solution is correct or I am on the right track. I have searched online and found a paper about Java type system being unsound but that doesn't really answer the progress and ...
1 vote
37 views

### Simple Lambda Calculus Question [closed]

For any 2 strongly normalizing terms in the Simply Typed Lambda Calculus, s and t, is st also strongly normalizing? And why? I'm a bit confused as this is used in a proof regarding strong ...
1 vote
23 views

1 vote
61 views

### Must the evaluation strategy for a language be specified in order to apply the Church-Rosser Theorem?

The Church-Rosser Theorem  states that the Lambda Calculus (LC) is confluent: between a source expression S and target expression T, the latter in normal form, for any given P, a sequence of ...
65 views

### Is there a hierarchy of computational expressivity that is sensitive to evaluation strategies?

Various computational hierarchies describes the relative expressivity of different classes of languages, machines, or other models of computing, with the classic progression for Automata Theory  ...
1 vote
58 views

### What are distinguishable terms in Bohm theorem?

I have just started to study "Lambda-Calculus and Combinators, an Introduction" by Roger Hindley. There is a formulation of B ̈ohm’s theorem that I can not understand. $M$ and $N$ are terms ...
159 views

### Formal language rewrite rules: strange notation

I'm reading "Program=Proof" by Samuel Mimram, and they use a notation for defining a formal language that I'm not familiar with. Here is how "Program=Proof" defines a formal ...
54 views

### Are there syntactic conditions on divergent $\lambda$-terms?

Probably the most famous example of a divergent term (ie, one which admits infinitely many $\beta$-reductions) in the $\lambda$-calculus is the Y combinator  Y = \lambda f. (\lambda x. f(xx)) (\...
79 views

### What is the lower bound on retrieving an item in a collection if no arrays(Random access memory) are allowed?

I know that retrieving an item in a collection can be done in $O(1)$ time(on average) using hash tables. I would like to know if there is an algorithm that could be as performance without using arrays....
### Turing Machine for the Language $L=\{(a^n)b(a^n)b(a^n) | n\geq0\}$
Turing Machine for the Language $L=\{(a^n)b(a^n)b(a^n) | n\geq0\}$ Here is what I have tried: 1. Starting State Read $a$, Write $x$, Move Right, Go To 2 Read $x$, Write $x$, Move Right, Go To 1 Read <...
Out of curiosity, why do combinators look this way? For example, why is $K = \lambda x y \to x$ and why is it called $K$? Why is it not $\lambda x y f m \to f m x$? These are just arbitrary letters, I ...