Re: [sio-dev] Definition of the SIO project

[rick@xxxxxxxxxxxxxx]

John, Thank you for the excellent examples. 

JFS> The question of strong typing vs. weak typing vs. untyped languages has been debated in many different variations for a long time.

The HETs infrastructure provides two capabilities that emerged from as well as extended this debate: type inference and theorems for free.

JFS> 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.

I understand the design decision.

Type inference is the capability to automatically deduce the type of an _expression_ at compile-time. This capability could possibly be quite useful in deducing types from untyped CL expressions.

And who wouldn't want something for free. Here's a fun paper on how from the type of a polymorphic function one can derive a theorem it satisfies. [1] The trick is based on Reynold's abstraction theorem for polymorphic lambda calculus. 

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.

JFS > 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. 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 yof them could transmit statements to CL.

That's an excellent insight and I think the translation would be very valuable for the OOR infrastructure.

Also valuable to the infrastructure might be to embed CL as an object language in HETs possibly using a CASL specification. Using CASL, HETs operationalizes logic translations with Instiutions.

1. http://www.mpi-sws.org/~dreyer/tor/papers/wadler.pdf

--
Rick
_________________________________________________________________ 
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     (01)