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! :)

Grammar

Refining Obelisk's Grammar yet more. Now there is no need for the type terminator #

So the function from last post would now be written.

// An accumulating implementation of the factorial function. Tail recursive.
(Int -> Int)
def factorial x
{
   (fact 1 x)
}
where
{
   (Int -> Int -> Int)
   def fact acc i
   {
      if (i > 0)
         // Recurse
         {(fact (i * acc) (i - 1))}
         // We've recursed enough.  Return.
         {acc}
   }
}

After so much Haskell Programming, I'm liking the syntax without significant whitespace a lot.

Obelisk syntax

I decided to change Obelisk's syntax.

For example, to define a function, you used to do (still the case on the online repository):

// An accumulating implementation of the factorial function. Tail recursive.
((Int -> Int) #
def factorial x
   ((fact 1 x))
   where
   ((Int -> Int -> Int #
   def fact acc i
      ((if (i > 0)
         ((fact (i * acc) (i - 1)))
         (acc)))))) 

That was okay because the syntax is unambiguous and was not affected by whitespace.

However, I thought it would make it clearer whether what you were looking at is a function application or a code block if it were to use curly braces.

This was especially a problem with where clauses! Multiple closing parenthesis are very ugly.

So the above function will now be written as:

// An accumulating implementation of the factorial function. Tail recursive.
(Int -> Int) #
def factorial x
{
   (fact 1 x)
}
where
{
   (Int -> Int -> Int) #
   def fact acc i
   {
      if (i > 0)
         // Recurse
         {(fact (i * acc) (i - 1))}
         // We've recursed enough.  Return.
         {acc}
   }
}

It looks much tidier, and still doesn't care about whitespace, which is great.

Edit: I'm still not so happy with it. The if statement looks ugly. Perhaps ruby style do and end would look nicer.

Edit2: Fixed it, removed need for functional application parenthesis around if expression.