|
|
Back to UserFriendly Strip Comments Index
| Poll: assertion notation |
by Michiel |
2008-04-28 13:43:32 |
If you have to write an assertion in a programming language (say, a postcondition for a sorting algorithm) which syntax would you prefer? A notation with quantifiers like 'forall' and 'thereis', or a skolem normal form? For example, here are two versions of the assertion "every int has a successor". In quantifier form:
forall(i)( thereis(j)(i < j) )
And in skolemized form:
i < f(i)
Where a 'forall' is implied for all undeclared variables (i) and a 'thereis' is implied for all undeclared functions (f). So the skolemized version says: "there is a mapping function f for which for all vars i, i < f(i)". Note that in reality, these vars and functions may still have to be declared specifically for this use.
I would like to know which notation is more popular. And with your reply, could you also tell me what your profession/field of study is? It is possible that all software engineers prefer one notation and all mathematicians prefer the other. I will take the outcome of this poll into account when I make my decision on the notation in my programming language.
I'll look at the results in the morning. And I might post this poll again tomorrow.
Thanks in advance for your reply! |
|
[ Reply ] |
|
|
[Todays Cartoon Discussion]
[News Index]
|
|
