Lazi

SFP (Sub-Formula Path , chemin de sous-formule)

Contexte

On cherche un moyen d'identifier un endroit quelconque dans une formule.

Définition

Pour une formule x, s est un SFP de x ssi s est une liste binaire vérifiant la disjonction :

  • s est vide
  • x est une application, le premier élément de la liste s est 0b et le reste de s est un SFP pour la partie fonction de x
  • x est une application, le premier élément de la liste s est 1b et le reste de s est un SFP pour la partie argument de x

De cette définition on déduit l'endroit identifié par un SFP : la formule entière pour la liste vide, si la liste commence par 0b on relativise à la partie fonction (et pour 1b à la partie argument), puis on continue récursivement.