SPECIFICA INIZIALE DELLE MAPPE FINITE

v. 0.0Gianna Reggio

reggio@disi.unige.it

Ver. 0.0

Naturali “iniziale”spec NATi = Sorts natOpns 0: nat succ: nat -> nat

_+_: nat x nat -> natAxioms

Def(0)Def(succ(n))

Def(n + m) ** 0 + n = n

succ(m) + n = succ(m+n)

• Esercizio 50: caratterizzare il modelo iniziale di NATi, se esiste.

• Esercizio 51: se eliminiamo l’assioma **, cambia il modello iniziale.

• Esercizio 52: estendere NATi con le altre 4 operazioni(-,*,mod,div).

Ver. 0.0

Esercizio 50• Il modello iniziale esiste poichè la specifica è positiva condizionale.• Usiamo la caratterizzazione vista a lezione I(NATi) = TSig(NATi) /~NATi

inoltre sappiamo che la congruenza ~NATi (indicata semplicemente da ~ nel seguito) può essere definita utilizzando il sistema di Birkhoff

• Tutte le operazioni sono totali e quindi ~ contiene tutte le coppie (t,t) con t termine ground su Sig(NATi)

• [@] Intuiamo che dagli assiomi consegue che per ogni t termine ground su Sig(NATi) esiste n≥0 t.c. t ~ succn(0). Proviamo ciò per induzione sulla struttura di t.– Base t = 0 Ovvio.– Step 2 casi

• t = succ(t1) Per l’ipotesi induttiva t1 ~ succn(0); pertanto t ~ succ(succn(0))= succn+1(0) (~ è una congruenza).

• t = t1 + t2 Per l’ipotesi induttiva t1 ~ succn(0) e t2 ~ succm(0). Usando Birkhoff possiamo provare che succn(0) + succm(0) = succn+m(0) (vedi dopo). Essendo Birkhoff sound, t ~ succn+m(0).

• Quindi il modello iniziale di NATi descrive precisamente i naturali intesi nel modo ovvio.

Ver. 0.0

Esercizio 50 (continauzione)• Prova con Birkhoff di

succn(0) + succm(0) = succn+m(0) per ogni n, m ≥ 0 [perchè n, m italici ???]

• per induzione su n– base n = 0

0 + n = n________Assioma proprio

0 + succm(0) = succm(0)__________Istanziazione

– step n = p+1

succp(0) + succm(0) = succp+m(0)

________________per l’ipotesi induttiva…………...

succ(n) + m = succ(n+m)________________________Assioma proprio__________________________________________________

succ(succp(0)) + succm(0) = succ(succp(0)+ succm(0) )Istanziazione

succ(succp(0) + succm(0)) = succ1+p+m(0)

________________congruenza

__________________________________________________

succ(succp(0)) + succm(0) = succ1+p+m(0)transitività

Ver. 0.0

Esercizio 51• Procediamo in modo simile all’esercizio 50;

ma in questo caso prima proviamo [@], e poi dato che I termini della forma succm(0) sono sempre definiti, usando Birkhoff proviamo che ogni t termine ground è definito.

Ver. 0.0

Aggiunta di <spec NAT1> = extend NATiPreds _<_: nat x natAxioms

x < succ(x)x < y x < succ(y)

• Esercizio 53: caratterizzare il modello iniziale, se esiste.

• Esercizio 54: definire una specifica STRINGi, tale che il suo modello iniziale caratterizzi le stringhe di caratteri.

Ver. 0.0

Esercizio 53• Per tutto ciò che non riguarda il < si ci riconduce all’esercizio 51 (poichè

non ci sono assiomi che coinvolgono sia < sia le altre operazioni, e tutte le operazioni sono totali).

• Intuiamo che dagli assiomi consegue che per ogni n,m≥0 succn(0) ~< succm(0) ses n < m. – SE m = n + p Usando Birkhoff proviamo succn(0) ~< succn+p(0)

[dopo]– SOLO SE Supponiamo di avere una prova per

succn(0) ~< succm(0). Per induzione sulla lunghezza della prova dimostriamo che n < m.

• Base primo assioma della specifica seguita da sua istanziazione provando che succn(0) ~< succn+1(0). OK

• Step La prova consiste di una prova di succn(0) ~< succm(0), seguita dal l’applicazione del secondo assioma, sua istanziazione, modus ponens.Per l’ipotesi induttiva n < m, e quindi n < m+1.

Ver. 0.0

Esercizio 53 (continuazione)• Prova con Birkhoff di

succn(0) ~< succn+p(0) per ogni n ≥ 0, p ≥ 1 • per induzione su p

– base p = 1

x < succ(x)________Assioma proprio

succn(0) < succ(succn(0))__________Istanziazione

– step p = q+1

succn(0) < succn+q(0)

________________per l’ipotesi induttiva…………...

x < y x < succ(y)________________________Assioma proprio__________________________________________________

succn(0) < succn+q(0) succn(0) < succ(succn+q(0))Istanziazione

__________________________________________________

succn(0) < succ(succn+q(0)) modus ponens

Ver. 0.0non positivi conditional

Mappe basiche (1)spec MAP = extend NATi, STRINGiSorts mapOpns

[]: map _[_/_]: map x nat x string -> map

_[_]: map x string -> natAxioms

-- [] e _[_/_] sono totaliDef([]) Def(m[n/s])-- solo l’ultima associazione di un naturale ad una-- stringam[n1/s][n2/s] = m[n2/s]s1 ≠ s2 m[n1/s1][n2/s2] = m[n2/s2][n1/s1]-- l’ordine delle associazione per stringhe diverse non-- contam[n/s][s] = ns1 ≠ s2 m[n1/s1][s2] = m[s2]

Ver. 0.0

Mappe basiche (2)Occorre definire Preds difS: string x string-- definibile con assiomi positivi conditionaldifS(s1,s2) m[n1/s1][n2/s2] = m[n2/s2][n1/s1]-- l’ordine delle associazione per stringhe diverse non-- contadifS(s1,s2) m[n1/s1][s2] = m[s2]

Esercizio 55: definire difS, il predicato corrispondente alla differenza tra stringhe.

Ver. 0.0

Insiemi di naturalispec SET-NATi = extend NATSorts set-natOpns-- costruttori

{}: set-nat{_}: nat -> set-nat -- singleton__: set-nat x set-nat -> set-nat

card: set-nat -> nat Preds isIn: nat x set-natAxioms-- tutte le operazioni sono totalidef({}) def({b}) def(s1 U s2)-- è comm, assoc, idempotente e {} è la sua identitàs1 s2 = s2 s1(s1 s2) s3 = s1 (s2 s3)s s = s {} s = scard({}) = 0card({n} s) = succ(card(s))Esercizio 56: trovare assioma errato, cioè che richiede una

proprietà non ragionevole per gli insiemi di naturaliEsercizio 57: caratterizzare il modello iniziale di

SET-NATi.

Ver. 0.0

Esercizio 56• L’assioma errato è l’ultimo; infatti implicitamente richiede che

tutti i naturali maggiori di 0 siano identificati con 1. Proviamolo con Birkhoff. Per semplicità diamo solo la prova di succ(succ((0)) = succ(0).

Ver. 0.0

Operazioni su mappeEsercizio 58: dare una specifica il cui modello iniziale corrisponde

alle mappe con dominio e codominio.

Esercizio 59: aggiungere anche un’operazione di restrizione ad un sottinisieme del codominio, e di combinazione di due mappe, con la

seconda che override le associazioni della prima in caso di conflitto.