CARPS repository

Hi, just putting out a shout about carps: it has a repository now.

Another couple of hacking sessions and it'll be ready for mod writing.

Also, I realized the underlying protocol would be useful for writing other systems which communicate over email. Strategy games come to mind.

mud

From writing my little projects I've learned one thing:

I cannot do very much.

It's a bit sad really, but it's true. However this knowledge now empowers me!

Ironically, I'm applying the lesson by taking on another project. However, I have structured it around having other people write all the code :)

It is: an rpg engine, for dungeon master and players, which uses email as a protocol. Hence to play, you only need an email address, and no one needs to own a server.

Game rules and interfaces will be implemented as mods. Hence, initially, I only need to write the lower level software.

I will post the repository soon!

New look

I made this blog less eye hurty. The existing css frightened me so I deleted most of it and rewrote some.

Thus some things may not work! Especially on *your* browser.

Re the algorithm in last post.

That the graph contains an 'implies not' relationship is a pre-condition of using the algorithm. For my application, this is also fairly easy to do.

There has to be some sort of check to ensure that you're not getting stuck in an infinite loop - this is done by checking you're not redundantly updating the implication_set.

There will be a finite, and for todays hardware, small number of atoms. This means the implication_set could be represented as a 1 dimensional array. Therefore set insertion and lookup can be done in constant time O(1).

I wrongly stated that the working from one graph can be insert into another. It CANNOT be.

The stack need not grow - we could have a data structure to which work could be pooled, and then executed after the stack has shrank again.

The setInterval function may be useful for implementing the algorithm in javascript - that way we can run a long computation without freezing the browser.

Optimized algorithm later :)

Fast software lolz

Re the last post, quest for propositional logic validation in O(N)

Firstly, since this post contains algorithms, I'd better say:

The algorithms described in this post, are copyright John Morrice, 2010, under the GNU Free Documentation License. http://www.gnu.org/licenses/gpl.html


.......where were we?
Unfortunately, the input will certainly NOT be well formed.

But I think I have such an algorithm. First, a concrete example.

First, a key.
P->Q
or similar arrows
means P implies Q

That is, Q must be true when P is true.

P-!>Q means P implies not Q. That is, Q must not be true when P is true.

Now the example:
What we will receive is a graph. It's simple, but has enough sophistry.

A-!>C
|   ^
|   |
v   |
B----

So what can we do?
Well first, it's fairly efficient to find which atoms are not implicated. In my particular application, I reference counting works well, since the graphs are created by user input. If each atom counts the number of other atoms which implicate it, the overhead of this would be constant. Which is good.

So we find A is not implicated. IMPORTANTLY, this means it has an empty implication set.

We see A->B. And A-!>C. We ALWAYS look at implications first.

B gets A's empty implication set, and adds A to it.

We see B->C. C gets B's implication set, and adds B to it.

Now we try the other path, A-!>B. We see that B has A in its implication set, and note that there is a contradiction.

What just happened?!

The algorithm:
Find unimplicated atoms, As.
For each A in As, validate(A, empty).

Validate(A, implication_set):
Set A.implication_set to a clone of implication_set
Get Is, the atoms implicated by A.
Get NIs, the atoms implicated to not be true by A.
For each I in Is, validate(I, insert A into implication_set)
For each NI in NIs, Contradiction?(NI, A)

Contradiction?(C, A):
if A is member of C.implication_set
then there is a contradiction

Comments:

This algorithm works along sequences of implications. For instance, if we started with:
A-!>B
|   ^
|   |
v   |
C   |
|   |
|   |
v   |
D----

Then when we arrive at C->D and D's implication set would be C's implication set, with C added. Then we arrive at B, and all is as it was before.

Also notice, that either C or D above, could imply not B and the contradiction would still be detected.

Furthermore, assigning an implication set to each atom memoizes the result of the computation. We could take the atoms A B C and D and run them as a part of another graph, without having to recompute the relationships between the atoms A B C and D.

Also note that as a side affect of the memoization, each relationship only needs to be visited once. This means that an optimum implementation of this algorithm will run in O(N) time, where N is the number of relationships in the graph.

