Atom Feed

Associated Blogs
 
Edge City
 
Orcmid's Lair
 
Praxis101
 
Prof. von Clueless in the Blunder Dome

Recent Items
 
Stepping Off the Edge
 
BlunderDome Disruption
 
Miser Hacks I: Floating Along the Ground
 
Preparing for FLoC 2006
 
Preparing for the Lang.NET Symposium
 
Logic, Language, Information and Computation
 
Logic Summer, Model Autumn: 2006 Season of Functional Programming
 
Moving Peano Ahead for OOPSLA
 
Searching for the Semantic Web
 
Metadata for the desktop

Archives
2004-05-30
2004-06-06
2004-06-13
2004-06-27
2004-08-22
2004-08-29
2004-10-03
2004-12-05
2005-01-23
2005-06-19
2005-08-14
2005-10-09
2006-01-01
2006-02-05
2006-02-12
2006-07-09
2006-07-16
2006-07-30
2006-08-06
2006-08-20
2006-10-08
2006-10-22

Stepping Off the Edge

This is the final post that will be made to Numbering Peano at the location http://nfocentrale.net/miser/astraendo/pn.  That also applies to the site feed from that location.

From now on, all posts will appear at the official Numbering Peano URL, at the location http://miser-theory.info/astraendo/pn.  The official site feed is also the one that is assured to work from now on.

You will know that you are at the old blog location if you see no post more recent than this, neither on the web page nor in the site feed.

PS: Sometime in the next few weeks, the old URLs will be moved atop the new, official ones and either set of URLs will work just fine.  For a while.  But the official ones will always work.

BlunderDome Disruption

I’ve been engaged in some serious web site reorganization over the past week.  Today, the movers are coming to the Miser Project and Numbering Peano. 

{tags: orcmid A2 Hosting nfoCentrale  web hosting Apache system incoherence confirmable experience}

What this means for readers of this blog is that the best reception will be found at URLs like http://miser-theory.info/astraendo/pn  and not http://nfocentrale.net/miser/astraendo/pn.  In fact, the second URL and the site feed at that same location will be not see any more blog updates for several weeks.

The Numbering Peano blog and feed at http://miser-theory/info/astraendo/pn  will see little or no interruption.  There may be some temporary breakage until the construction crew can straighten things out.  

To know more about what is happening and why, there is an account on my little-known blog, Spanner Wingnut’s Muddleware Lab.

Miser Hacks I: Floating Along the Ground

While chatting with Andrew Appel in the early days of the 2006 Federated Logic Conference, I explained a little about the way I simplify Lisp’s fundamental data model for my miniature system, Miser.  Appel suggested that, especially with immutability and no cycles, Miser should be very amenable to inductive proofs and related simplicities.  But Andrew also thought that the way I made the primitive functions closed and total would turn out to be an ugly hack.  Appel’s intuition is that the hack will make reasoning and proofs unnecessarily difficult.  I see how that might be, although I remain attached to the hack until I can confirm the trade-off more closely.

I think the basic hack, to have the three primitive operations corresponding to those of Lisp be total, holds up.  But there are other ways in which I will have to be very careful.  Here’s the part that I think is safe enough.

The Miser Obs

oMiser, the pure, entry-level computational model for the Miser Project, uses a pure Lisp-like storage model and an untyped system.  There is a single ground type (Ob, where in pure Lisp it is SEXPR) and the system is closed over that type—operations on elements determine elements only of that type and are defined only on elements of that type.  

The computational model has unstratified control: any data structure is also program and vice versa.  These qualities are fundamental to Miser.  The implementation is as close to a theoretical model of universal computation as we can get, allowing us to explore and comprehend the opportunities and limitations of such models in concrete, demonstrable terms. 

The basic data model involves the following functions, illustrated in the oMiser logo.

ob.c(x, y) corresponds to Lisp’s cons[x;y] and the result is the ordered pair that has x as its a-path and y as its b-path.  (I refer to the components of ordered pairs as the a-path and b-path to emphasize that access is best thought of as navigation—movement of attention—not construction and destruction.)

