Skip to main content
Commonmark migration
Source Link

No, you cannot strictly distinguish syntactic from semantic methods, but the distinction still ends up making sense.

  • Structural operational semantics is not denotational, because it is not a compositional method of giving semantics to a programming language.

  • However, you can build denotational models out of a structural operational semantics by using a realizability or logical relations method. As an example, see Robert Harper's Constructing Type Systems over Operational Semantics.

  • Term models are denotational, but generally semanticists are not satisfied with them. What they usually want is a category of models in which the term model is initial, which can be used to prove soundness and completeness results. (The soundness and completeness of the typed lambda calculus for cartesian closed categories is the paradigmatic example; see Alex Simpson's Categorical Completeness Results for the Simply-Typed $\lambda$-calculus for some details.)

  • In the other direction, if you have a denotational semantics, you might want to figure out what the syntax for it is. Then you want to go and find a syntax and abstract machine whose term model can serve as an intitial object in a suitable category of models.

    For instance, game semantics began its life as a purely semantic construction, and eventually led to work on operational game semantics --- a recent example of which is Alexis Goyet's The lambda lambda-bar calculus: A dual calculus for unconstrained strategies.

For instance, game semantics began its life as a purely semantic construction, and eventually led to work on operational game semantics --- a recent example of which is Alexis Goyet's The lambda lambda-bar calculus: A dual calculus for unconstrained strategies.

  • Overall, you can think of structural operational semantics as a way of specifying abstract machines, which we hope are easy to implement. A denotational semantics gives a compositional model of a language, which we hope is easy to reason about. If we have both, then we can both implement and reason about the language.

  • Normalization theorems are an interesting ambiguous case. Usually, to prove normalization, you need a semantic model (typically a logical relation). However, once you know that normalization holds, many properties can now be proved by induction on normal forms, which is a purely syntactic argument.

    For weak logics (anything up to first-order logic without induction, roughly), you can prove normalization syntactically, using the technique of hereditary substitution. In these logics, the subformula property holds, and so you can prove normalization by induction on types. See Frank Pfenning's paper Structural Cut Elimination for an explanation of how this works.

For weak logics (anything up to first-order logic without induction, roughly), you can prove normalization syntactically, using the technique of hereditary substitution. In these logics, the subformula property holds, and so you can prove normalization by induction on types. See Frank Pfenning's paper Structural Cut Elimination for an explanation of how this works.

No, you cannot strictly distinguish syntactic from semantic methods, but the distinction still ends up making sense.

  • Structural operational semantics is not denotational, because it is not a compositional method of giving semantics to a programming language.

  • However, you can build denotational models out of a structural operational semantics by using a realizability or logical relations method. As an example, see Robert Harper's Constructing Type Systems over Operational Semantics.

  • Term models are denotational, but generally semanticists are not satisfied with them. What they usually want is a category of models in which the term model is initial, which can be used to prove soundness and completeness results. (The soundness and completeness of the typed lambda calculus for cartesian closed categories is the paradigmatic example; see Alex Simpson's Categorical Completeness Results for the Simply-Typed $\lambda$-calculus for some details.)

  • In the other direction, if you have a denotational semantics, you might want to figure out what the syntax for it is. Then you want to go and find a syntax and abstract machine whose term model can serve as an intitial object in a suitable category of models.

For instance, game semantics began its life as a purely semantic construction, and eventually led to work on operational game semantics --- a recent example of which is Alexis Goyet's The lambda lambda-bar calculus: A dual calculus for unconstrained strategies.

  • Overall, you can think of structural operational semantics as a way of specifying abstract machines, which we hope are easy to implement. A denotational semantics gives a compositional model of a language, which we hope is easy to reason about. If we have both, then we can both implement and reason about the language.

  • Normalization theorems are an interesting ambiguous case. Usually, to prove normalization, you need a semantic model (typically a logical relation). However, once you know that normalization holds, many properties can now be proved by induction on normal forms, which is a purely syntactic argument.

For weak logics (anything up to first-order logic without induction, roughly), you can prove normalization syntactically, using the technique of hereditary substitution. In these logics, the subformula property holds, and so you can prove normalization by induction on types. See Frank Pfenning's paper Structural Cut Elimination for an explanation of how this works.

No, you cannot strictly distinguish syntactic from semantic methods, but the distinction still ends up making sense.

  • Structural operational semantics is not denotational, because it is not a compositional method of giving semantics to a programming language.

  • However, you can build denotational models out of a structural operational semantics by using a realizability or logical relations method. As an example, see Robert Harper's Constructing Type Systems over Operational Semantics.

  • Term models are denotational, but generally semanticists are not satisfied with them. What they usually want is a category of models in which the term model is initial, which can be used to prove soundness and completeness results. (The soundness and completeness of the typed lambda calculus for cartesian closed categories is the paradigmatic example; see Alex Simpson's Categorical Completeness Results for the Simply-Typed $\lambda$-calculus for some details.)

  • In the other direction, if you have a denotational semantics, you might want to figure out what the syntax for it is. Then you want to go and find a syntax and abstract machine whose term model can serve as an intitial object in a suitable category of models.

    For instance, game semantics began its life as a purely semantic construction, and eventually led to work on operational game semantics --- a recent example of which is Alexis Goyet's The lambda lambda-bar calculus: A dual calculus for unconstrained strategies.

  • Overall, you can think of structural operational semantics as a way of specifying abstract machines, which we hope are easy to implement. A denotational semantics gives a compositional model of a language, which we hope is easy to reason about. If we have both, then we can both implement and reason about the language.

  • Normalization theorems are an interesting ambiguous case. Usually, to prove normalization, you need a semantic model (typically a logical relation). However, once you know that normalization holds, many properties can now be proved by induction on normal forms, which is a purely syntactic argument.

    For weak logics (anything up to first-order logic without induction, roughly), you can prove normalization syntactically, using the technique of hereditary substitution. In these logics, the subformula property holds, and so you can prove normalization by induction on types. See Frank Pfenning's paper Structural Cut Elimination for an explanation of how this works.

added 4 characters in body
Source Link
Neel Krishnaswami
  • 32.9k
  • 1
  • 104
  • 165

No, you cannot strictly distinguish syntactic from semantic methods, but the distinction still ends up making sense.

  • Structural operational semantics is not semanticdenotational, because it is not a compositional method of giving semantics to a programming language.

  • However, you can build denotational models out of a structural operational semantics by using a realizability or logical relations method. As an example, see Robert Harper's Constructing Type Systems over Operational Semantics.

  • Term models are denotational, but generally semanticists are not satisfied with them. What they usually want is a category of models in which the term model is initial, which can be used to prove soundness and completeness results. (The soundness and completeness of the typed lambda calculus for cartesian closed categories is the paradigmatic example; see Alex Simpson's Categorical Completeness Results for the Simply-Typed $\lambda$-calculus for some details.)

  • In the other direction, if you have a denotational semantics, you might want to figure out what the syntax for it is. Then you want to go and find a syntax and abstract machine whose term model can serve as an intitial object in a suitable category of models.

For instance, game semantics began its life as a purely semantic construction, and eventually led to work on operational game semantics --- a recent example of which is Alexis Goyet's The lambda lambda-bar calculus: A dual calculus for unconstrained strategies.

  • Overall, you can think of structural operational semantics as a way of specifying abstract machines, which we hope are easy to implement. A denotational semantics gives a compositional model of a language, which we hope is easy to reason about. If we have both, then we can both implement and reason about the language.

  • Normalization theorems are an interesting ambiguous case. Usually, to prove normalization, you need a semantic model (typically a logical relation). However, once you know that normalization holds, many properties can now be proved by induction on normal forms, which is a purely syntactic argument.

For weak logics (anything up to first-order logic without induction, roughly), you can prove normalization syntactically, using the technique of hereditary substitution. In these logics, the subformula property holds, and so you can prove normalization by induction on types. See Frank Pfenning's paper Structural Cut Elimination for an explanation of how this works.

No, you cannot strictly distinguish syntactic from semantic methods, but the distinction still ends up making sense.

  • Structural operational semantics is not semantic, because it is not a compositional method of giving semantics to a programming language.

  • However, you can build denotational models out of a structural operational semantics by using a realizability or logical relations method. As an example, see Robert Harper's Constructing Type Systems over Operational Semantics.

  • Term models are denotational, but generally semanticists are not satisfied with them. What they usually want is a category of models in which the term model is initial, which can be used to prove soundness and completeness results. (The soundness and completeness of the typed lambda calculus for cartesian closed categories is the paradigmatic example; see Alex Simpson's Categorical Completeness Results for the Simply-Typed $\lambda$-calculus for some details.)

  • In the other direction, if you have a denotational semantics, you might want to figure out what the syntax for it is. Then you want to go and find a syntax and abstract machine whose term model can serve as an intitial object in a suitable category of models.

For instance, game semantics began its life as a purely semantic construction, and eventually led to work on operational game semantics --- a recent example of which is Alexis Goyet's The lambda lambda-bar calculus: A dual calculus for unconstrained strategies.

  • Overall, you can think of structural operational semantics as a way of specifying abstract machines, which we hope are easy to implement. A denotational semantics gives a compositional model of a language, which we hope is easy to reason about. If we have both, then we can both implement and reason about the language.

  • Normalization theorems are an interesting ambiguous case. Usually, to prove normalization, you need a semantic model (typically a logical relation). However, once you know that normalization holds, many properties can now be proved by induction on normal forms, which is a purely syntactic argument.

For weak logics (anything up to first-order logic without induction, roughly), you can prove normalization syntactically, using the technique of hereditary substitution. In these logics, the subformula property holds, and so you can prove normalization by induction on types. See Frank Pfenning's paper Structural Cut Elimination for an explanation of how this works.

No, you cannot strictly distinguish syntactic from semantic methods, but the distinction still ends up making sense.

  • Structural operational semantics is not denotational, because it is not a compositional method of giving semantics to a programming language.

  • However, you can build denotational models out of a structural operational semantics by using a realizability or logical relations method. As an example, see Robert Harper's Constructing Type Systems over Operational Semantics.

  • Term models are denotational, but generally semanticists are not satisfied with them. What they usually want is a category of models in which the term model is initial, which can be used to prove soundness and completeness results. (The soundness and completeness of the typed lambda calculus for cartesian closed categories is the paradigmatic example; see Alex Simpson's Categorical Completeness Results for the Simply-Typed $\lambda$-calculus for some details.)

  • In the other direction, if you have a denotational semantics, you might want to figure out what the syntax for it is. Then you want to go and find a syntax and abstract machine whose term model can serve as an intitial object in a suitable category of models.

For instance, game semantics began its life as a purely semantic construction, and eventually led to work on operational game semantics --- a recent example of which is Alexis Goyet's The lambda lambda-bar calculus: A dual calculus for unconstrained strategies.

  • Overall, you can think of structural operational semantics as a way of specifying abstract machines, which we hope are easy to implement. A denotational semantics gives a compositional model of a language, which we hope is easy to reason about. If we have both, then we can both implement and reason about the language.

  • Normalization theorems are an interesting ambiguous case. Usually, to prove normalization, you need a semantic model (typically a logical relation). However, once you know that normalization holds, many properties can now be proved by induction on normal forms, which is a purely syntactic argument.

For weak logics (anything up to first-order logic without induction, roughly), you can prove normalization syntactically, using the technique of hereditary substitution. In these logics, the subformula property holds, and so you can prove normalization by induction on types. See Frank Pfenning's paper Structural Cut Elimination for an explanation of how this works.

Source Link
Neel Krishnaswami
  • 32.9k
  • 1
  • 104
  • 165

No, you cannot strictly distinguish syntactic from semantic methods, but the distinction still ends up making sense.

  • Structural operational semantics is not semantic, because it is not a compositional method of giving semantics to a programming language.

  • However, you can build denotational models out of a structural operational semantics by using a realizability or logical relations method. As an example, see Robert Harper's Constructing Type Systems over Operational Semantics.

  • Term models are denotational, but generally semanticists are not satisfied with them. What they usually want is a category of models in which the term model is initial, which can be used to prove soundness and completeness results. (The soundness and completeness of the typed lambda calculus for cartesian closed categories is the paradigmatic example; see Alex Simpson's Categorical Completeness Results for the Simply-Typed $\lambda$-calculus for some details.)

  • In the other direction, if you have a denotational semantics, you might want to figure out what the syntax for it is. Then you want to go and find a syntax and abstract machine whose term model can serve as an intitial object in a suitable category of models.

For instance, game semantics began its life as a purely semantic construction, and eventually led to work on operational game semantics --- a recent example of which is Alexis Goyet's The lambda lambda-bar calculus: A dual calculus for unconstrained strategies.

  • Overall, you can think of structural operational semantics as a way of specifying abstract machines, which we hope are easy to implement. A denotational semantics gives a compositional model of a language, which we hope is easy to reason about. If we have both, then we can both implement and reason about the language.

  • Normalization theorems are an interesting ambiguous case. Usually, to prove normalization, you need a semantic model (typically a logical relation). However, once you know that normalization holds, many properties can now be proved by induction on normal forms, which is a purely syntactic argument.

For weak logics (anything up to first-order logic without induction, roughly), you can prove normalization syntactically, using the technique of hereditary substitution. In these logics, the subformula property holds, and so you can prove normalization by induction on types. See Frank Pfenning's paper Structural Cut Elimination for an explanation of how this works.