plt17:assignment_2

This shows you the differences between two versions of the page.

Next revision | Previous revision | ||

plt17:assignment_2 [2017/09/27 00:23] hossein created |
plt17:assignment_2 [2017/12/05 14:45] (current) hossein [Task 3] |
||
---|---|---|---|

Line 18: | Line 18: | ||

In this project, you will continue working with the λ-calculus definition from [[plt17:lecture_10|Lecture 10]]. | In this project, you will continue working with the λ-calculus definition from [[plt17:lecture_10|Lecture 10]]. | ||

Define a function that calculates the set of free variables in a λ-expression. | Define a function that calculates the set of free variables in a λ-expression. | ||

+ | A set can be defined using a predicate $P(x)$ that determines if an object belongs to the set or not $\{x | P(x)\}$. | ||

+ | Set is a collection of objects for which $P$ is true. | ||

+ | Define the function ''free'' that gets a variable and determines if it is free in a λ-expression or not. | ||

+ | |||

+ | ''Fixpoint free (x: string) (e: term) : Prop''. | ||

===== Task 2 ===== | ===== Task 2 ===== | ||

- | Prove the following theorem: if two λ-expressions are equal, then their set of free variables should also be equal. | + | Prove the following theorem: if two λ-expressions are equal up to α-conversion, then their set of free variables are also equal. |

===== Task 3 ===== | ===== Task 3 ===== | ||

Line 26: | Line 31: | ||

Prove the following theorem: if a variable does not appear free in a term, then substituting it with any other expression has no effect. | Prove the following theorem: if a variable does not appear free in a term, then substituting it with any other expression has no effect. | ||

+ | ''Theorem subset_fresh : forall e1 e x, ~ (free x e) -> subst e1 x e = e.'' | ||

===== Task 4 ===== | ===== Task 4 ===== | ||

plt17/assignment_2.1506486202.txt.gz · Last modified: 2017/09/27 00:23 by hossein