# Tagged Questions

For questions on the formal system in mathematical logic for expressing computation using abstract notions of functions and combining them through binding and substitution.

20 views

### Algorithms for type checking, typability and inhabitation problems?

Studying typed lambda calculus, I was asked the following questions: (1) Given a lambda term $M$ and a type $\sigma$, does one have $\vdash M : \sigma$? That is, is $M$ of type $\sigma$? (type ...
14 views

### How to apply a church numeral to a n-ary function?

I was reading about Church encoding, and couldn't figure out some of the grammar of function applications (in terms of church numerals). In particular, the examples I've seen thus far apply to unary ...
39 views

38 views

### Do λ-terms form a group with composition?

Consider obviously as composition the well known combinator $\circ := \lambda f g.\lambda x.f(g x)$. It is easy to see that it associates ($\circ(\circ f g)h \equiv \circ f(\circ g h)$), and that it ...
30 views

34 views

### In lambda calculus what is the correct definition of numbers

As a programmer I have been diving into functional programming and am therefore interested about the math behind all of the languages. I had a small course of lambda calculus at university, but ...
50 views

### Is the combinator $\mathbf{SI}$ typable (à la Curry)?

Consider the combinators $\mathbf{S} \equiv \lambda xyz . xz(yz)$, $\mathbf{I} = \lambda w.w$ and their application $\mathbf{SI}$. Is this term typable à la Curry? From what I did so far, it seems it ...
25 views

### Find recursively enumerable theory $\mathcal{T}_3$ such that $\mathcal{T}_1 \subsetneq \mathcal{T}_3\subsetneq \mathcal{T}_2$.

I am trying to solve the following problem: Let $\mathcal{T}_1, \mathcal{T}_2$ be recursively enumerable $\lambda$-theories such that $\mathcal{T}_1 \subsetneq \mathcal{T}_2$. Show that there ...
36 views

104 views

### What breaks the Turing Completeness of simply typed lambda calculus?

On the Wikipedia page about Turing Completeness, we can read that: Although (untyped) lambda calculus is Turing-complete, simply typed lambda calculus is not. I am curious as to what exactly ...
56 views

### Meta-introduction for implication in Natural Deduction for intuitionistic Propositional Logic

I am going through a paper entitled A Tutorial on the Curry-Howard Correspondence by Darryl McAdams. The author defines a ternary notation as follow to easily manipulate proof trees (page 6 - line 4):...
118 views

### Are untyped and simply typed lambda calculus mutually exclusive?

In "Proposition as Types" by Philip Wadler we can read that: The two applications of lambda calculus, to represent computation and to represent logic, are in a sense mutually exclusive. If ...