# ### Site Tools

plt17:assignment_2

# Differences

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

 plt17:assignment_2 [2017/09/27 00:23]hossein created plt17:assignment_2 [2017/12/05 14:45] (current)hossein [Task 3] 2017/12/05 14:45 hossein [Task 3] 2017/12/05 14:45 hossein [Task 1] 2017/12/05 14:43 hossein [Task 3] 2017/12/05 14:42 hossein [Task 1] 2017/12/05 14:42 hossein [Task 1] 2017/12/05 12:21 hossein [Task 2] 2017/09/30 23:32 hossein [Task 1] 2017/09/27 00:23 hossein created Next revision Previous revision 2017/12/05 14:45 hossein [Task 3] 2017/12/05 14:45 hossein [Task 1] 2017/12/05 14:43 hossein [Task 3] 2017/12/05 14:42 hossein [Task 1] 2017/12/05 14:42 hossein [Task 1] 2017/12/05 12:21 hossein [Task 2] 2017/09/30 23:32 hossein [Task 1] 2017/09/27 00:23 hossein created 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 ===== 