Le modèle relationnel de la logique linéaire est (trop) simple : on interprète une formule par un ensemble ; et une preuve par un sous-ensemble.
Les espace cohérents ou hyper-cohérent, les espaces de finitude peuvent être vus comme des raffinements du modèle relationnel, auquel on a rajouté de la structure.
Après un court rappel sur le modèle relationnel, je présenterais deux nouveaux modèles :
Ces deux modèles ont une présentation très différente mais sont en fait isomorphes. D'un certain coté, (2) est un représentation concrète de (1).
Un de leurs intérêts est qu'ils permettent de modéliser le non-déterminisme en rajqoutant un notion de somme sur les preuves : on peut en faire un modèle du lambda calcul différentiel.
Un autre intérêt est que la structure des catégories présentées est beaucoup plus riche que la simple structure linéaire. Malheureusement, les intuitions autour de cette structure supplémentaire sont pour le moment disjointes des intuitions liées à la logique linéaire.