User Tools

Site Tools


plt17:assignment_2

Differences

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

Link to this comparison view

Both sides previous revision Previous revision
Next revision
Previous revision
plt17:assignment_2 [2017/09/30 23:32]
hossein [Task 1]
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.
-Note that there are several ways to define a set in Coq. You may want to use the Coq.Msets from the Coq library. The other way is to use the mathematical definition of a set. A set can be defined using a  predicate $P(x)$ that determines if an object belongs to the set or not $\{x | P(x)\}$. ​+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.  Set is a collection of objects for which $P$ is true. 
-You can write a function that gets a variable and determines if it is free in a λ-expression or not+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''​.+''​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 31: 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.1506828749.txt.gz · Last modified: 2017/09/30 23:32 by hossein