3
votes
0answers
43 views

What is the desirable function identification when setting up arrows in the category of types?

My question is which functions can not be allowed in a statically typed programming language, so that the "canonical" category is less coarse than what you get if you define it's arrows to be ...
3
votes
2answers
95 views

Types versus kinds and sorts

In the context of logic, especially Higher‑Order‑Logic and Calculus‑of‑Construction, what is a kind and how does it relates to and differs from a type? My raw guess if that a kind is the higher level ...
6
votes
1answer
126 views

How to prove that these are the only type inhabitants?

Consider a type $$\mathsf{Boolean} = \forall \alpha.\ \alpha \to \alpha \to \alpha$$ with its two inhabitants \begin{align} \mathrm{tt} &= \lambda x.\ \lambda y.\ x \\ \mathrm{ff} &= \lambda ...
0
votes
0answers
44 views

Proof of $(\forall x. \varepsilon(x)) \Rightarrow \bot $ in $\lambda\pi $ calculus $\equiv$

What is the right representation of the proof of $(\forall x. \varepsilon(x)) \Rightarrow \bot $ in simple type theory as a term of $\lambda\pi $ calculus $\equiv$? Note on notation: The epsilon ...
2
votes
1answer
76 views

Simple type theory: Proof inexistance of closed term

In simple type theory, how can I prove that there is no closed term of type? $$((P \Rightarrow Q) \Rightarrow Q) \Rightarrow P$$
1
vote
0answers
33 views

Reductions under lambda in dependently typed lambda calculus

I am currently reading a Simon Thompson's Type Theory book. In chapter 5 he introduces a system TT(0,C), which limits a notion of reduction . In this notion of reduction, reductions under lambda are ...
4
votes
3answers
108 views

What's a good resource to learn about the simply typed lambda calculus?

I've read An Introduction to Functional Programming Through Lambda Calculus by Greg Michaelson, and found it to be a very good resource to learn about the untyped lambda calculus. However, I want to ...
7
votes
4answers
171 views

How or why does intutionistic logic proof negations from within the theory, constructively?

I'm having a little of a cognitive dissonance why, in intuitionistic logic, it's possible to show stentences like $(\neg A \land \neg B) \implies \neg(A\lor B).$ In plain text: If 'A isn't true' as ...
3
votes
1answer
132 views

Give an example of a program in Simply Typed Lambda that produces Bottom.

I'm not sure how bottom applies to simply typed lambda calculus. not A is a common abbreviation for A -> ⊥ But I see no way to construct a function of that signature within the theory. Edit: A more ...
1
vote
1answer
95 views

What can be proven within Simply Typed lambda calculus?

I was reading http://en.wikipedia.org/wiki/Simply_typed_lambda_calculus and I'm having a hard time thinking of anything remotely interesting that can be proven within Simply Typed lambda calculus. Am ...
3
votes
3answers
227 views

Book on lambda calculus logic and type theory

Can someone recommend me a book for self study which will cover topics of logic, lambda calculus and type theory. I know about "Computability and Logic" written by Bolos but it describe recursive ...
11
votes
1answer
649 views

If $f(x)=g(x)$ for all $x:A$, why is it not true that $\lambda x{.}f(x)=\lambda x{.}g(x)$?

There's something about lambda calculus that keeps me puzzled. Suppose we have $x:A\vdash f(x):P(x)$ and $x:A\vdash g(x):P(x)$ for some dependent type $P$ over a type $A$. Then it is not necessarily ...
42
votes
6answers
5k views

Learning Lambda Calculus

What are some good online/free resources (tutorials, guides, exercises, and the like) for learning Lambda Calculus? Specifically, I am interested in the following areas: Untyped lambda calculus ...