# Translations of intuitionistic logic

m (→Call-by-value Girard's translation A\imp B \mapsto \oc{(A\limp B)}: typos) |
m (→Call-by-value translation A\imp B \mapsto \oc{(A\limp B)}: T L rule) |
||

Line 444: | Line 444: | ||

\LabelRule{\oc R} |
\LabelRule{\oc R} |
||

\UnaRule{{}\vdash \oc{\one}} |
\UnaRule{{}\vdash \oc{\one}} |
||

+ | \DisplayProof |
||

+ | </math> |
||

+ | |||

+ | <br /> |
||

+ | |||

+ | <math> |
||

+ | \AxRule{\Gamma\vdash C} |
||

+ | \LabelRule{T L} |
||

+ | \UnaRule{\Gamma,T\vdash C} |
||

+ | \DisplayProof |
||

+ | \qquad\mapsto\qquad |
||

+ | \AxRule{\Gamma^v\vdash C^v} |
||

+ | \LabelRule{\one L} |
||

+ | \UnaRule{\Gamma^v,\one\vdash C^v} |
||

+ | \LabelRule{\oc d L} |
||

+ | \UnaRule{\Gamma^v,\oc{\one}\vdash C^v} |
||

\DisplayProof |
\DisplayProof |
||

</math> |
</math> |

## Latest revision as of 22:25, 5 October 2009

The genesis of linear logic comes with a decomposition of the intuitionistic implication. Once linear logic properly defined, it corresponds to a translation of intuitionistic logic into linear logic, often called *Girard's translation*. In fact Jean-Yves Girard has defined two translations in his linear logic paper^{[1]}. We call them the call-by-name translation and the call-by-value translation.

These translations can be extended to translations of classical logic into linear logic.

## Contents |

## [edit] Call-by-name Girard's translation

Formulas are translated as:

This is extended to sequents by .

This allows one to translate the rules of intuitionistic logic into linear logic:

## [edit] Call-by-value translation

Formulas are translated as:

The translation of any formula starts with , we define such that .

The translation of sequents is .

This allows one to translate the rules of intuitionistic logic into linear logic:

We use .

### [edit] Alternative presentation

It is also possible to define as the primitive construction.

If we define , we have and thus we obtain the same translation of proofs.

## [edit] Call-by-value Girard's translation

The original version of the call-by-value translation given by Jean-Yves Girard^{[1]} is an optimisation of the previous one using properties of positive formulas.

Formulas are translated as:

The translation of any formula is a positive formula.

The translation of sequents is .

This allows one to translate the rules of intuitionistic logic into linear logic:

We use .

## [edit] References

- ↑
^{1.0}^{1.1}Girard, Jean-Yves.*Linear logic*. Theoretical Computer Science. Volume 50, Issue 1, pp. 1-101, doi:10.1016/0304-3975(87)90045-4, 1987.