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 18:56] vkuncak |
sav08:homework05 [2008/03/20 19:04] vkuncak |
||
---|---|---|---|
Line 1: | Line 1: | ||
- | ====== Homework 05 - DRAFT due 2 April 2008 (after break) ====== | + | ====== Homework 05 - due 2 April 2008 (after break) ====== |
===== Problem 1 ===== | ===== Problem 1 ===== | ||
Line 28: | Line 28: | ||
**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 38: | ||
* 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 58: | ||
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. | ||
- |