A Too-Simple Model of X-Logic
A simple model of semantics and soundness for X-Logic.
Purposes and key ideas.
An overview of the model with specifications of the various types of entity involved in it.
Three kinds of proposition are defined, concerning truth of documents, correctness of programs and derivation of documents.
Elementary reasoning about inferences and their composition.
Purposes and key ideas.

The main purposes are:

  1. To provide a simple formal exposition of the core concepts of X-Logic
  2. To provide the basis for the XL-Glue proof tool.
  3. To provide some informal examples to clarify the point of it all.
Key Ideas

X-Logic is a document oriented logical framework for the semantic web. At the X-Logic level we are concerned with documents as assertions, and with programs performing inferences by reading documents and creating new documents.

The key surprises here are:

  1. The languages which concern us here are not just logics, but any language which has a propositional semantics, and any language can be given a propositional semantics (or two).
  2. The things which do inference are not just theorem provers, but any program which has a propositional specification, and any program can be given a propositional specification (or two).

The Theory xl-mm1
We here introduce the new theory in the context of galactic set theory (though it could have been done in less exotic environs).
open_theory "gst";
set_pc "gst";
force_new_theory "xl-mm1";
force_new_pc "xl-mm1";

This is just the first stage in the development of models for XL-Glue, and doesn't yield a good model. I had hoped that it would be useful for the exposition of the "two key ideas", but even for that purpose it would need to be reworked substantially. The second metamodel seems to me better, but because it is intended to address the use of digital signatures it is also significantly more complex. Someday this will have to be redone.
An overview of the model with specifications of the various types of entity involved in it.
Domain of Discourse

The subject matter of the model is programs which perform transformations over documents, which are written in a variety of languages.

We take the set of documents to be unspecified. A language is modelled as a set of documents.

This should be understood as a purely semantic definition, in which the essential feature of a document is that it expresses an assertion, and the only matter of interest for our present purposes is whether that assertion is true.

Thus the set of documents which constitutes a language is the set of documents which when interpreted in that language are true.

A program is any partial function over the documents. A specification is any pair of languages, which are to be understood as the input and output languages of some program.

Basic Types
The following definition should be understood as introducing the semantic objects which correspond to the parts of a very simple language. Of these, the last three are kinds of "proposition" corresponding two three kinds of sentence which are available in our language. Informally they are the propositions respectively that a document in some language is true, that a program satisfies some specification, and that one document has been computed from another by some program.
Document Language Program Specification DocProp ProgProp InferProp :GS
¬fttabg Document
fttabLanguage = ℘g Document
fttabProgram = Document g Document
fttabSpecification = Language ×g Language
fttabDocProp = Language ×g Document
fttabProgProp = Specification ×g Program
fttabInferProp = Program ×g (Document ×g Document)
The following definitions provide constructors for the basic types.
mk_spec mk_dp mk_pp:
fttabGS → GS → GS;
fttabGS → GS → GS → GS
fttabmk_spec = $↦g
fttabmk_dp = $↦g
fttabmk_pp = $↦g
fttabmk_ip = λpr inp out•
fttabfttabpr ↦g (inp ↦g out)
The following definitions provide projection functions for extracting components from the structures.
in_lang out_lang dp_lang dp_doc
pp_spec pp_prog ip_prog ip_in ip_out
fttab:GS → GS
fttabin_lang = fst
fttabout_lang = snd
fttabdp_lang = fst
fttabdp_doc = snd
fttabpp_spec = fst
fttabpp_prog = snd
fttabip_prog = fst
fttabip_in = (λd• fst (snd d))
fttabip_out = (λd• snd (snd d))
Three kinds of proposition are defined, concerning truth of documents, correctness of programs and derivation of documents.
In this section we provide the meaning for the three kinds of proposition introduced above. In each case this is a property which should be understood as defining when the relevant kind of sentence is true.
First, a document is true in some language if it is a member of that language. (it suffices for our present purposes to model a language by its set of true sentences)
TrueDocP: GS → BOOL
∀dp• TrueDocP dp ≡
fttabdp ∈g DocProp ∧
fttab(dp_doc dp) ∈g (dp_lang dp)
Next, some document is inferred by a program from another document if the function which is the value of the program maps the second document to the first. Note that function application is not used in this statement because of the possible complication that the input document is not in the domain of the function.
DocInferP: GS → BOOL
∀ip• DocInferP ip ≡
fttabip ∈g InferProp ∧
fttab(ip_in ip) ↦g (ip_out ip) ∈g (ip_prog ip)
Finally, a program is sound with respect to some specification if any document computed by that program from a true document in its input language will be a true document of the output language.
SoundProgP: GS → BOOL
∀pp• SoundProgP pp ≡
fttabpp ∈g ProgProp ∧
ftbr ∀ind oud•
fttabTrueDocP (mk_dp (in_lang (pp_spec pp)) ind) ∧
fttabDocInferP (mk_ip (pp_prog pp) ind oud) ⇒
fttabTrueDocP (mk_dp (out_lang (pp_spec pp)) oud)
Soundness of Identity Function

