next up previous Sommario
Next: 7.3 Strumenti per la Up: 7. Il linguaggio Gödel Previous: 7.1 Una semantica semplice   Sommario

7.2 Il Type System

Le motivazioni per avere i tipi in un linguaggio per la programmazione logica possono essere riassunte nelle seguenti: usando i tipi si può più direttamente rappresentare la conoscenza rilevante in un'applicazione; inoltre le dichiarazioni di tipi possono essere usate dal compilatore per produrre un codice più efficiente; infine le dichiarazioni di tipi possono facilitare la rilevazione di errori e la stesura di programmi corretti.



Nei sistemi Prolog generalmente non è presente un type system, che deve essere quindi, quando necessario, realizzato dal programmatore, con tutti i problemi di efficienza conseguenti.

Il Gödel fornisce un type system basato sulla logica many-sorted: tale logica generalizza le ordinarie logiche del primo ordine unsorted in quanto ha una dichiarazione di tipo per ogni variabile, costante, funzione e predicato nel linguaggio.

Per trattare logiche many-sorted è necessario generalizzare le nozioni usuali di interpretazione, conseguenza logica e così via. L'idea chiave è che una interpretazione many-sorted ha un dominio per ogni tipo e così ogni costante, per esempio, è assegnata da una interpretazione ad un elemento del dominio corrispondente al suo tipo. Similmente si generalizzano le restanti nozioni semantiche.

Le logiche many-sorted non sono più generali delle logiche unsorted, ma sono molto più espressive e permettono di evitare l'uso dei predicati necessari per definire i tipi nelle logiche unsorted.



Il Gödel permette inoltre una forma di polimorfismo sui tipi, detto polimorfismo parametrico. Tale polimorfismo, usuale nei linguaggi per la programmazione funzionale, permette, per mezzo dell'introduzione di variabili di tipo, di scrivere predicati che possono avere argomenti il cui tipo può variare. Un esempio può essere il predicato Append che, definito su argomenti di tipo List(alpha), con alpha variabile di tipo, potrà essere applicato di volta in volta a liste di elementi di diverso tipo.

Il Type System del Gödel è fortemente tipato e il tipo di ogni costante, funzione, proposizione e predicato deve essere specificato per mezzo di dichiarazioni.


next up previous Sommario
Next: 7.3 Strumenti per la Up: 7. Il linguaggio Gödel Previous: 7.1 Una semantica semplice   Sommario
Roberto Giungato 2001-03-14