ob.a(z) corresponds to Lisp’s car[z].  The choice of which of ob.a and ob.b are thought to be the first or second or left or right or other aspect of ordering is arbitrary.  It is only necessary that we be consistent with whatever view is chosen.  We will see, later on, that introduction of an asymmetry will predispose our choice of idioms for the natural representation of lists and other structures.  Operationally, the implementation of ob.b is not allowed to be slower than that for ob.a.

ob.b(z) corresponds to Lisp’s cdr[z] and basically selects the component of z that is generally not the one ob.a determines (unless they happen to be the same).

If z = ob.c(x, y), then ob.a(z) = x and ob.b(z) = y, where “=” is equality in the system.  This “=” corresponding to Lisp’s equal[x;y].

The First Hack

The first Miser hack is related to the differentiation between ordered pairs and individuals (the Miser counterparts of Lisp atoms and set-theoretic ur-Elements).  Individuals are not themselves ordered pairs and must in some way be simply taken as given.

In Lisp, there are elements, m, for which it cannot be shown that there are x and y such that m = cons[x, y].  The Lisp atoms have this quality: it is inadmissible to suppose car[m] or cdr[m] in the case atom[m].  That is, car and cdr are undefined on atoms. 

It has been my thinking that having ob.a and ob.b be total (defined for all elements) enriches the availability of programming idioms and simplifies implementations by avoiding exception checks.  I was inspired by those practical considerations and the useful fact that there are never, ever cyclic structures in Miser Obs. 

So I make ob.a and ob.b total: ob.a(x) and ob.b(x) are each defined on all elements x. 

The Miser individual is the counterpart of the Lisp atom (in Lisp, satisfying atom[x]).  For every Miser individual, x, ob.a(x) = ob.b(x) = x.  Furthermore, ob.c(ob.a(z),ob.b(z)) is never z when is-individual(z), but it is always z when z is some ob.c(x, y).

The only difference in this case is that instead of requiring some oracle to determine atom[x], we have a structural feature of the system of elements that allows individuals to be distinguished by inspection (which is to say that “=” has all of the oracular power that we require).

Furthermore, needing to qualify certain theorems/axioms by whether or not there are individuals involved is no more difficult, I claim, than the current situation with Lisp when certain functions are undefined for atoms.

Justifying the Hack

As for Lisp, the equality of Miser objects is definable as a structural identity that preserves the equality-by-parts that is fundamental to the nature of ordered pairs: if the corresponding parts of two ordered pairs are the same, the pairs are equal and the pairs are different otherwise. 

In both Lisp and Miser, equality-by-parts applies only for constructions (that is, elements z that are asserted to be determined by cons[x;y] or ob.c(x, y)).  That is sufficient.

If you look at a procedure for implementation of Lisp equal[x;y] or the Miser x=y, the occurrence of atoms (or individuals) is separated out and some different implementation-specific oracle is used to determine whether atoms (individuals) are the same or not. 

The Lisp hack involves reliance on use of atom[x] and eq[x; y] for atoms x and y.  With Miser the means for differentiating individuals is not visible, but one can always determine computationally when a Miser individual is in hand by virtue of ob.a(x) = x being satisfied.  (The choice of ob.a is related to the second hack, visible in the diagram above but not yet addressed in this discussion.)

I claim that either approach is equally tractable (or equally intractable if you prefer).  Atoms (individuals) are distinguishable from ordered pairs, and the principles for inference of characteristics of pairs are essentially the same.

I realize that there is the odd case where one cannot make deductions about x and y based on ob.a(x) = ob.a(y) without determining whether both are individuals or not.  This is not a new problem.  With the Lisp model, one must avoid applying deductions that are valid when z is a cons[x;y] and not when atom[z].  The guards that must be incorporated in deductions and in identities are essentially the same.

Going Too Far?

If I had stopped here, I think there is no problem and I would be confident that I need not be too concerned about Appel’s objection.  I would certainly keep his warning in mind and be on the lookout for difficulties when I have more practice at reasoning about Miser and its programs. 

But I didn’t stop here, and I will take up the next hack in a separate note.

Preparing for FLoC 2006

