---
# System prepended metadata

title: 'MCAL : TD1'
tags: [lambda-calcul, '2021']

---

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

## Exercice 1 : Arbres syntaxiques
![](https://i.imgur.com/KWZSHI9.png)
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

![](https://i.imgur.com/qcjwS7T.png)





| 1. ![](https://i.imgur.com/Yg1Lkjs.png) | 2. ![](https://i.imgur.com/48jYyOQ.png) | 3. ![](https://i.imgur.com/CeTD5FW.png) |
|:--------------------------------------- | --------------------------------------- | --------------------------------------- |
| 4. ![](https://i.imgur.com/Fj6KIVf.png) | 5. ![](https://i.imgur.com/MgDe1SU.png) | 6. ![](https://i.imgur.com/X2p3OoE.png) |

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

![](https://i.imgur.com/GWR0yqm.png)

## 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 ![](https://i.imgur.com/2Rv2pOZ.png).
Une varaible libre est surlignée ![](https://i.imgur.com/L0l3nQx.png).

1. λx.x y
![](https://i.imgur.com/0ebtfCh.png)

   
2. λv x y.u v y
![](https://i.imgur.com/viUNpNu.png)

3. λx.x (λy. y x)
![](https://i.imgur.com/DETLHCf.png)
 
4. (λx yz.x z (y z)) u x w
![](https://i.imgur.com/rglWFSL.png)

5. u x (y z) (λx.x y)
![](https://i.imgur.com/Jws2x3Y.png)

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

![](https://i.imgur.com/XHwvDIz.png)
![](https://i.imgur.com/B4tFnvf.png)
![](https://i.imgur.com/0EGUTPF.png)
![](https://i.imgur.com/0ONDk7v.png)

## 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
```coq
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.
```coq
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
```coq
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 