railroad diagrams so underrated
Conversation
How about Oberon? :O
3
Also, can somebody come up with 'railroad diagrams' for inference rules?
1
3
2
how do they look?
1
1
2
The idea is that you each inference rule is kind of a 'branch node' and the axioms are 'leaf nodes' and you slot them together to build a proof tree.
2
1
oh yes! these look very diagrammable!
1
1
Yeah I reckon so! I think the big issue I have with them though is scaling them to full language specs - the current inference rule notation works for small stuff, but can get unmanageable quickly.
1
1
I was thinking it would be neat to have some text notation to define the rules, and then a way of presenting them that implementors can use - perhaps with a way of switching between a diagram version, generated 'prose', and more traditional maths notation.
1
1
With clickable links to jump to definitions and usages, ways of grouping based on judgement vs syntactic construct, and an index of rules, judgements and syntax.