Here you can ask questions and find or give answers to organizational, academic and other questions about studying computer science.

1.1k questions

1.2k answers


546 users

0 votes

Why is S3 alternation-free? 

nu.x depends on y.

I followed the lecture example: 

in * TF "Emb. Sys. and Rob." by (610 points)

1 Answer

+1 vote
Best answer
...but there is no alternation. Both fixpoints, the one on y and the one on x are greatest fixpoints, so that there is no alternation.
by (166k points)
selected by
okay so when we say fixed point operator it only means nu or mu, and not nu.x or mu.y as a whole?

Therefore, same fixed nu so there's no alternation.
Yes, for the alternation, we just consider the mu's and nu's, and just when it comes to decide about the dependence of the fixpoints, the variables matter.
The formula from the question is quite similar to the second bullet point in the examples.

Related questions

0 votes
1 answer
0 votes
1 answer
0 votes
1 answer
Imprint | Privacy Policy