3 ms·

The semantics of a simple functional language

96 points by matt_d 4y ago

nextos 4y ago
The discussion in the post about dependent types is interesting, e.g.: > [...] 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 http://www.concrete-semantics.org [2] https://raw.githubusercontent.com/blanchette/logical_verification_2020/master/hitchhikers_guide.pdf https://raw.githubusercontent.com/blanchette/logical_verific... [3] http://adam.chlipala.net/frap http://adam.chlipala.net/frap [4] http://adam.chlipala.net/cpdt http://adam.chlipala.net/cpdt [5] https://ilyasergey.net/pnp https://ilyasergey.net/pnp
gergo_barany 4y ago
This started a bit of a competition, some other versions of the same proofs in Agda and Lean are linked from here: https://mastodon.online/@nomeata/110004145921681756 https://mastodon.online/@nomeata/110004145921681756
- deleted 4y ago
  [deleted]
hackandthink 4y ago
I could not write this stuff. It looks simple but it isn't. 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-general/topic/operational.20semantics/ 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#Abstraction https://en.wikipedia.org/wiki/Denotational_semantics#Abstrac...
- Twisol 4y ago
  > My intuition is: evaluating in Lean and embedding the result in the toy language is identical to big step evaluation in the toy language. 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) where "eval _" in Lean becomes "ev x", and "_.embed" becomes "ve _". 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/ExampleSemantics.agda#L285 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.
  - hackandthink 4y ago
    From time to time I'm starting a Theorem prover tutorial, sometimes I even finish. The learning curve is long. 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" )

96 points by matt_d 4y ago

The discussion in the post about dependent types is interesting, e.g.: > [...] 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 http://www.concrete-semantics.org [2] https://raw.githubusercontent.com/blanchette/logical_verification_2020/master/hitchhikers_guide.pdf https://raw.githubusercontent.com/blanchette/logical_verific... [3] http://adam.chlipala.net/frap http://adam.chlipala.net/frap [4] http://adam.chlipala.net/cpdt http://adam.chlipala.net/cpdt [5] https://ilyasergey.net/pnp https://ilyasergey.net/pnp

gergo_barany 4y ago

This started a bit of a competition, some other versions of the same proofs in Agda and Lean are linked from here: https://mastodon.online/@nomeata/110004145921681756 https://mastodon.online/@nomeata/110004145921681756

deleted 4y ago
[deleted]

hackandthink 4y ago

I could not write this stuff. It looks simple but it isn't. 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-general/topic/operational.20semantics/ 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#Abstraction https://en.wikipedia.org/wiki/Denotational_semantics#Abstrac...

Twisol 4y ago
> My intuition is: evaluating in Lean and embedding the result in the toy language is identical to big step evaluation in the toy language. 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) where "eval _" in Lean becomes "ev x", and "_.embed" becomes "ve _". 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/ExampleSemantics.agda#L285 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.
- hackandthink 4y ago
  From time to time I'm starting a Theorem prover tutorial, sometimes I even finish. The learning curve is long. 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" )