Supponiamo di avere un insieme di funzioni che caratterizzano qualcosa: nei metodi del mondo OO che caratterizzano un tipo. In matematica queste sono proposizioni e abbiamo due tipi: assiomi e lemmi. Gli assiomi sono assunzioni, i lemmi sono facilmente derivati da loro. Negli assiomi C ++ sono pure funzioni virtuali.
Ecco il problema: c'è più di un modo per assiomatizzare un sistema. Dato un insieme di proposizioni o metodi, un sottoinsieme delle proposizioni che è necessario e sufficiente per derivare tutti gli altri è chiamato una base.
Allo stesso modo, per i metodi o le funzioni, abbiamo un insieme desiderato che deve essere definito, e in genere ognuno ha una o più definizioni in termini degli altri, e chiediamo al programmatore di fornire definizioni di istanza che siano sufficienti per consentire tutti gli altri da definire e, se c'è un eccesso di specificazione, allora è coerente.
Lasciatemi fare un esempio (in Felix, il codice Haskell sarebbe simile):
class Eq[t] {
virtual fun ==(x:t,y:t):bool => eq(x,y);
virtual fun eq(x:t, y:t)=> x == y;
virtual fun != (x:t,y:t):bool => not (x == y);
axiom reflex(x:t): x == x;
axiom sym(x:t, y:t): (x == y) == (y == x);
axiom trans(x:t, y:t, z:t): implies(x == y and y == z, x == z);
}
Qui è chiaro: il programmatore deve definire == o eq o entrambi. Se entrambi sono definiti, le definizioni devono essere equivalenti. La mancata definizione di uno non causa un errore del compilatore, causa un loop infinito in fase di esecuzione. Definire entrambi inequivocabilmente non causa nemmeno un errore, è solo incoerente. Si noti che gli assiomi specificati vincolano la semantica di qualsiasi definizione. Data una definizione di == direttamente o tramite una definizione di eq, allora! = Viene definito automaticamente, anche se il programmatore potrebbe sostituire l'impostazione predefinita con qualcosa di più efficiente, chiaramente tale overspecification deve essere coerente.
Si noti che == potrebbe anche essere definito in termini di! =, ma non lo abbiamo fatto.
Una caratterizzazione di un ordine parziale o totale è più complessa. È molto più impegnativo in quanto vi è un'esplosione combinatoria di basi possibili.
C'è una ragione per desiderare una eccessiva precisazione: le prestazioni. C'è anche un altro motivo: scelta e convenienza.
Quindi qui ci sono diverse domande: una è come controllare che la semantica sia rispettata e non sto cercando una risposta qui (troppo difficile!). L'altra domanda è:
Come possiamo specificare e verificare che un'istanza fornisca almeno una base?
E una domanda molto più difficile: come possiamo fornire diverse definizioni predefinite che dipendono dalla base scelta?