Grmph. So that's why it wouldn't compile...
I've been learning Twelf. It has the steepest learning curve of any language I've ever approached, and that includes Objective Caml. OMG, Twelf is weird.
It is, however, very cool.
As a learning project, I started with the introduction, then the tutorials, and (dispensing with the User Manual, which is out of date), moved on to trying to write a signature to prove various things about the unsorted polyadic π-calculus. I spent a long damned time trying to make a totality assertion about structural process congruence. Weeks. Adding up to more than two months, I think. Embarrassing.
I was getting very discouraged with my progress, until I cracked open Milner's book... and there, on page 91, I saw the following words:
Exercise 9.14 (for logicians) Prove that if neither P nor Q contains replication, the it is decidable if P ≡ Q.
Exercise 9.15 (for experienced logicians) Is P ≡ Q decidable in general?
I think I'm an "experienced logician" now.
The answer to 9.15 is no, sadly, and I suspect this is why various adaptions to the π-calculus have appeared that feature limits on replication. It makes structural congruence undecidable in general, so researchers have come up with alternatives and then shown that the full π-calculus can be encoded in them.
I can roll with that. It just so happens I have an alternative in my pocket that I used in the OCaml NAE Cf_gadget module. I'll report back later on whether I can get decidable structural process congruence out of it.
p.s. I think I've mostly figured out how to write Twelf code now.
Update: okay, I'm beginning to think that proving a totality assertion on the transitivity of structural congruence is just not going to work. As soon as I add replication to any kind of variant I've tried, the coverage checker explodes. Every time I add a lemma to plug a case, the coverage checker ends up giving me an even larger list of missed cases. I suppose this makes intuitive sense— when you add replication to the calculus, you introduce the possibility that reaction can increase the structure rather than reduce it.
So. I'm going to give up on the symmetry of structural congruence. I'm moving on. I'll just assert totality on the transitivity of reduction, then proceed to transitivity of reaction. It now makes intuitive sense to me that symmetry would collapse on me at this point. Progress!
My Groups
-
Writers Hub Updated: Yesterday
-
Amnesty International Updated: Yesterday
Neighborhood
Explore friends, family, friends & family, or entire neighborhood.
