LARA

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
sav07_homework_1 [2007/03/17 19:44]
vkuncak
sav07_homework_1 [2007/04/12 21:34]
vkuncak
Line 1: Line 1:
 ====== SAV07 Homework 1 ====== ====== SAV07 Homework 1 ======
  
-Here is the {{hw1.pdf|Homework 1 PDF}}.+Here is the {{hw1.pdf|Homework 1 PDF}} (with some corrected typos).
  
 Here are some example ocaml programs that may help you get started with using ocaml (but see also http://​caml.inria.fr/​ ).  Please remove the .txt extension Here are some example ocaml programs that may help you get started with using ocaml (but see also http://​caml.inria.fr/​ ).  Please remove the .txt extension
Line 7: Line 7:
   * {{formulas.ml.txt}}   * {{formulas.ml.txt}}
   * {{maps.ml.txt}} ​   * {{maps.ml.txt}} ​
 +Note that you will need to use a slightly different syntax tree compared to one in formulas.ml,​ because the quantifiers in your homework are bounded.
 +
 +See also [[Notes on Context-Free Grammars]].
 +
 +Here is [[SAV07 Homework 1 Solution]] for the theoretical part.
 +
 +NOTE: A formula of the form
 +
 +  forall x < 0. F
 +
 +should always evaluate to true when x ranges over non-negative integers, regardless of F.  Namely, there are no such non-negative x, so this is the case of a bounded quantifier over an empty set.  This formula is trivially true because it is equivalent to
 +
 +  forall x. false -> F
  
-[[SAV07 Homework 1 Solution]] will be available only after the due date.