The semantics of a simple functional language
lawrencecpaulson.github.io
lawrencecpaulson.github.io
> [...] I'm curious, who has promoted the myth that you need dependent types to do semantics
My experience is that teaching materials for Coq are much more developed in the context of semantics and software verification, despite Coq being harder to use.
The post mentions Concrete Semantics [1], which is a really nice Isabelle book. There's also a Lean version [2]. However, to my best knowledge, there's no intermediate/advanced teaching material such as [3-5] for Isabelle, Lean, or Agda. Just introductory stuff.
[1] http://www.concrete-semantics.org
[2] https://raw.githubusercontent.com/blanchette/logical_verific...
[3] http://adam.chlipala.net/frap
I played with Sebastian Ulrich's Lean 4 Port of Conor Mc Bride's Agda Code.
( bottom of https://leanprover.zulipchat.com/#narrow/stream/113488-gener... ) ( View in Playground (right top corner))
I got stuck here:
/-- Operational and denotational semantics coincide. -/
theorem eval_eval : x ~>* (eval x).embed := by
My intuition is: evaluating in Lean and embedding the result in the toy language is identical to big step evaluation in the toy language.
But I can't parse the theorem.
https://en.wikipedia.org/wiki/Denotational_semantics#Abstrac...
Yes, I think that's right.
> But I can't parse the theorem.
I think there's a bit of a divide between languages with tactic-based proofs and languages without tactics, and it looks like both Lean and Isabelle use tactics.
I've gotten very comfortable with Agda over the past year. Agda doesn't have a real tactics metalanguage; but I honestly prefer working with proof terms, since it's easier (I feel) to write comprehensible proofs. While tactics make for very compact proofs, I think giving a proof some space to breathe is a good thing -- I'm interested in why it's true, not only that it's true.
I think the analogous theorem in Conor McBride's Agda version of this development is here [1]:
ev=>* : {t : Ty} (x : Exp t)
-> x =>* ve (ev x)
The theorem body is heavily commented (nice!), and each case is handled explicitly and in full. While the development is probably a little bit longer than in Lean or Isabelle, I find it easier to approach.
[1] https://github.com/pigworker/Samizdat/blob/main/ExampleSeman...
> I could not write this stuff. It looks simple but it isn't.
True that. I bounced a number of times off of proof assistants before it stuck. Like I said, I feel very comfortable with Agda now; but I won't claim this is easy.
Thanks, I looked at the Agda version. It is more explicit and well documented.
And I agree: tactics are another thing to learn and can be very arcane.
But in this discussion everybody admires Isabelle/Hol's automation: "I'm envious of the degree of automation that Isabelle affords".
---
My problem with "theorem eval_eval : x ~>* (eval x).embed" was very basic.
I got confused by the infix definition of "~>*".
Viewing the type in the playground as "∀ {a : Ty} {x : Exp a}, RTC Eval x (Val.embed a (eval x))" helped.
---
I am just dabbling around but I will try Lean 4. It seems to work well though it is not officially released.
And Lean 4 seems to be a very fast funcional programming language.
(I actually finished an Agda Tutorial a few years ago, it's focus is on programming. Lean somehow succeeded to "fix" or "hack around" this annoying intensional equality:
"Lean's standard library defines an additional axiom, propositional extensionality, and a quotient construction which in turn implies the principle of function extensionality"
)
Aaah, I'm sorry -- I thought you meant the theorem body -- the proof itself -- was hard to parse. (Which it also is!)
Yes, custom infix operators are just one of many novelties you can find in these languages. I think Haskell is the only "mainstream" (hah) language I'm familiar with that has anywhere close to the same degree of syntax customization.
All these things together really do make for a steep learning curve...