Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision Next revision Both sides next revision | ||
|
sav08:homework05 [2008/03/20 19:00] vkuncak |
sav08:homework05 [2008/03/25 14:14] piskac |
||
|---|---|---|---|
| Line 1: | Line 1: | ||
| ====== Homework 05 - due 2 April 2008 (after break) ====== | ====== Homework 05 - due 2 April 2008 (after break) ====== | ||
| + | |||
| + | |||
| ===== Problem 1 ===== | ===== Problem 1 ===== | ||
| Line 17: | Line 19: | ||
| Test examples shown in the class: | Test examples shown in the class: | ||
| + | |||
| + | {{test.cnf.txt}} | ||
| [[http://icwww.epfl.ch/~piskac/test.cnf|test.cnf]]. | [[http://icwww.epfl.ch/~piskac/test.cnf|test.cnf]]. | ||
| Line 28: | Line 32: | ||
| **Part a)** Consider an implementation of that definition of sfsubst as a recursive function on syntax trees that directly follows its definition. Consider formulas with many identical quantifiers, $\exists x. \exists x.\ldots \exists x. P(x)$. More precisely, let $F_0$ denote formula $P(x)$ and $F_{n+1}$ denote formula $\exists x. F_n$ for all $n \geq 0$. How many accesses to syntax tree nodes does this function perform on the abstract syntax tree of formula $F_n$? | **Part a)** Consider an implementation of that definition of sfsubst as a recursive function on syntax trees that directly follows its definition. Consider formulas with many identical quantifiers, $\exists x. \exists x.\ldots \exists x. P(x)$. More precisely, let $F_0$ denote formula $P(x)$ and $F_{n+1}$ denote formula $\exists x. F_n$ for all $n \geq 0$. How many accesses to syntax tree nodes does this function perform on the abstract syntax tree of formula $F_n$? | ||
| - | **Part b)** Define the "fast, safe" substitution, fsfsubst, with the property that for a formula with $n$ syntax tree nodes, the number of accesses to syntax tree nodes is $O(n)$. | + | **Part b)** Define the "fast, safe" substitution, fsfsubst, with the property that for a formula with $n$ syntax tree nodes, the number of accesses to syntax tree nodes is $O(n)$. (You do not need to implement it, but this may be helpful if for you to debug your definition.) |
| **Part c)** Prove (using appropriate proof technique) that your definition of fsfsubst has the property | **Part c)** Prove (using appropriate proof technique) that your definition of fsfsubst has the property | ||
| Line 38: | Line 42: | ||
| * one unary function symbol $f$ | * one unary function symbol $f$ | ||
| * one binary relation symbol $R$ | * one binary relation symbol $R$ | ||
| - | * logical operations $\land$, $\lnot$, $\exists$ | + | * operations $\land$, $\lnot$, $\exists$ as the only logical operations. |
| ===== Problem 3 ===== | ===== Problem 3 ===== | ||
| Line 58: | Line 62: | ||
| If a set $S$ of sentences has arbitrarily large finite models (that is, for every $n$, there exists a model $(D,\alpha)$ with $D$ a finite set of at least $n$ elements), then $S$ has an infinite model. | If a set $S$ of sentences has arbitrarily large finite models (that is, for every $n$, there exists a model $(D,\alpha)$ with $D$ a finite set of at least $n$ elements), then $S$ has an infinite model. | ||
| - | |||