Pages

Wednesday, 24 June 2015

Another Blog

This post is about what global economic and technological development ought to be.

Logica Bolivia is a new blog. It is for things I think should be taken seriously. You won't read anything there about the University of Cambridge, for example.

Ian

Saturday, 6 June 2015

Why is Telecommunications Security Important?

"Man is a political animal." So wrote Aristotle, somewhere. This does not mean that he tells lies on TV to win votes. It means that the essential nature of man is that he lives in a polis, a community of fellow men, and together they create the conditions necessary for a civilized life. So it is only through cooperation that a collection of individuals form a polis. And a necessary condition for cooperation is that the individuals concerned trust one another.

Consequently, communications security is important, because cooperation at a distance requires communication, and if the medium is not secure then trust is impossible: you cannot trust someone unless you know that you are really communicating with that person, and not an impostor.

The Internet is not secure. So if we want to use the Internet as a medium for cooperation at a distance, then we must first secure it.

The essence of telecommunication is the transmission of actual knowledge, at a distance. That means transmission of actual knowledge through some medium. Telecommunications therefore entails both actual knowledge, and also the existence of the medium. Clearly then, there is no point in securing the medium unless one has first secured actual knowledge.

Now actual knowledge is uniquely the product of a good education. It follows then, that (a) the final cause of telecommunications security is securiung a good education for all involved, and (b) only a good education will secure the medium. Hence we have established two things:
  1. A good education is the sine qua non of secure telecommunications, and
  2. Secure telecommunications is the sine qua non of a good education.
And the reader  will here recognise the form of circular reasoning called pratityasamuhtpada in Sanskrit, typically translated as dependent co-arising in Western texts.

This explains final cause, the description of the phenomenon pre-supposes the conditions under which it is possible to observe that phenomenon, and which pre-conditions are also the effect, or reason for which that phenomenon exists. This reason for existence, Aristotle calls the essence of the thing.

Now the people at Cambridge want to know "Why Bolivia?" and the answer is "Because Bolivia has potential." And since Markus fancies himself a physicist of sorts, from time to time, he knows that the relevant formula is
E = mgh
where, in the Systeme International of units of physical measure, E stands for the energy in Joules, m stands for the mass in kilograms, h stands for the height in metres, and g stands for the acceleration due to gravity in metres per second per second. Now put in some numbers: let g = 9.8, h = 4000, and take m = 1 kg per litre. Then we have that 100 litres of water has approximately 4 megajoules of potential energy. Now consider a modest reservoir, such as Ch'iyar Qullu, which supplies the city of La Paz with fresh water. How many hundred litres of water does it contain, do you think? You may look it up on Google maps, if you like.

Now imagine, if you will, what we could do with a long straight polythene tube, leading from the reservoir, down to a hydraulic ram. Ask Ross Anderson how a hydraulic ram works, in case you don't know. There are all sorts of lovely things one could do with a setup such as this! For example, one side effect of a hydraulic ram is that it compresses the air in the "shock absorber." So we could use it to liquify air at a few meters above sea-level. That might find applications in refrigeration, say, or perhaps we could use it to produce LPG from the hydrocarbons that are conveniently located down there in Teoponte.