FLoC Begins.  Tomorrow, August 11, is the first day of my attendance at the 2006 Federated Logic Conference.  I will be attending the workshop on Proof Carrying Code (PCC).  I’ll also be collecting all of my tickets and proceedings for the tracks and workshops I’m registered for. There are several places where I want to be in three places at once.  Most of the time, I’ll go to a session that I don’t have any proceedings paper for.  But I expect to adjust as I go through the marathon 9 days that I’ll be attending.

At lang.NET 2006 I managed to connect to the wonderfully-fast wired LAN in Microsoft Building 20.  I also managed to mess up my wireless connection for home use—my Tablet PC can no longer see or be seen by my workgroup computers—and I haven’t resolved that yet.  But the wired LAN connection works great at home, with everything visible the way it is supposed to be.  I am content for now to reserve wireless operation for on-the-road use, such as in the WIFI area of the FLoC venue.

Every time I have an outside event to attend, I do a little more to make Quadro, my Tablet PC, ready for travel.  Beside bringing over a lot of electronic documents on conference-related topics, I now have blogging software running on Quadro.  I may actually manage to “live blog” from the venue.  This initial post is confirmation that I have BlogJet working and connected properly.  (I also see that use of “BlogJet” in the text causes a link to be created automatically.  How cute.)

Preparing for the Lang.NET Symposium

Lang.NET Symposium Agenda.  The agenda for lang.NET is available and I am using this delightful Sunday afternoon to prepare for three days in Redmond.  The first project is working out the bus routes and schedules between West Seattle and the Microsoft Campus.  Then I’ll prepare Quadro, my Tablet PC, with materials I wish I had already dug into but I just might while there.  This is a bit like filling my luggage with books to read and then bringing them home still unread after a short vacation.  I need to move some of my functional-programming and computation-theory materials to Quadro anyhow, so the housekeeping will be good for me.  And I do like reading while commuting by bus.

