v0.6 ‐ Constructive Negation

In v0.6, we'll mostly be expanding our treatment of negation, which is still a bit limited. Currently, the compiler throws an error if it cannot work with a statement that involves negation or conditionals-you then have the option of changing your statement or using modes.

What we want to allow a higher amount of statements to work.

Constructive Negation

To our knowledge, there isn't a perfect way to negate a generic relation, as in not p(x). The constructive approach still requires,

• The compiler to make a not_p statement for every relation.
• Explicitly asking the compiler to make a not_p relation.

The way we'll be addressing this is,

• Important, commonly-used relations will be converted automatically.
• A bool mode will be added.

The bool mode

bool p(x)
  x!=2

> not p(x)
| x=2

Therefore, in the interest of letting the user better try the logic paradigm, we'll be adding a bool mode.

If the user wants to try constructive negation, they can simply mark a relation as bool.

Changing commonly used statements

The second thing we'll do is make it so commonly used statements can be negated. In practice, a lot of relations used in programming are not arbitrary. By covering relations that are commonly used in a not/if, then the user may not need to even mess with modes.

get, size or has are such that they are likely to be used on a condition.

Adding null

The get statement is changed so that it succeeds with a null value.

Up until now, get would evaluate to false if the element isn't found. The idea was that in a function the mode system would remind you to encase any get in an if-statement. This behavior is changed to at.

fun(t,x)
 if(table.at(t,'x',x))
  true

Why?

> not at(x,1,_) ==> not (existsAt(x,1) and at(x,1,_)) ==> not existsAt(x,1) or not at(x,1,_)

Compare to,

> not x=t[1] ==> x!=t[1]

It's way harder to work negation into our previous operator. However, with our new operator, the negation of t[1]=x is simply t[1]!=x.

• Failure is reified.
• get works with both if (reif) and not.

This is actually a lot better for freestyle scripting or working with pure logic programming.

Although the behaviour of at works for oldschool logic programming, and this can then work with our function mode, our language would then lack support for programming in the rel mode which is set to work only with pure logic operators.

This is somewhat in line with our original idea of modes. The rel mode allows for freestyle programming. The function mode is strict but at the same time it will not attempt to work with pure logic programming.

Using a function

fun(t,x)
 if(at(t,1,x))
  true

Using a relation

rel(t,x)
 if(t[1]=x)
  true

The tictactoe example

It's nice to have a sample program as reference, in order to illustrate what a program looks like in the language. The following code comes from our tic-tac-toe example.

some(col in range(0,2)) //check if a column is filled
	board[0][col]=piece
	board[1][col]=piece
	board[2][col]=piece

You may apply negation to such statements by using the bool mode or simply the not operator.

It would result in the following code,

for(col in range(0,2))
	board[0][col]!=piece or	board[1][col]!=piece or	board[2][col]!=piece

Yup. Just like that, the fabled pure logic negation--what some may call the Holy Grail of Logic Programming, is now a reality in the Cosmos™ programming language.