Rick, (01)
The question of strong typing vs. weak typing vs. untyped languages
has been debated in many different variations for a long time. In
programming languages, the debates have swung back and forth since
the 1960s. In versions of logic, the debates have been going on
even longer. Following is a brief summary of the issues: (02)
1. Types restrict the range of variables. Therefore, an untyped
language is more expressive than a typed language (in the sense
that any statement in a typed language can be translated to
an untyped language, but not vice versa). (03)
2. A strongly typed language (such as the Z specification language)
enforces type checking in the syntax. Therefore, typing errors
can cause a sentence to be rejected as syntactically incorrect.
This kind of early detection is often helpful for programming
languages. (But it can also be a nuisance when an editing
program barks at you while you're typing a statement.) (04)
3. A weakly typed language allows syntactically correct sentences
to contain typing errors. This option has some advantages and
some disadvantages. (05)
4. An untyped language places no restrictions on the types of any
variable. For a language that is designed as a generalization
of many different kinds of languages with different typing
conventions, it may be necessary to have an untyped language. (06)
Since common Logic is intended to be a generalization of many
different kinds of logic, including strongly typed languages such
as Z and untyped languages such as full OWL and RDF, it had to
be untyped. (07)
However, CL does support quantifier restrictions, which support
a kind of weak typing. For example, the sentence "A cat is on
a mat" can be represented by the following untyped CLIF sentence: (08)
(exists (x y) (and (Cat x) (Mat y) (On x y))) (09)
But it can also be represented with restricted quantifiers by
using the monadic relations Cat and Mat as quantifier restrictions: (010)
(exists((x Cat) (y Mat)) (On x y)) (011)
This says that there exists an x of type Cat, a y of type Mat,
and x is on y. Note that it's somewhat shorter and more
readable than the untyped version. But it's only a weak kind
of typing because a type error simply makes a sentence false.
It does not make the sentence syntactically incorrect. (012)
As another example, consider the following CLIF sentence, which
says that there exists an elephant x, which is equal to 23: (013)
(exists ((x Elephant)) (= x 23)) (014)
In CL, this sentence is syntactically correct, but semantically
false. But the equivalent sentence in Z would be syntactically
incorrect. It;s truth value could not be evaluated. (015)
RM> In the context of http://www.paultaylor.eu/stable/prot.pdf the
> types of Girard's System F whose implementations are typically
> some refinement of the Hindley Milner type system. (016)
I haven't checked the details, but I don't see any problems in
translating sentences in that logic into CL. The type constraints
would be translated to monadic relations used as restrictions on
the quantifiers. A syntax error caused by a typing error in
that logic would just be translated to a false statement in CL. (017)
With that kind of flexibility, CL can accept input from two
strongly typed languages with different typing conventions.
They couldn't share data between themselves, but both of them
could transmit statements to CL. (018)
John (019)
_________________________________________________________________
Msg Archives: http://ontolog.cim3.net/forum/sio-dev/
Join Community: http://ontolog.cim3.net/cgi-bin/wiki.pl?WikiHomePage#nid1J
Subscribe/Config: http://ontolog.cim3.net/mailman/listinfo/sio-dev/
Unsubscribe: mailto:sio-dev-leave@xxxxxxxxxxxxxxxx
Community Shared Files: http://ontolog.cim3.net/file/work/SIO/
Community Wiki:
http://ontolog.cim3.net/cgi-bin/wiki.pl?SharingIntegratingOntologies (020)
|