# Differences

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

Both sides previous revision Previous revision Next revision | Previous revision | ||

sav07_homework_1 [2007/03/18 17:14] 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]]. | See also [[Notes on Context-Free Grammars]]. | ||

- | [[SAV07 Homework 1 Solution]] will be available only after the due date. | + | 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 | ||