The Notion of Focus

This document is called: [FOCUS]

Review

We start by reviewing some relevant NEWFOL [type]s.

[context]

All [context]s are [named-object]s, that is, they have a 'name' attribute of type [context-name] which is a SUBTYPE of [symbol]. A [context] might be defined as

(type [context] subtype [named-object]
  (its-attributes-are
    (name *type* [context-name])
    (signature *type* [signature])
    (language *type* [language])
    (simulation-structure *type* [simulation-structure])
    (facts *type* [facts]) )
  (its-constraints-are
    (forall c. CONTEXT?(c) implies
      (SIGNATURE-EQUAL 
        lang-get-signature(context-get-lang c)
        ss-get-signature(context-get-ss c) ) ) )

[system]

For simplicity, NEWFOL defines the type [system] to be an alias for [newfol-system]. A [system] is an [environment] whose indexes are [context-name]s. A [system] might be defined as

(type [newfol-system] subtype [environment]
  (its-parts-are
    (contexts
      *type* [closed-context]
      *range* [0-INF]
      *split-type* (attribute name) ) )
  (its-constraints-are
    (forall sys. (SYSTEM? sys) implies 
      (exists bn. (BRANCH-NAME sys bn) & (SYM-EQUAL bn 'Current-Context)) ) ) )

NEWFOL uses two different [representation]s for [context]s: open and closed.

Closed [context]s

A [closed-context] must be represented as a single data structure can be used as a part of a [system]. A [closed-context] might be defined as

(type [closed-context] subtype [context]
  (its-attributes-are
    (name *type* [context-name]) )
  (its-representations-are *closed-context-rep*) )

Open [context]s

Every [system] has one [context] called Current-Context, that is, its focus. This is the only [context] that can be an example of an [open-context]. The [current-context] is singled out for two reasons: one, it may have an implementation/representation that has been optimized for fast access to its parts; and two, it may be destructively manipulated but leaving its without de The [open-context] might be defined as

(type [current-context] subtype [context]
  (its-attributes-are
    (name *data* Current-Context) )
  (its-representations-are *open-context-rep*) )

Elementary vs Non-Elementary

When modeling a subject that mentions structured objects we could talk about a single example of something or about all the examples of things of its [type]. In normal conversation we switch back and forth between these 'points of view' of a subject.

An interesting question is "What principle are we using that allows us to switch between points of view? An in what context is this principle used?

In ordinary language this issue arises frequently. If we are describing a general action we would say "To mail a letter, you take your car to the village and deposit the letter in the mailbox at the post office." But if I were talking to you I would just say 'Drive to village and deposit letter in the mailbox at the post office." In other words if I am talking about the action in general, the person doing the action is mentioned in the description and if I am talking to you then I only tell you 'what to do' and do not include who is doing it.

For people knowlegable about the blocks world: In a STRIPS like system the operation called 'stack' could be described as having two arguments: 1) on object (a block) and 2) where to put it. We might write

  stack(what-to-stack,wheretostack-it).

This formulation assumes that the world where the action is to take place and who will do the action is implicit in the system. In reasoning about actions in general we need to be more explicit because these will be different in different contexts.

For mathematicians/logicians: In group theory in chapter one we are introduced to the axions of a group [axiom-group] and we prove some theorems. In chapter two we define the notion of a 'subgroup' and prove the theorem 'The order of any subgroup of a finite (for simplicity) group divides the order of the group'. Unfortunately neither the 'order of a group' nor the notion of 'subgroup' is definable using the language and axions given in chapter one, so this 'theorem' is not even stateable in the axion system of chapter one. Logicians know this and will explain that the axioms in chapter one are the axioms of the elementary theory of groups and the ideas in chapter two use the non-elementary theory of groups!!!! We have simply changed axiom systems!!!! The question for the logician is: 'What principle allows us to go from the first (elementary) axiomatization of groups to the second (non-elementary) axiomatization of groups?

If this note were just for logicians we would have called it 'Elementary vs Non-elementary Theories'.

The Smn theory for contexts

Suppose we have a [context], C, with a sort S&mdaskh;one of several—and we have an individual constant, s, of sort S. If, in the language of C, there are any function and predicate symbols whose fmaps mention S (or a sort, S1, where (MG S1 S) as an arg or (LG S S1) as a val) then we 1) replace all such fmaps with (fmap-replace fmap S1 (singleton-sort S)) and instantiate any fact that quantifies over S to quantify over S1, ... Then we can relativise the context to S and get the elementary theory of S (from any context whose language contains S).

This relativization is a function on C that is satisfaction preserving (and thus a definable 'rule of inference' in NEWFOL.

Upside Down

Both the 'Smn theorem' and 'many-sorted logic' are generally thought of as ways of preserving some property when a defining property is restricted. This is only half of the story.

Kleene's Smn theorem (XXX) says that if you have a recursive predicate, P1, of m+n arguments and you fix m of the arguments to be a constant, then there is a recursive predicate, P2, of n arguments which is logically equivalent to the 'restricted' version of P1. A corrolary of this theory dtates the result for recursive functions.

My question is: if you are given a recursive function, f2, of n arguments, what recursive function of n+m arguments is it a restriction of?

The question arises in thinking about many-sorted logic. One basic result about many-sorted logics is that if you restrict all of the quantified variables to range over a sort, S, (ie part of the domain) then all of the consequences with variables also restricted to S are 'still' consequences because the restricted quantifier rules (under the restriction to S) are 'valid' as is!!! (XXX and XXX)

Here the question is the same as above. What is the 'normal' one sorted logic the specialization of?

This relativization is a function on C that is satisfaction preserving (and thus a definable 'rule of inference' in NEWFOL.

The 'inverse' of the usual theorems are a kind of generalization and we propose such theorems and their implementation as NEWFOL rules.

--aside-implementation note----------------------------------------------------
IBUKI keeps the [current-system] as value of the [symbol] %CONTEXT-LIST% and
represents the [current-system] as an [alist] of the form
[current-system] == (alist-of [context-name] [closed-context])
The details of the representation of a [closed-context] is quite complex
and not included here.
-------------------------------------------------------------------------------