2. előadás

Típusellenörzési szabályok

ha

t : A -> B   u : A

akkor

t u : B

x : A ⊢ t : B

akkor

(λ x -> t) : A -> B

t típusa B feltéve hogy x típusa A

akkor (aka mindig)

x : A ⊢ x : A

A kötött változók nevei nem számítanak

(λ x -> x) = (λ y -> y) = ...

(λ x -> t) u = t[x -> u]

---
példa:

(λ x -> x + (3 * x)) (2 + 1) = (x + (3 * x)) [x -> (2 + 1)]

átalakul:

(2 + 1) + (3 * (2 + 1))