This is not the kind of reasoning which the metanotation is intended for, but as a very trivial demonstation of how programs other than proof tools can do inferences for us we demonstrate that the identity function infers soundly against any specification in which the input and output languages are the same. (i.e. given a true proposition it returns the same true proposition)

In the following theorem the ⌜l ↦g l⌝ is the specification, which states that the input and output languages are both ⌜l⌝, and the right hand side of the conditional asserts that the identity function over ⌜l⌝ satisfies that specification or is sound with respect to that specification. i.e. when given a true proposition in language ⌜l⌝, it returns a true proposition in the same language. The specification does not require the output proposition to be the same as the input proposition, but in this case it is.

set_goal([],⌜∀l• l ∈g Language ⇒
SoundProgP ((l ↦g l) ↦g (id l))⌝);
a (prove_tac [
fttabget_spec ⌜id⌝,
fttabget_spec ⌜pp_spec⌝,
fttabget_spec ⌜mk_pp⌝,
fttabget_spec ⌜Language⌝,
fttabget_spec ⌜SoundProgP⌝,
fttabget_spec ⌜DocInferP⌝,
fttabget_spec ⌜TrueDocP⌝]);
a (bc_thm_tac (rewrite_rule
fttab[get_spec ⌜id⌝] id∈gg_thm2)
fttabTHEN strip_tac);
val id_spec_thm =
fttabsave_pop_thm "id_spec_thm";

Meta Reasoning
Elementary reasoning about inferences and their composition.
In the following we investigate the kind of reasoning which could be undertaken in a language suitable for talking about the model we have introduced. Rather than invent a language, we use the syntax already available to us, and build up some elementary tools for reasoning about the model. If we then devised a suitable special concrete syntax and gave this its semantics in terms of the model by a semantic embedding into ProofPower GST, the proof tools we devise here would then serve as a tools for reasoning about this new language. The step to concrete syntax will be omitted, however, since we expect further elaborations to the model before this would be worthwhile.
What kind of logic?

We have a language in which programs, modelled as functions, are applied to documents to yield new documents, and hence an expression language involving function application. We have a couple of predicates which are applied to these programs and documents. So it looks like we are heading for some kind of predicate calculus.

On the other hand, if we consider languages as types of document and specifications as types of program, then both our predicates become typing assertions in an applicative calculus. Since typing inference in pure combinatory logic is the same as a fragment of propositional logic we may hope that a metalanguage based on the simple model we have in hand will logically much simpler than the predicate calculus, and we may hope for fully automatic proofs.

Modus Ponens
The central inference rule is analogous to modus ponens.
set_goal([],⌜∀in_doc in_lan p out_doc out_lan•
ftbr TrueDocP
fttab(mk_dp in_lan in_doc)
∧ SoundProgP
fttab(mk_pp (mk_spec in_lan out_lan) p)
∧ DocInferP
fttab(mk_ip p in_doc out_doc)
⇒ TrueDocP
fttab(mk_dp out_lan out_doc)⌝ );
a (rewrite_tac[
fttabget_spec ⌜TrueDocP⌝,
fttabget_spec ⌜SoundProgP⌝,
fttabget_spec ⌜DocInferP⌝,
fttabget_spec ⌜Document⌝,
fttabget_spec ⌜mk_spec⌝,
fttabget_spec ⌜in_lang⌝]
ftbr THEN REPEAT strip_tac
ftbr THEN all_asm_fc_tac[]);
val mm1_mp_thm =
fttabsave_pop_thm "mm1_mp_thm";

Because programs are permitted only one input and one output document, the limitations of this metamodel are very severe. Now we have modus ponens we can easily compose inferences to give results over chains of computations, but that's about all we can do.
Composition of Inferences
The following proof demonstrates that sound inferences compose.
set_goal([],⌜∀d1 l1 d2 l2 d3 l3 p1 p2•
ftbr TrueDocP
fttab(mk_dp l1 d1)
∧ SoundProgP
fttab(mk_pp (mk_spec l1 l2) p1)
∧ SoundProgP
fttab(mk_pp (mk_spec l2 l3) p2)
∧ DocInferP
fttab(mk_ip p1 d1 d2)
∧ DocInferP
fttab(mk_ip p2 d2 d3)
⇒ TrueDocP
fttab(mk_dp l3 d3)⌝ );
a (REPEAT strip_tac
val mm1_mpc_thm =
fttabsave_pop_thm "mm1_mpc_thm";

up quick index © RBJ

privacy policy


$Id: xl-metamod1.xml,v 1.2 2006/03/25 22:50:36 rbj01 Exp $