{tags: lang.NET 2006 .NET CLR .NET Languages Mono ECMA CLI IronPython Scheme F# Spec# Second Life orcmid}

My main interest is the content for the three days, although it will be interesting to actually see the Microsoft Store.  Being in Building 20, the home of Port25, will also be interesting.  It is also remarkable that this event was scheduled to take advantage of people already traveling to be at OSCON last week.

And then there’s the content.  Before there was an agenda, I was intrigued by organizer Erik Meijer’s involvement and his background with Haskell.  I’ve always wanted to understand Haskell’s treatment of imperative and interactive activity.  My toy miniature functional system, oMiser, is purely mathematical and one challenge is to see how to embrace interaction and imperative (stateful) activity while somehow preserving the amenability of as much of the "pure" elements to mathematical rigor as possible.  I keep thinking it is about McCarthy-Painter semantics and I keep wondering if that is enough, along with a way to tell pure operations from ones that aren’t or that aren’t determined to be. 

It is a desire to become more immersed in these topics that had me install F# recently, download the latest Mono bits, make sure I have the ECMA C# and CLI specifications, and be looking forward to the following sessions:

• Anders Helsjberg (Microsoft) on LINQ and C# 3.0
  but mainly because I like how Anders talks, share his love for ALGOL 60, and, heh, he doesn’t have a blog that I can find
    
•  Jim Hugunin (Microsoft) on IronPython and dynamically typed languages on the Common Language Runtime (CLR)
    
• C21.1: Versioning in the TwentyFirst Century
  because I’m curious and some cures for DLL hell seem to be worse than the disease, if that’s possible
    
• William Cook (U. Texas at Austin) on AppleScript and the Effect of Latency on Programming Languages
   
• Mike Barnett (Microsoft) on Spec# and Why Every Language Should (Will) Have Contracts
    
• Gilad Bracha (Sun Microsystems) on Dynamically Typed Languages on the Java Platform
    
• Gary William Flake (Microsoft) on the Internet Singularity (and Microsoft Live Labs)
    
• Shriram Krishnamurthi (Brown Univesity) on Interactive Web Applications (and PLT Scheme)
  and how many different ways his name is misspelled everywhere
    
• Miguel de Icaza (Novell) on Mono
    
• Second Life (and maybe how they will stop forcing downloads on us devoted non-admin users)
    
• Don Syme (Microsoft) on F# and HOT Languages on the CLR
    
• Phoenix (to find out if they really can do all of that starting from compiled code)

There’s more, including Open Spaces sessions, but I’m already running on overdose.

If I blog about any of these sessions and other activities, I will doubtless split my posts between Numbering Peano and Professor von Clueless, depending on which way I tilt during the session.

[update 2006–08–03: I changed the tag to agree with the one requested at the symposium.  I also got tremendous value from the symposium along with meeting many interesting people.  Even so, I missed Harry Pierson being in the room on Monday.]

Logic, Language, Information and Computation

The WoLLIC 2006 workshop started today.  This is not the week for me to be away, although I find the program to be challenging and of interest. 

Two of the WoLLIC tutorials and associated presentations span my interests, with a few other presentations fitting in the middle somewhere.

• Solomon Feferman’s development of an Operational Theory of Sets intrigues me because I don’t understand it.  I also don’t understand Feferman’s chapter D.4 in the Handbook of Mathematical Logic.  The definition of Cartesian closed universes with a function space that includes basic combinators suggests to me that this should have some bearing on computation but I haven’t puzzled it out.  I thought maybe listening to Feferman would perhaps get me through whatever barrier (i.e., my own ignorance and, oh yes, laziness) that I must traverse in order to be able to make use of this work.   A number of Feferman’s papers are available on-line.  The opportunity is to add some accessible-to-me selection to my summer reading.
    
• Yuri Gurevich’s thesis about Expanding Notions of Algorithms is relevant to our understanding of the Church-Turing Thesis and limits of computation as effective procedures.  Gurevich suggests that considering algorithms over higher abstractions may take us out of the tar pit.  Others have also suggested that interactive systems may take us beyond Church-Turing.  I don’t know enough to understand in what way there is a break-out, and would love to hear more. I’ve only seen glancing references to the work on AsmL at Microsoft.  Gurevich has an extensive annotated list of articles.  He provides an useful abstract and reading list for WoLLIC.  This is definitely the basis for further summer reading.

These were the main attractors for me.  Other workshop topics provided tangential interest, but learning more might lead to recalibration about those subjects.   This was not enough to justify the trip, especially in the face of competing events here at home.

It’s heartening to know that there is extensive publicly-available material around the themes of both Solomon Feferman and Yuri Gurevich.

Logic Summer, Model Autumn: 2006 Season of Functional Programming

For reasons that are not entirely clear to me, the Pacific Coast is the beneficiary of some major conferences that relate to logic and computation, with varying relationships to functional programming and perspectives on computational abstractions:

• WoLLIC 2006, July 18-21 at Stanford University, Stanford, California.  Workshop on Logic, Language, Information and Computation
    
• 2006 Lang.NET Symposium, July 31 – August 2 (new dates) at Microsoft, Redmond, Washington.
     
• FLoC 2006, August 10–22, Seattle, Washington.  The 2006 Federated Logic Conference, marking the Gödel Centenary.  Including, under one tent:
• August 12–15, three parallel conferences:
  LICS: IEEE Symposium on Logic in Computer Science
  RTA: Conference on Rewriting Techniques and Applications (August 12–14)
  SAT: International Conference on Theory and Applications of Satisfiability Testing
• August 17–20, three parallel conferences:
  CAV: Conference on Computer Aided Verification
  ICLP: International Conference on Logic Programming
  IJCAR: International Joint Conference on Automated Reasoning
• Plus one and two-day workshops preceding, between, and following the blocks of parallel conferences
      
• ICFP 2006: September 16–21, Portland, Oregon. International Conference on Functional Programming, with several workshops at the front and on the rear of the September 18–20 conference days.
      
• PLOP 2006: October 21–23, Portland, Oregon.  Pattern Languages of Programming Design 2006.
      
• OOPSLA 2006: October 22–26, Portland, Oregon.  ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications.

And if you want a break between ICFP and PLOP-OOPSLA in the Pacific Northwest, one might consider

• MoDELS 2006: October 1–6, Genova, Italy.  ACM/IEEE 9th International Conference on Model Driven Engineering Languages and Systems. Formerly the UML series of conferences.