Disclaimer: Dieser Thread wurde aus dem alten Forum importiert. Daher werden eventuell nicht alle Formatierungen richtig angezeigt. Der ursprüngliche Thread beginnt im zweiten Post dieses Threads.
Basic Questions
Hi Frederik,
is λ-Calc. only definable with types ι and o? Can we define λ-Calc. without types -or- are types the elements of λ-Calc. for the semantic construction?
What are the main advantages of λ-Calc. and types ι and o independently?
Best,
Pelin
Hi Pelin,
there are different versions of the lambda calculus.
For example, there is the untyped lambda calculus. This allows you to write things like λx.xx, which you can’t do in a typed lambda calculus.
So in a way the untyped lambda calculus is more powerful, but it can also cause all kinds of problems, because e.g. beta reduction doesn’t always terminate.
First-order logic is also typed: it has individuals (over which you can quantify) and propositions.
So it is a very natural thing to use those types during the semantics construction as well.
Ignoring the types for a while and then somehow adding them when we are in first-order logic seems unnecessarily complicated. Additionally, having types during the semantics construction allows us to type-check the semantics construction, which can help us detect and avoid all kinds of errors.
Does this clarify things a bit?
Cheers,
Frederik
type incompatibility check
Hi Frederik,
A point is not clear to me from our today’s conversation. It is about the type incompatibility of run(j).
∀ has a type of (ι -> o)->o.
j has a type of ι.
so we write j as λP.Pj in order to get the type (ι -> o)->o.
run has a type of ι -> o.
My question is: how do we check the type incompatibility by run(∀) and run(j)? By putting the ∀ or j type into run type (((ι → o)->o)->o or (ι → o)).
Best,
Pelin
Hi Pelin,
∀ has type (i → o)->o.
run has type i → o.
This means that run expects an argument of type i.
So we can apply run to ∀, because ∀ is not of type i.
In other words: we are not allowed to say run ∀.
j has type i.
Therefore, we can apply run to j, because run expects an argument of type i.
So we can say run j.
For ∀, we can do it the other way around: ∀ expects an argument of type i → o.
So we can say ∀ run.
Similarly, λP.Pj has type (i → o) → o, which means that we can write
(λP.Pj) run
but we cannot write
run λP.Pj
If we write
(λP.Pj) run
it beta reduces to
run j
which is okay, because j is of type i and that’s exactly what run expects.
So, we check the type compatibility by checking that the arguments we provide have the same type that the function expects.
Does this answer your question?
Best,
Frederik
Yes, thank you.