Many tasks in compilation and program analysis (in symbolic computation in general, I suppose) amount to finding solutions to systems of the form (x = f(x)). However, when asked to define algorithms to find such fixed points, we rarely stop and ask “which fixed point are we looking for?”

In practice, we tend to be interested in fixed points of monotone functions: given a partial order ((\prec)), we have (a \prec b \Rightarrow f(a)\prec f(b)). Now, in addition to being a fairly reasonable hypothesis, this condition usually lets us exploit Tarski’s fixed point theorem. If the domain of (f) (with (\prec)) forms a complete lattice, so does the set of fi…

Similar Posts

Loading similar posts...

Keyboard Shortcuts

Navigation
Next / previous item
j/k
Open post
oorEnter
Preview post
v
Post Actions
Love post
a
Like post
l
Dislike post
d
Undo reaction
u
Recommendations
Add interest / feed
Enter
Not interested
x
Go to
Home
gh
Interests
gi
Feeds
gf
Likes
gl
History
gy
Changelog
gc
Settings
gs
Browse
gb
Search
/
General
Show this help
?
Submit feedback
!
Close modal / unfocus
Esc

Press ? anytime to show this help