IN.5021 Formal Methods Flashcards
1
Q
Hoare triple
A
{P} S {Q}
P = a precondition, assumed to be true before execution of S
S = a sequence of statements
Q = a postcondition, will be true after execution of S
indicate: if P is true, then executing S will make Q true
2
Q
primed notation: x’
A
x’ refers to the value after the execution of a program and its unprimed notation x refers to its value before the program execution
3
Q
primed notation: x’
A
x’ refers to the value after the execution of a program and its unprimed notation x refers to its value before the program execution
4
Q
program annotation
A
a predicate, an assertion
it states what is assumed to be true when the program reaches that point of execution
5
Q
partial correctness
A
a desired result is achieved
6
Q
program verification
A
in general impossible to do
7
Q
partial correctness
A
a desired result is achieved (after a loop has come to an end)
8
Q
termination
A
when a loop definitely will come to an end
9
Q
total correctness
A
= partial correctness + termination
10
Q
partial correctness: (loop) invariant
A
a loop invariant is a logical formula that is true
- before the loop
- before each execution of the loop body
- after each execution of the loop body
- after the loop
-> you have to invent an invariant!
11
Q
(loop) variant
A
- an integer-valued expression
- value that can change over time
- is decreased at least by 1 in each execution of the loop body
- cannot go below 0
12
Q
invariant inv
A
an invariant is something you have to find, invent
- true after initialization
- precondition to the loop body
- true after execution of loop body
13
Q
interpretation I
A
is a truth-value assignment to propositional variables P, Q, …
14
Q
satisfiability
A
F is satisfiable iff notF is not valid
- > there is some interpretation I that makes F true
- > I makes notF false
- > not all interpretations make notF true (because I doesn’t)
15
Q
validity
A
F is valid iff notF is not satisfiable
- > all interpretations make F true
- > no interpretation makes F not true (false)
- > no interpretation makes notF true
16
Q
negation normal-form
A
if and only if negations appear only directly in front of variables, i.e. they appear only in literals, and the formulas contain only disjunctions and conjunctions
17
Q
domain and range
A
incl. negation normal form
cf. 2-Proposi…pdf slide 14
18
Q
disjunctive normal form
A
A formula F is in disjunctive normal-form, if and only if it is in negation normal-form and it is the disjunction (OR) of conjunctions (AND).
-> incl. negation normal form
19
Q
resolution
A
aims at deciding satisfiability
20
Q
deciding satisfiability
A
- via truth table (but O(2^n) space)
- SAT algorithm (only O(n) space)
21
Q
SAT algorithm
A
capable of checking the satisifability of a formula
- recursive
- tries out truth table but sequentially
22
Q
busy beaver
A
just a TM that can write a sequence of 1’s on the tape
- > when it stops: the output is the number of 1’s it wrote on the tape
- > is non-computable because …
23
Q
busy beaver function
A
given a number n, what is the MAXIMAL output such a busy beaver can produce when the BB has n+1 states
24
Q
decision problem
A
TM only says “yes” or “no”
25
turn computational problem into decision problem
by giving the TM two strings v and w and ask whether the TM on input v will produce output w
26
language acceptance
about decidability
27
language acceptance
about decidability
28
recursively enumerable languages
languages that are accepted by Turing machines
29
recursive language
like r.e. language but guaranteed to stop in a non-accepting state
30
when is a problem decidable?
the languages that encode the problem must be recursive for the problem itself to be decidable
if language is r.e. then the TM might not stop for a given input w and then we would not know whether w is a solution to the problem or not or whether we had just not waited long enough
31
intractable
(also called "NP-hard")
is a problem to which an algorithm solving the
problem does exist, but it is so inefficient that it is considered as practically useless
i.e. it takes so much time for bigger instances of the problem that it's useless
-> also called beyond-polynomial-time algorithms
32
tractable
- polynomial-time algorithms are perceived as tractable
| - beyond-polynomial-time algorithms are perceived as intractable
33
diagonalization language
no TM accepts it
34
acceptance by a TM
such a language L is recursive
| the TM always stops
35
pseudo/partial algorithm
could run forever
| --> for recursively enumerable languages
36
reduction
- a reduction is an algorithm for transforming one problem into another problem
- a reduction from one problem to another may be used to show that the second problem is at least as difficult as the first
- is a transformation from one input alphabet to another input alphabet such that this transformation must be computable
- > there is a TM that always stops and does the transformation
37
if the complement of a language L is not RE
then the language L is not recursive only RE
38
L_u's complement is not RE
by reduction from L_d
39
partial algorithm vs algorithm
may run forever vs always stops
a partial algorithm = a strategy that may be successful or may not, if successful we can trust the outcome, otherwise we cannot because it may never say yes or no
40
property of the RE languages
is just a set of RE languages (those that satisfy the property).
e.g. there is at least a word in the language that contains a symbol the digit 2
41
property of the RE languages
is just a (sub-)set of RE languages (those that satisfy the property).
e. g. there is at least a word in the language that contains a symbol the digit 2
- if the property were false then it would be the empty set (no language will satisfy false)
42
a language
a set of strings all of which are chosen from some E*, where E is a particular alphabet
43
a recursively enumerable language
a language has a TM that accepts it
- > the TM is a finite representation of that language
- > that TM has the property that its encoding is just a string of 0's and 1's
- > the encoding of TM (a single string) is a representation of the language (= a set of strings)
44
decidability
tbd...
45
TM
a R/RE language has a TM that accepts it
- > the TM is a finite representation of that language
- > that TM has the property that its encoding is just a string of 0's and 1's
- > the encoding of TM (a single string) is a representation of the language (= a set of strings)
- > a TM is a finite representation of something that is infinite (e.g. a TM that accepts all even numbers)
46
a decidable property P
a property P is decidable iff the language L_p, which represents P, is a decidable language => if it is recursive
47
Rice theorem
Every nontrivial property of the RE languages is undecidable
48
an undecidable problem
a problem to which no algorithm solving the problem exists
49
L_u
a RE language -> there is a partial algorithm (= a strategy that may be successful or may not, if successful we can trust the outcome, otherwise we cannot because it may never say yes or no)
50
a "problem"
is about membership of a string in a language
in automata theory, a "problem" is the question of deciding whether a given string is a member of some particular language
=> anything we more colloquially call a "problem" can be expressed as membership in a language
51
an intractable problem
a problem to which an algorithm solving the
| problem does exist, but it is so inefficient that it is considered as practically useless
52
an intractable problem
a problem to which an algorithm solving the
| problem does exist, but it is so inefficient that it is considered as practically useless
53
beyond-polynomial-time = intractable
in general, beyond-polynomial means "exponential"
| but there are functions that are between the polynomials and exponential functions
54
complexity classes
P and NP
55
complexity class P
-> P is class of all problems aka all languages that are recursive s.t. the algorithm does not take more than polynomially many steps, that algorithm is represented by a deterministic TM
If for a problem P there exists a deterministic TM M such that M solves P (i.e. L(M) = P) in polynomial time, then we say that P is in complexity class P
56
complexity class NP
-> NP is class of all problems that can be solved by non-deterministic TM in polynomial time (remember: there is this unbounded parallelism!)
If for a problem P there exists a non-deterministic TM M such that M solves P (i.e. L(M) = P) in polynomial time, then we say that P is in complexity class NP
57
P is contained in NP but not vice versa, why?
-> there are problems in NP that cannot be solved by a deterministic TM in polynomial time
58
unbounded parallelism
possible in NTM
59
is there a witness in NP but not in P?
no ones knows.
But if NP != P then I can characterize problems that would have to be outside of P
-> describe most difficult problems in NP -> then, are those problems outside of P?
we know that P is a subset of NP (just by definition of those two classes)
60
polynomial-time reductions
sl, 63 in 4-pdf
P1 reduces to P2 in polynomial-time
61
running time of algorithms
is equivalent to running time of deterministic TM
| algorithms as we have them in CS are those that are represented by deterministic TMs
62
NP-hard
- a problem H is NP-hard when every problem L in NP can be reduced in polynomial time to H
- for a problem Q it is proved that any other problems of NP can be reduced to Q, but the first line (slide 67) is not yet proved (i.e. that Q is in NP), then such a problem Q is called NP-hard
63
NP-complete problem
a decision problem is NP-complete when it is both in NP and NP-hard
believed to be intractable
-> there does not exist a polynomial time algorithm that solves the NP-complete problems
64
satisfiability problem for propositional logic
is an NP-complete problem!
65
SAT problem
- SAT is an NP-complete problem
- > can be solved by an NTM in polynomial time (all truth assignments are tested in parallel)
- > it is NP-hard meaning that all problems in NP can be reduced in polynomial time to this problem SAT
66
NP problem characterized
an NP problem increases in difficulty in a non-polynomial way (-> NP) / the rate at which a problem gets harder defines it as a truly difficult problem
e.g. factorization
67
nature of computation
we're talking about how the difficulty scales up as you make the problem bigger and bigger
68
polynomial time
An algorithm is said to be of polynomial time if its running time is upper bounded by a polynomial expression in the size of the input for the algorithm, i.e., T(n) = O(n^k) for some constant k.
Problems for which a deterministic polynomial time algorithm exists belong to the complexity class P.
Polynomial time is a synonym for "tractable", "feasible", "efficient", or "fast".
E.g. maximum matchings in graphs;
69
The complexity class NP
The complexity class NP is a set of problems whose solutions can be verified in polynomial time, even if finding those solutions takes — as far as anyone knows — exponential time
70
partial correctness and invariant
- A meaningful invariant will make the postcondition of the loop true
- partical correctness: When, after the loop has come to an end, a desired result is achieved (desired result: the post condition)
71
termination and (loop) variant
- (loop) variant is an expression that is decreased at least by 1 in each execution of the loop body
- cannot go below 0
- by means of the variant and 1 Hoare triple termination of a program is proved
72
computable vs decidable
a problem is computable if and only if its corresponding decision problem is decidable
73
decidable problem
a TM can answer yes or no to a given input.
So decidability has to do with "language acceptance"
74
a language encodes a problem
...
75
problem vs language
a problem is really a language
76
direction of reduction
the only way to prove a new problem P2 to be undecidable is to reduce a known problem P1 to P2 (and not reduce P2 to some known undecidable problem P1!).
That way, we prove the statement "if P2 is decidable, then P1 is decidable". The contrapositive of that statement is "if P1 is undecidable, then P2 is undecidable". Since we know that P1 is undecidable, we can deduce that P2 is undecidable.
If we are given a problem P1, for which we can show that if it were decidable, an already known undecidable problem P2 would be decidable, then P1 must be undecidable. We say we reduced P2 to P1.
e.g. We do so by reducing SAT first to CSAT and then CSAT to 3SAT.
77
contrapositive
every if-then statement has an equivalent form that in some circumstances is easier to prove.
The contrapositive of the statement "if H then C" is "if not C then not H"
-> a statement and its contrapositive are either both true or both false, so we can prove either to prove the other
78
system state
the purpose of a state is to remember the relevant portion of the system's history
79
automata
study the limits of computation
80
decidability
| decidable
what can a computer do at all?
| the problems that can be solved by a computer
81
intractability
| tractable
what can a computer do efficiently?
the problems that can be solved by a computer using no more time than some polynomial growing function of the size of the input.
82
deductive proofs
p. 6
83
proof by contradiction
you assume that the conclusion is false
- then use that assumption, together with parts of the hypothesis, to prove the opposite of one of the given statements of the hypothesis. Then show that it is impossible for the conclusion to be false. The only possibility that remains is for the conclusion to be true whenever the hypothesis is true. That is, the theorem is true.
84
a formal proof
the purpose is to convince someone about the correctness of a strategy you are using in your code. If it is convincing, then it is enough; if it fails to convince the "consumer" of the proof, then the proof has left out too much.
85
prove if-else
| prove while-loop
2 Hoare triples
| 3+1 Hoare triples
86
complexity theory
in this field, we are interested in proving lower bounds on the complexity of certain problems.
87
NP-hard vs NP-complete?
A decision problem H is NP-hard if there is a polynomial-time reduction from an NP-complete problem G to H.
As any problem L in NP reduces in polynomial time to G, L reduces in turn to H in polynomial time
88
P: polynomial time
NP: nondeterministic polynomial time
P: quickly solvable problems (e.g. multiplication, sorting)
NP: quickly checkable problems (includes search problems such as graph coloring, TSP, scheduling), solved with searching (hard)
89
is P1 more difficult than P2?
problem P1 is more difficult than a problem P2 when P1 cannot be solved in polynomial time whereas P2 can
90
P1 <
P1 reduces to P2 in polynomial time (P2 is the known problem here)
91
BCP
Boolean Constraint Propagation
92
Idea of Cook's theorem
Construct the propositional formula (phi) that is satisfiable IFF the truth values assigned to its propositional values correspond to a correct
encoding of an accepting computation of NTM M, i.e. some input w is in P
93
polynomial algorithm
e.g. n, n log n, n^2, n^10
```
An algorithm is said to be of polynomial time if its running time is upper bounded by a polynomial expression in the size of the input for the algorithm, i.e., T(n) = O(n^k) for some constant k
-> Problems for which a deterministic polynomial time algorithm exists belong to the complexity class P
```
94
a problem is NP-hard...
some problems L are so hard that although condition (2) (=every language in NP reduces to L in polynomial time) is proven, condition (1) is not: that L is in NP.
If so, we call L NP-hard.
L is very likely to require exponential time or worse.
NP-hard =~ intractable
95
what does "undecidable" mean?
if a language L is not recursive, then we call the problem expressed by that language "undecidable"
```
a decidable "problem" is really membership of a string in a language L which is recursive, i.e. there exists a TM (informally "an algorithm") s.t. if w is in L, M accepts and if w is not in L, then M halts without accepting.
So problem (=language) L is "decidable" if it is a recursive language, and it is called "undecidable" if it is not a recursive language (e.g. a RE language whose TM may not halt and give us a sense that "the problem is not solved")
RE languages (e.g. L_u) have some TM, non-RE languages (e.g. L_d) have no TM
```
96
a problem that is in RE but not recursive
| a language that is not in RE
L_u
| L_d (no TM accepts it)
97
recursive and RE languages
the languages accepted by Turing machines are called recursively enumerable (RE), and the subset of RE languages that are accepted by a TM that always halts are called recursive
98
FOL is undecidable
proof by reduction from L_u to validity of FOL
99
FOL can represent a TM
yes
logical view vs operational view
-> machines and logic are very frequently the same
