Coinductive Big-Step Semantics
36 views
Skip to first unread message
Matt Oliveri
Jan 31, 2016, 3:09:42 AM1/31/16
to Type Theory Study Group
At the end of the meeting yesterday, Danny asked about using a divergence judgment along with big-step "evaluation dynamics". This was called coinductive big-step semantics here:
http://gallium.inria.fr/~xleroy/coindsem/
"Coinductive" because the divergence judgment is defined coinductively. The paper linked to from the link above explains coinductive judgments. It shows a form of type safety that can be proven using coinductive big-step semantics and discusses the pros and cons. (It says other things too.)
Relevant future PFPL chapters for paper:
8: Functions
20: Recursive Types (But this is isorecursive types, while paper uses a cheaty form of equirecursive types.)
21: Untyped lambda-Calculus (for fixed point combinators)
22: Dynamic Typing (Most of the paper uses a dynamically-typed lambda calculus.)
25: Behavioral Typing (The paper's type safety section concerns a Curry-style system, and behavioral typing seems to be the closest thing PFPL discusses.)
I'm not saying you need to understand all those chapters before you can understand the paper though.
People keep (re)inventing styles of operational semantics. I kind of like definitional interpreters, but hardly anyone even mentions them. The "denotational semantics" in section 5 of the paper is really more of an interpreter, and I consider it a form of operational semantics. I have (re)discovered that this sort of definitional interpreter is amenable to direct statements and proofs of type safety.
Another form of big-step semantics that properly distinguishes between unsafe and nonterminating programs is clocked big-step semantics:
https://cakeml.org/popl14.pdf (Section 7)
Basically, add a natural number "clock" to the judgement, which counts down in enough places, and have a fake "timed-out" result if evaluation runs out of time. Nonterminating programs time out no matter how much time you give them.
http://gallium.inria.fr/~xleroy/coindsem/
"Coinductive" because the divergence judgment is defined coinductively. The paper linked to from the link above explains coinductive judgments. It shows a form of type safety that can be proven using coinductive big-step semantics and discusses the pros and cons. (It says other things too.)
Relevant future PFPL chapters for paper:
8: Functions
20: Recursive Types (But this is isorecursive types, while paper uses a cheaty form of equirecursive types.)
21: Untyped lambda-Calculus (for fixed point combinators)
22: Dynamic Typing (Most of the paper uses a dynamically-typed lambda calculus.)
25: Behavioral Typing (The paper's type safety section concerns a Curry-style system, and behavioral typing seems to be the closest thing PFPL discusses.)
I'm not saying you need to understand all those chapters before you can understand the paper though.
People keep (re)inventing styles of operational semantics. I kind of like definitional interpreters, but hardly anyone even mentions them. The "denotational semantics" in section 5 of the paper is really more of an interpreter, and I consider it a form of operational semantics. I have (re)discovered that this sort of definitional interpreter is amenable to direct statements and proofs of type safety.
Another form of big-step semantics that properly distinguishes between unsafe and nonterminating programs is clocked big-step semantics:
https://cakeml.org/popl14.pdf (Section 7)
Basically, add a natural number "clock" to the judgement, which counts down in enough places, and have a fake "timed-out" result if evaluation runs out of time. Nonterminating programs time out no matter how much time you give them.
Cyrus Omar
Jan 31, 2016, 12:22:04 PM1/31/16
to Matt Oliveri, Type Theory Study Group
Thanks for the references! Another recent paper along those lines is this one, which has an interesting "proof-depth-indexed" approach that allows you to use induction to prove a form of type safety: http://dl.acm.org/citation.cfm?doid=2635631.2635846.
--
You received this message because you are subscribed to the Google Groups "Type Theory Study Group" group.
To unsubscribe from this group and stop receiving emails from it, send an email to type-theory-study...@googlegroups.com.
To post to this group, send email to type-theory...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/type-theory-study-group/a53320cb-8a74-4d46-829c-fbe6cf8dd48d%40googlegroups.com.
For more options, visit https://groups.google.com/d/optout.
Matt Oliveri
Jan 31, 2016, 6:29:30 PM1/31/16
to Type Theory Study Group
(Here is a non-paywall copy: ftp://ftp.disi.unige.it/person/AnconaD/Ancona-FTfJP14.pdf)
I see. So it fixes the problem with coevaluation by having infinite values.
Their finite approximation of the coevaluation relation makes it similar to clocked big-step, with the approximation index corresponding to the clock.
I personally prefer a "timed-out" or "bottom" result to infinite values, which are just as fake, and much more complicated.
I see. So it fixes the problem with coevaluation by having infinite values.
Their finite approximation of the coevaluation relation makes it similar to clocked big-step, with the approximation index corresponding to the clock.
I personally prefer a "timed-out" or "bottom" result to infinite values, which are just as fake, and much more complicated.
Reply all
Reply to author
Forward
0 new messages