However, this algorithm is presented in pseudo code. If you were to try and visualize how it would run on a stack-based machine, you would find it would grow the stack.
What I need is a better implementation of it ;)

Slow software, lolz

I've been trying to make a fast algorithm to validate propositional logic for our little website. I came up with something that I thought was faster, but I just worked out it would take BILLIONS UPON BILLIONS OF EONS to validate worst case input of only size 100.

I don't think a user would enjoy waiting for that length of time!

Edit:

I was getting such long times because I'd assumed the input would be ill-formed: and even in that case I never thought of converting it into well formed sentences. Doh!

Then all you need to do is check for sentences of the form

A_0 implies A_1 .... implies A_n implies NOT A_m where m < n

Fast solution.
For any of A_x in A_n:
if A_x == A_m the sentence is invalid

O(N) time, about 2 lines of code....


...a lot better than my 460 line symbolic reasoning engine I wrote in the last three days which runs at O(N^N).....
I am a tool.

Note to self

Work out computational complexity BEFORE implementing new supposedly 'faster' software

Obelisk

I've been working on the report. Type checking and scoping are done for now. Evaluation will be approached tomorrow. I think I'm going to follow the structured operational semantics as described in "The Semantics Of Programming Languages" by Mathew Hennessy. Lots of reading to do!

I also took some broken modules out of the build tree, so it should build again. I didn't really care before, because the automated tests still compiled and passed :)

Chomp

I'm working on a website for a friend and I needed to chomp. So I worked out the regex.

Here you go.

Javascript:

EDIT: corrected!

// chomp
function chomp(text)
{
   // Check for empty
   if (text.search(/\S/) === -1)
   {
      return "";
   }
   else
   {
      // Chomp it.
      return text.replace(/^\s*((\S+\s+)*?\S+)\s*$/, "$1");
   }
}

Obelisk semantics

I'm just a chuftie, been working on the semantics. Trying to be precise without being too verbose in my logic.

I want to share some, because I'm just happy that the snm math plugin is working well.

In English:

A function definition F only has correct scoping when the set of its where clause constants Wc have correct scoping and the set of its where clause function definitions Wf have correct scopping and its block Fb has correct scoping.

The source (I use '.' to separate constraints for readability):

forsome F.
Fb member F. Fb = Block.
Wc member F. Wc = Set. forall C. C member Wc. C = ConstantDefinition.
Wf member F. Wf = Set. forall G. G member Wf. G = FunctionDefinition.
forsome S. forsome Bq. forsome Wcq. forsome Wfq.
new_scope(Fb, S, Bq). new_scope(Wc, S, Wcq). new_scope(Wf, S, Wfq).
scope(F, S) iff scope(Fb, Bq) and scope(Wc, Wcq) and scope(Wf, Wfq)

Output:

∃ F.
Fb ∈ F. Fb = Block.
Wc ∈ F. Wc = Set. ∀ C. C ∈ Wc. C = ConstantDefinition.
Wf ∈ F. Wf = Set. ∀ G. G ∈ Wf. G = FunctionDefinition.
∃ S. ∃ Bq. ∃ Wcq. ∃ Wfq.
new_scope(Fb, S, Bq). new_scope(Wc, S, Wcq). new_scope(Wf, S, Wfq).
scope(F, S) ⇔ scope(Fb, Bq) ∧ scope(Wc, Wcq) ∧ scope(Wf, Wfq)

Probably doesn't make any sense as I haven't declared what the new_scopes are for the block, where clause elements etc, but I think it looks pretty cool.

snm_math

I've written a math plugin for snm called snm_math

It turns this sort of thing:

forall E. A subset B. E member A implies E member B

Into this:

∀ E. A ⊆ B. E ∈ A ⇒ E ∈ B


And this:

n member R. m member R. m > 1 iff (n / m) < n

Into this:

n ∈ R. m ∈ R. m > 1 ⇔ (n ÷ m) < n

I'm going to go and work on the redraft of Obelisk's semantics now, with nice looking math symbols! :)