[Ricorsione] Logica informatica

[Katakleido]

Sto studiando per un esame e mi sono imbattuto in due esercizi che non so come risolvere:

1) Considerare formule generate dalla sintassi
F::=⊥|¬F|F∧F|F∨F
Definire per ricorsione strutturale una funzione c(F) che ritorni true sse tutte le negazioni occorrono come sottoformule di almeno una congiunzione.
Esempio:
c(¬(⊥∧⊥)) = false
c(⊥∧(⊥∨¬⊥)) = true

Qui il grande dubbio è: come faccio, dopo aver appurato che c'è una congiunzione, vedere se c'è anche la negazione nelle sue sottoproduzioni immediate?

2) Considerare le liste di numeri naturali definite dalla grammatica
L::= [] | N::L
dove [] rappresenta la lista vuota e N::L la lista con il naturale N in testa e L come coda. Scrivere una funzione f(L) che ordini la lista L usando esclusivamente ricorsione strutturale. Come al solito, è possibile usare funzioni ausiliarie purchè definite anch’esse per ricorsione strutturale.

Come posso scorrere la lista ed ordinarla?

Grazie

[apatriarca]

1) Nel primo punto ragionerei come segue:
\[\begin{align*}
c(\bot) &= \mathrm{true} \\
c(\lnot F) &= \mathrm{false} \\
c(F_1 \wedge F_2) &= \mathrm{true} \\
c(F_1 \vee F_2) &= c(F_1) \wedge c(F_2)
\end{align*}\]
L'idea è che supponendo di partire dal "basso" e costruendo l'espressione da lì, ogni negazione porta ad un valore negativo nel risultato a meno che non ci sia una congiunzione a "catturare" tale valore. La disgiunzione è la più complicata in quanto sta semplicemente trasportando il valore negativo in alto. Non ho mai davvero fatto queste cose, ma spero sia più o meno chiara come idea.

2) Ci sono molti metodi per ordinare liste, esattamente come avviene per gli array. In effetti quasi ogni metodo di ordinamento può essere convertito in modo da usare una lista. Alcuni algoritmi abbastanza semplici possono essere l'insertion sort o il merge sort. Per esempio il merge sort sarebbe qualcosa come il seguente:

Codice:

split (a:b:xs) odds evens = split xs (a:odds) (b:evens)
split (a:xs) odds evens = ( a:odds, evens )
split [] odds evens = (odds, evens)

merge [] ys = ys
merge xs [] = xs
merge (x:xs) (y:ys) = if x < y then (x : merge xs (y:ys)) else (y : merge (x:xs) ys)

sort xs = let odds, evens = split xs [] [] in merge (sort odds) (sort evens)


Non ho testato il codice, l'ho scritto sul momento.. Potrebbe insomma contenere errori. La sintassi è quella di Haskell, un linguaggio funzionale pure in cui le liste sono definite esattamente in quel modo.