# MCAL : TD1
###### tags: `lambda-calcul` `2021`

## Exercice 1 : Arbres syntaxiques
1. (((x y) z) t ) = x y z t
2. ((λx.x) y)
3. (λt.((u t) v)) = λt.utv
4. (λt.(λr.(λu.(λx.z)))) = λt.λr.λu.λx.z


| 1.  | 2.  | 3.  |
|:--------------------------------------- | --------------------------------------- | --------------------------------------- |
| 4.  | 5.  | 6.  |

3. Simplifier au maximum le parenthèsage des termes de l’exercice 2.

| 1/ λxv.x | 2/ λx.xy | 3/ x(y t) |
| --------------- | ---------------- | ------------------------- |
| 4/ λv.λt.λr.uxz | 5/ x y (z t t v) | 6/ (λv.utvr) (y z) (λx.x) |

## Exercice 2 : Abréviations
Donner la notation complètement parenthésée et non abrégée des λ-termes suivants :
1/ (x y z) = **((x y) z)**
2/ λv.u x z = **(λv.((u x) z))**
3/ λv x y.u = **(λv.(λx.(λy.u)))**
4/ λv t r.(u x z) = **(λv.(λt.(λr.((u x) z))))**
5/ λx.(x (λy.y x)) = **(λx.(x (λy.(y x))))**
6/ (u x (y z)(λv.v y)) = **(((u x) (y z))(λv.(v y)))**
7/ (λx yz.(x z (y z)) u v w) = **(λx.(λy.(λz.(((((x(z (y z)))) u) v) w))))**
8/ (w (λx yz.(x z (y z)) u v)) = **(w (λx.(λy.(λz.((x (z (y z))) (u v)))))**

## Exercice 3 : Définitions de fonctions


## Exercice 4 : Variables libres / liées
Pour chaque λ-terme, donner les occurrences libres et liées, puis marquer la portée de chaque variable x.
Une variable liée est soulignée .
Une varaible libre est surlignée .

1. λx.x y

2. λv x y.u v y

3. λx.x (λy. y x)

4. (λx yz.x z (y z)) u x w

5. u x (y z) (λx.x y)

## Exercice 5 : Redexes et Réduction
Souligner les redexes des λ-termes suivants puis les réduire jusqu’à leur forme normale.


## Exercice 7 : Évaluations en Coq
1/ Vérifier pour deux expressions de la section 4 vos résultats pour les variables libres et liées

Definition q11:= \x~x y.
Print q11.
Compute (vliees q11).
Compute (vlibres q11).


Definition q12:= \v x y~u v y.
Print q12.
Compute (vliees q12).
Compute (vlibres q12).

2/ Vérifier pour deux expressions de la section 5 vos résultats pour l’ensemble des redexes et la réduction.

Definition q21:= (\x~x x) (\y~x) (\y~x).
Print q21.
Compute (red_cbn q21).

Definition q22:= (\y~x) ((\y~x)(\y~x)).
Print q22.
Compute (red_cbn q22).

4/ Traduire les λ-termes suivants en expressions lexp

Definition exp1:= (\x y~x) (\a~a) ((\b~b)(\c~c)).
Print exp1.
Compute (show_cbn exp1).
Compute (show_cbv exp1).

`show_cbn` fait une réduction en partant des expressions à gauche
`show_cbv` fait une réduction en partant des expressions à droite
`show_wcbn` fait une réduction
`show_wcbv` fait une réduction