Now, for anyone wondering how a polythene tube could sustain the pressure produced by a 4km head of water, then  recall that the compressive strength of polythene is quite considerable. (Ask Nik Thomas of BAE Systems, if you don't believe us. Nik has a degree in materials science from Cambridge, you know.) Now imagine that the polythene tube is embedded firmly in a trench, surrounded a few meters of rock ...

Now ask Ross how high a jet of water could be fired from the ram. And for an extra fish, ask him to calculate the air temperature at the top of the trajectory. So how far could She propell a few metric tonnes of hailstones, each the size of a football? And what is the ceiling of an Iroquois helicopter, or back to this century, an Apache attack helicopter? And how high do military forward ops satellites fly?

So much for gravitational potential!

But there are equally promising possible applications for electrical potential. All along the edge of the Altiplano, there are mountains called the Cordillera Real, and they enjoy frequent electrical storms. Now,  maybe we could find some interesting geological coincidences, involving, say, metal-bearing rock plates, with some dielectric substance sandwiched between them. Discharging a petafarad electrolytic capacitor through a suitable coil, and with a well-designed reflector dish, is unlikely to get FCC approval, but it could nevertheless turn out to be useful, on occasion. How would you like your birds cooked, sir. Charcoal, or vapor?

Well, you know, it goes on and on and on. Try this for a thought experiment: What if She could inject a couple of cubic kilometers of cold water into an opportunistically placed geological fault? How much alluvial metrial couild she wash down into the Pacific? But whatever you do, don't mention a word of this to the Chilean politicos, because they may think it a threat, you see. But She doesn't use threats, unless all diplomatic means have failed. And recall that a diplomatic means that fails is one which is seen by both parties to have failed for the same reason. Otherwise, it could not have been a diplomatic means, could it?

Well, we did tell you, back in 2011, that "Bored little girls play complicated games." This is what happens, you see, when you leave Ian in the streets for a couple of months, with nothing to do. He eventually gets enough cash together to buy 3 BOB worth of 100 % pure cane spirit, and that gets him a couple of hours connect time to the lustrecacho ultranet. Then the next thing you now, the fucker's reincarnated the Inka's answer to Archimedes and Aristotle, and the better part of the Royal Corps of Engineers, all in one.

Wouldn't it have been better if you'd just offered to send him a really good laptop, 64 bit, 4 Gig RAM, half a terabyte disk, you know, standard issue for a shit-pot Royal Society Research fellow, along with half a dozen Raspberry Pis and US$5,000 so that he can get his PT1 sorted out and start teaching Real Spanish computer science to beautiful women?

Then, instead of a pissed, Generally U/S Grant, you would have only had to deal with a dozen happy, polite, grateful, and extremely beautiful women, porting Red October to RP, and making a tera-qubit global quantum super-computer called GOD. Don't you think that would be a better way to start the movie?

You little Cambridge fellows need to get literate! "What he tells you three times is true!" Ian is not going to leave the Plurinational State of Bolivia. So it's not Ian's Bolivian adventure that is going to end, it's your Bolivian adventure that has just begun!

Call it Global Bio-geo-terrorism, if you like. That's why Aristotle didn't write about comedy in the Poetics. The difference between comedy and tragedy, you see, is just the point of view! And 4km is high moral ground.

So try to remember this, next time you hear everyone laughing at you. It helps, really it does! Yes! Even when they're laughing at the whole University!

Check out the band Wara, on YouTube, if you want to hear another example of final cause. And if you still don't get it, look into the history of the University at Sucre. So it seems there's a lovely old University looking for a new lease of life. What's its core competency  going to be then? Inka Military Tech. (with Psi-ops) or Telecommunications Science (with psycho-botany)? If it´s the latter, then you can also open up J-Stor, and while you're about it, digitize the entire contents of the library of the Society for Psychical Research. Don't worry, we'll explain all the bits you don't understand.

Love and kisses,
Alice

Sunday, 3 May 2015

e-mail

e-mail is not what it used to be. So I'm posting the password to my only e-mail account: ian.a.n.grant@gmail.com. The password is M5s3c1lTr3n3ty I imagine some people will be keen to delete some of the things they've sent to me. Maybe someone will make a copy of it before that happens.

Economics and Economics II

I wrote Economics in November 2012 when it became clear that nobody was really thinking about anything I wrote. Nothing seems to have changed much since then.

I am posting it here again, because I am not a pessimist. I stand by the promise I made: we can change the world, and we can do it in 6 months, and we will do it, just as soon as we decide it is worth doing. That is not a difficult decision to make!

Economics II has some of Aristotle's technical details, most of which I do not understand.

The complete text of the two books on ethics, and economics, and mechanics is in The Works of Aristotle. As Bruce Willis says in The Fifth Element "Every weapon has a manual ..." and this is the manual. The weapon against evil is the Human mind.

Makin' Movies

I was impressed by the Aristotelian metaphysics in Interstellar It's a pity they didn't get Einstein's 'joke´ though, and a pity they ended up on the wrong planet.

A race of people that can't govern Wall Street aren't going to be able to manage moving to another planet any better.

Thursday, 30 April 2015

Metric Spaces

I sent this to Laura a couple of years ago. It's about Galois connections and metric spaces, more or less. Another way of putting is to say "What is the difference between Saturday and Sunday, really?"

https://drive.google.com/file/d/0B9MgWvi9mywhZkJqTGdfWmlTUThoR1pHV2NfbVQwRGNpN0c4/view?usp=sharing

Whore Logic

 I did a French course at Cambridge, and the best thing I learned from it was how fantastic is Jacques Brel:
https://www.youtube.com/watch?v=n2kkr0e_dTQ&index=7&list=RDZkZ_ihsn404

For my Mum and Dad

 My parents seem not to believe I'm their son. I grew up listening to this song:

https://www.youtube.com/watch?v=34FMx1t089Q&noredirect=1

Tuesday, 28 April 2015

For H.

Nick Cave
"As I Sat Sadly By Her Side"

As I sat sadly by her side
At the window, through the glass
She stroked a kitten in her lap
And we watched the world as it fell past
Softly she spoke these words to me
And with brand new eyes, open wide
We pressed our faces to the glass
As I sat sadly by her side

She said, "Father, mother, sister, brother,
Uncle, aunt, nephew, niece,
Soldier, sailor, physician, labourer,
Actor, scientist, mechanic, priest
Earth and moon and sun and stars
Planets and comets with tails blazing
All are there forever falling
Falling lovely and amazing"

Then she smiled and turned to me
And waited for me to reply
Her hair was falling down her shoulders
As I sat sadly by her side

As I sat sadly by her side
The kitten she did gently pass
Over to me and again we pressed
Our indifferent faces to the glass
"That may be very well", I said
"But watch the one falling in the street
See him gesture to his neighbours
See him trampled beneath their feet
All outward motion connects to nothing
For each is concerned with their immediate need
Witness the man reaching up from the gutter
See the other one stumbling on who can not see"

With trembling hand I turned toward her
And pushed the hair out of her eyes
The kitten jumped back to her lap
As I sat sadly by her side

Then she drew the curtains down
And said, "When will you ever learn
That what happens there beyond the glass
Is simply none of your concern?
God has given you but one heart
You are not a home for the hearts of your brothers

And God don't care for your benevolence
Anymore than he cares for the lack of it in others
Nor does he care for you to sit
At windows in judgement of the world He created
While sorrows pile up around you
Ugly, useless and over-inflated"

At which she turned her head away
Great tears leaping from her eyes
I could not wipe the smile from my face
As I sat sadly by her side.

Measuring Ignorance

This is an unfinished essay, which dissolves into a message to a friend. I am posting it in this state because I don't have a computer anymore, and as I am living on the streets it is going to be a while before I can do any more work.

https://drive.google.com/file/d/0B9MgWvi9mywhUkU2UlUyRXNlalVXZjU5QVFvVUZVUFg5SC1v/view?usp=sharing

Developing Secure Communications

Two months ago I sent this to the Vice President of the Plurinational State of Bolivia.

It seems the government are in the process of procuring "security appliances" of some kind, and that there is no real interest in developing this capacity locally.

https://drive.google.com/file/d/0B9MgWvi9mywhcnRpeU54RWQ0M1VWbWNkQkUyWTdKd09wSUQ4/view?usp=sharing

Tuesday, 10 March 2015

Securing the Estado Plurinacional with Raspberry Pi

This is a blatant appeal for charitable funding. I have reason to believe that the Estado Plurinacional de Bolivia may be about to face a computer and communications systems emergency scenario. And just so that there is a chance we can do something about it, and in the absence of further funding, I am going to make some network security appliances, out of Raspberry Pi II. So my appeal is for donors to make a donation directly to the distributors, or to  Raspberry Pi themselves, so that someone can organize a consignment by express delivery of some kind. It would be nice to have just one sample here in advance, to test installations, but that may not be feasible. We are going to need a couple of hundred at the very least.

In the happy event that the machines aren't needed for security applications, I can PERSONALLY promise a very long and interesting series of posts on applications of these machines that are very unlikely to have been thought of before. They won't be MY ideas, you understand, because I have never had an idea of my own. You'll have to wait and see, and hope and pray that we don't need them for security ...

Policing the Traffic Cops

I started out musing about how to verify the security of a "secure appliance". It's funny how your mind wanders in this place ...

https://drive.google.com/file/d/0B9MgWvi9mywhMFRYbjV2VC1rdTVHbmlQUThIdHBjb0xrTFVV/view?usp=sharing

Love and Kisses,
Osama Guevara Katari Kaizer Soza xxx

Friday, 30 January 2015

Metacircular Interpretation

(* Buster Testacles and his infeasibly large Monad ... or is it
   Testacles Monad and his infeasibly large Buster ... or is it
   Monad Buster and his infeasibly large Testicles ... ?

   You see, it's worth taking some trouble to get the arguments in the
   right order, so that we can use currying and type-directed partial
   evaluation to compose monadic representations at the same time as
   we compose parsers for those types. And, if we can compose the
   types, then we should be able to compose the semantics too.

   There are also "fringe benefits" to be had --- decidable
   Higher-Order Unification, for example. That sounds useful. ["Higher
   Order Unification Revisited: Complete Sets of Transformations", by
   Wayne Snyder and Jean H. Gallier] It might make HOU decidable for
   any language we interpret in a monad. If so, then that ought to
   make quite a lot of stuff decidable. Peano Arithmetic (PA) for
   example. Then Ladies will be able to understand the proofs in the
   Arithmetica of Diophantus.

   The Arithmetica of Diophantus was written by a Woman. The reason I
   think I know this is that little men, e.g. Heath, don't seem to
   understand it. I know this because Heath asserts as a fact, some
   statement to the effect that ``Diophantus only used a single
   variable in his problems because he couldn't conceive of the notion
   "more than one variable"''.  _Even though_ he observes that
   Diophantus takes great pains to cast problems in two or more
   unknowns into monadic form.

   Heath apparently sees no reason to explain to his readers this
   utterly incredible discovery he has made: which is, how it is that
   the "man" who had apparently invented the notion of using a
   non-numerical symbol, i.e., a _variable,_ to represent an unknown,
   and who had proved dozens and dozens of theorems in arithmetic and
   whose examples frequently used six digit numbers, couldn't
   _conceive_ of the notion of "one variable" generalisng to "two
   variables" or "three variables".

   Heath thus seems to think Diophantus stupid. Yet Heath knows at the
   same time that he (Heath, I mean!) doesn't know how Diophantus
   proved "the porisms" which are referred to throughout the text. It
   doesn't seem to occur to Heath that the author might have had a
   _reason_ for not using more than one unknown value in the
   equations, and that that reason might have something to do with the
   unknown (to Heath) proof methods in the porisms. Maybe the machine,
   "for technical reasons", couldn't automatically generate proofs for
   propositions with more than one hypothetical?

   This is what I see as typical of how little men treat the thought
   of Women when it is so far advanced of their own that they cannot
   even recognise it as thought. They are at best patronising (see
   e.g. Babbage's comments on the work of Ada Augusta Lovelace), or
   they ridicule it. Perhaps that's better than them recognising that
   it _is_ thought, but not being able to understand it, because then
   they get angry and all they can think of doing is trying to insult
   her.

   Now if there is any reader who is scoffing "... and of course both
   Diophantus and Heath would have been completely familiar with
   Eilenberg and Moore, not to mention Moggi!" Well, I won't complain.
   At least you're not insulting me. But if you want to learn
   something, perhaps for the first time in your life, then look up
   what Aristotle writes on the theory of proportionals, in particular
   on the proposition Proportionals Alternate (PA) which is Euclid's
   Prop. V.16. It seems to be about using translations between
   languages to apply the same proof in three different domains:
   logic, arithmetic and geometry.

   But I have to agree with Wadler on one thing: I'm also a fan of
   John Reynolds. What I love about the man is that he writes to
   explain things, not just because he thinks he can make himself look
   clever. And he doesn't make himself look clever, because he
   explains things so well that he makes what he's writing about seem
   utterly trivial. Perhaps that's why so few seem to have heard of
   him, and also why hardly anyone seems to have really read anything
   he's written.

   This is a bit of a problem, because it's _systemic_. There's a
   mechanism in "academia" which consistently acts against anyone who
   thinks and writes clearly, and that means _anyone_ who does work of
   any real lasting value. As Leonard Cohen never dared to say,
   everybody knows that the mediocre is the enemy of the best, but how
   can they know that, really, when even the mediocre is perpetually
   swamped by the utterly useless?

   It doesn't take an academic "genius" to explain what is the
   mechanism either. The problem is _trade_. Human reason is not a
   least-fixedpoint, so it's not effective reason: it's co-effective
   reason, and a greatest-fixedpoint. So actual Human knowledge is
   inherently, necessarily, co-operative. Therefore, if you take
   people whose responsibility is the acquisition and dissemination of
   knowledge, and you force them to compete against each other in "the
   race whose prize is `Daily Bread'" then they are unable to
   co-operate without losing "the prize". Consequently, the good ones,
   who co-operate, and who actually know something, drop out, and the
   winners are ... can you guess?

   Well, by a truly remarkable co-incidence, they all turn out to be
   men who don't have time to read what other men write because
   they're far too busy writing things for those other men to not read
   ...  Now how long can this sort of thing go on before somebody
   cottons on to the fact that what's being published is, well, less
   than mediocre, shall we say? And what's going to happen then? I
   daresay there are a lot of very clever schemes that have been
   thought up to deal with it, so we needn't worry about anything,
   need we ...?

*)

signature Monad =
sig
   type 'a M
   val unit : ('a -> 'b) -> 'a -> 'b M
   val bind : 'a M -> ('a -> 'b M) -> 'b M
   val show : ('a -> 'b) -> 'a M -> 'b
end

signature Interpreter =
sig
   type term
   type result
   val eval : term -> result
end

signature Value =
sig
   type value
   type result
   val showval : value -> result
   val errval : string * string -> value
end

signature Evaluator =
sig
   type environment
   type term
   type value
   type 'a M
   val interp : term -> environment -> value M
end

signature Environment =
sig
   eqtype name
   type value
   type environment
   val lookup : environment -> name -> value
   val bind : environment -> name * value -> environment
   val null : environment
end

functor ListEnvironment
   (eqtype name
    type value
    val error : name -> value)
   :> Environment
      where type name = name
        and type value = value =
struct
   type name = name
   type value = value
   type environment = (name * value) list
   local fun lookup e n =
            case List.find (fn (n',_) => n' = n) e
              of NONE => error n
               | SOME (_,v) => v
         fun bind e p = p::e
   in
      val lookup : environment -> name -> value =
           lookup
      val bind : environment -> name * value -> environment =
           bind
      val null = []
   end
end

structure InterpI =
struct
   type name = string
   structure MonadI :> Monad =
   struct (* This way you see more clearly that the Monad is just a type function *)
      type 'a M = 'a
      val unit : ('a -> 'b) -> 'a -> 'b M
          = fn f => fn x => f x
      val bind : 'a M -> ('a -> 'b M) -> 'b M
          = fn x => fn f => f x
      val show : ('a -> 'b) -> 'a M -> 'b
          = fn f => fn x => f x
   end
   datatype value =
       Wrong
     | Num of int
     | Fun of value -> value MonadI.M
   datatype term =
       Var of name
     | Con of int
     | Add of term * term
     | Lam of name * term
     | App of term * term
   structure Value
      :> Value
          where type value = value
            and type result = string =
   struct
      local
         fun showval Wrong = "<wrong>"
           | showval (Num i) = Int.toString i
           | showval (Fun _) = "<fn>"
         fun errval (_,_) = Wrong
      in
         type value = value
         type result = string
         val showval : value -> result =
            showval
         val errval : string * string -> value =
            errval
      end
   end
   structure Env : Environment =
      ListEnvironment (type name = name
                       type value = Value.value
                       val error : name -> value =
                          fn n => Value.errval ("bind",n))
   structure Evaluator
      :> Evaluator
            where type value = value
              and type 'a M = 'a MonadI.M
              and type environment = Env.environment
              and type term = term =
   struct
      type environment = Env.environment
      type term = term
      type value = value
      type 'a M = 'a MonadI.M
      local
         open MonadI
         fun add (Num i) (Num j) = Num (i + j)
           | add _ _ = Value.errval ("Add","wrong type(s)")
         fun app (Fun k) a = k a
           | app _ _ = unit Value.errval ("App","wrong type")
         fun interp (Var x) e = unit (Env.lookup e) x
           | interp (Con i) e = unit Num i
           | interp (Add (u,v)) e =
                         bind (interp u e) (fn a =>
                         bind (interp v e) (fn b =>
                         unit (add a) b))
           | interp (Lam (x,v)) e =
                          unit Fun (fn a =>
                                      interp v (Env.bind e (x,a)))
           | interp (App (u,v)) e =
                          bind (interp u e) (fn a =>
                          bind (interp v e) (fn b =>
                          app a b))
      in
         val interp : term -> environment -> value M
            = interp
      end
   end
   fun eval t =
      let val env = Env.null
          val m = Evaluator.interp t  env
      in MonadI.show  Value.showval m
      end
end

(*             Wadler calls this "the standard meta-circular
               interpreter". But Reynolds, who coined the phrase, might
               not agree, because this interpreter doesn't
               interpret itself. This is because it doesn't
               represent the abstract syntax and deconstruct it.

               It might be argued that this is merely a nicety, but
               consider the questions Wadler asks, such as "How do we
               compose interpreters in a monad?" And "Can we interpret
               a call-by-need interpreter in a monad?" If the
               interpreters really were meta-circular then the answers
               to these questions would obviously be positive.

               And Wadlers interpreters aren't modular, as he
               claims. They're all one big amorphous blob.

               If you now go and carefully read Reynolds' paper
               "Definitional Interpreters for Higher-Order Programming
               Languages" in Higher-Order and Symbolic Computation, 11,
               363–397 (1998), you will see that the treatment he
               gives there is far, far superior to the one Wadler
               gives, some twenty years later.

               Note, for example, how Reynolds uses recursive symbolic
               _environments_ to implement fixedpoint combinators, and
               how they dissolve in the first-order translation (p.
               381).  The resulting first-order meta-circular
               interpreter is one of the most beautiful 20 lines of
               code I've ever seen: it is just three lambda
               expressions (excluding the trivial wrapper function
               interpret) and one pair of these---eval and apply---are
               mutually recursive. The function eval also calls the
               function get, which is (simply) recursive. One final
               interesting point to note is that eval takes _two_
               arguments: a value, and an environment, which is a kind
               of _state._

               If anyone can show me more recent work that uses this
               idea, with or without attribution, I would be very
               interested to hear about it. I have never come across
               the idea mentioned anywhere else, and it is what a
               mathematician might call "highly non-obvious".

               Another notable feature of Reynolds' treatment is that
               he uses abstract syntax as an informal type
               discipline. All the values used in definitional
               interpreters are for all practical purposes,
               typed. This is from "Definitional Interpreters
               Revisited" in Higher-Order and Symbolic Computation,
               11, 355–361 (1998):

                  In “Definitional Interpreters”, however, closures do
                  not contain lambda expressions, but merely unique
                  tags that are in one-to-one correspondence with
                  occurrences of lambda expressions in the program
                  being defunctionalized. The computations described
                  by these occurrences are moved to interpretive
                  functions associated with the points where closures
                  are applied to arguments. Moreover, within each
                  interpretive function the case selection on tags of
                  closures is limited to those tags that might be seen
                  at the point of application

            .     I’ve been told that this was an early example of
                  control flow analysis in a functional setting, which
                  has inspired some of the extensive development of
                  this area [23]. In fact, however, the limiting of
                  the case selections was not determined by control
                  flow analysis, but by the informal abstract type
                  declarations (called abstract syntax equations) that
                  guided the construction of the original interpreter.

               Something which any reader of the full paper will find
               curious is the fact that Reynolds' for some reason
               implements the successor function and the equality
               relation as bound values in the first four
               interpreters, even though none of the interpreters
               actually use these functions. The answer is perhaps
               that in the last interpreter, which implements
               memories: which are essentially lists of references,
               the successor and equality are the only two primitive
               constants that are needed, And coincidentally this is
               also enough to bootstrap PA.

               So why would anyone want to implement the last
               interpreter in the first one? Perhaps because the first
               one can be implemented pretty easily in any language.

               And that leads to the question "Why would anyone want
               memories in the first interpreter?" Well, memories are
               essentially lists of references to values
               (cf. Reynold's comment quoted above, regarding how
               closures are implemented, and the role of abstract
               syntax as an informal type discipline). So memories
               allow one to implement abstract syntax in the
               interpreter. And that, I think, is why the first
               interpreter is called meta-circular: because it can
               interpret the last interpreter, which can interpret the
               first one. So those first 20 lines of code are enough
               to bootstrap any language which can be described by a
               grammar, i.e. in terms of abstract syntax equations on
               records, and a formal semantics described in terms of
               untyped lambda calculus.

               That would make quite a neat API for the LLVM JIT
               engine, wouldn't it? There's not much that one would
               have to write ad-hoc, and then from any scripting
               language, one could interpret interpreters with a
               full-on assembler, capable of optimising tail-recursive
               calls, and handling and throwing exceptions, and all
               this running in native machine code on half a dozen
               different processor architectures. And an API like that
               would be an awful lot easier to use than all that macho
               hairy stuff with templates and abstract classes and
               what-not. Are there _really_ no simpler ways to
               implement abstract syntax in c++?

               Now if we have memories representing abstract syntax,
               then we have (informally) typed values, one of which is
               the type of memories. And those memories can hold any
               sort of object that could be described by a recursive
               set of abstract syntax equations.

               Now take a look at the type system that MacQueen,
               Plotkin and Sethi describe in "An ideal model for
               recursive polymorphic types" (1983) The ideal model is
               just such a set of recursive equations. Note that they
               define a least-fixedpoint type variable binder, and a
               pair of rules that can be included in a type inference
               algorithm W, with a circular unification algorithm. As
               MacQueen et al. point out, type checking is undecidable
               in general, but this can be used in practice, and the
               denotational semantics handle the possibility, because
               there is the error value W for _dynamic_ type errors. So
               much for mu, the least fixedpoint. There is also the
               type nu, of type environments, which are functions from
               variables to ... well, memory values, I suppose. Like
               the algorithm W would be, implemented meta-circularly:
               a function from lambda expressions to memory values,
               i.e. abstract syntax representing types.

               Now look at the 1982 paper "Principal Typeschemes for
               Functional Programs" by Damas and Milner, and see the
               curious comment they make in the section describing the
               denotational semantics, to the effect that "A free type
               variable is implicitly universally quantified across
               the _whole_ of the expression in which it appears, and
               so it is sufficient to verify just the instantiation of
               type variables by any monotype ... " The whole
               expression in this case includes the "modelled by"
               turnstile, so they seem to be referring to some sort of
               inner model of the type system ... one that could be
               described in terms of memories, perhaps?

               And since untyped lambda expressions can be represented
               by abstract syntax, and since the successor and an
               equality predicate can be implemented in untyped lambda
               calculus, there you have it: operational semantics from
               hot aehr! (This Aristotle's term, meaning
               "information", as far as I can tell.)

               Which brings us to "Proofs and Bloody Types" by Girard
               et al. Perhaps the missing intuition (all of it is
               missing, from that book!) is to be found in this
               "operational denotational semantics" idea. Look perhaps
               at their "denotational" model of system-T expressions
               as untyped lambda expressions implemented as an
               operator algebra and written in the language of ZF set
               theory, then at their reducibility proofs for System F,
               and then at the proofs in MacQueen et al. on the
               contractive/non-expansiveness of the type operators
               when they are under least-fixedpoints: these have an
               eerie familiarity (so much so that it makes me feel bit
               sick to think about it, but I hope that I'll soon be
               able to face opening that book again, and enjoying it
               --- once I have some idea what it's about.)
 *)

local
   open InterpI
   val term0 = (App (Lam ("x", Add (Var "x", Var "x")),
                     Add (Con 10, Con 11)))
in
   val rI = eval term0
end

Representing Data

This is what was really the idea behind Red October a general data representation for any interpreted language.  It includes a section on some potentially interesting applications to cryptography, and an explanation on pages 14-15 as to why I am not yet convinced of any claims that the security of any cryptographic protocol is based on mathematics.
https://drive.google.com/file/d/0B9MgWvi9mywhX0tlbldHSjYzR0NkWGMwaGxPeVlTWVpLdkg0/view?usp=sharing

Tuesday, 13 January 2015

Process Synchronisation by Communication

This is about using inter-process communication to implement process synchronisation primitives which can be used in distributed multi-programming systems: computation "in the cloud" where the particular machines which carry out the steps of a computation are nondeterministically chosen as the computation progresses. Computation distributed in this way is secure, because no one physical system has a complete representation of the state of the computation.
https://drive.google.com/file/d/0B9MgWvi9mywhN01WTHF2RmpTOWtGYlR4VjdQaWhEQlBFWHJN/view?usp=sharing