Concise notation for event-token reification

Hi,

I'm trying to find a concise form of event-token reification (as described
by Donald Davidson).
I'm using types to avoid the need for parens. All functions have fixed arity
and the only brackets left are those marking beginning and ending of blocks
(kind of lists. I'm using some of REBOL terminology, because the syntax ends
up looking much like REBOL, that is, Polish notation). Even those can be
reduced, by only having the block end marker. For those rare cases where a
block is passed by name instead of explicitly, a keyword overrides this
behavior.

[DISCLAMER: I don't claim to have any deep knowledge of type theory and
other stuff I may mention. I'm just playing with the idea of making an
expressive logical language based of event-token-reification (ETR), among
other things. There may be big beginner mistakes in my ideas and I'm looking
for help.]


What we want to express is a sentence like this:
"Brutus killed the emperor with a knife"

If we use ETR it may be something like this:


(exists (?e) (and (eventOfType kills ?e)(subj Brutus ?e) (obj (the emperor)
e) ((a-role w-instr knife)e) ))

Where:
(def a-role  (lambda (?r ?p ?a) (exists (x) (and (?r ?x ?a)(exists (e2) (and
(eventOfType ?p ?e2)(subj ?x ?e2))  ))) ))



So, these are my types:

o: object (individual)
v: truth value (T|F)
b: block

Now let's declare the types of some symbols:

declare L#kills [a] :: b->v
declare kills [a b] :: o->o->v

declare L#isAknife [a] :: b->v
declare isAknife [a] :: o->v

declare L#isAnEmperor [ a] :: b->v
declare isAnEmperor [a] :: o->v

declare longsnt [p] :: (o->o->v)->(o->o->b->v)

declare Brutus [ ]:: o
declare subj [a b] :: o->o->v
declare obj [a b] :: o->o->v
declare w-instr [a b] :: o->o->v
declare the [p] :: (o->v)->o
declare a-role [r p] :: (o->o->v)->(o->v)->o->v

Notes:

_ I assume implicit currying of all functions.

_ I'm also assuming we have a particular interpretation, so that predicates
have the form b->v or o->v, that is, they yield a truth value without having
to apply them to a possible world or things like that. I'm not sure about
the formal semantics of the language. I have some ideas, but those are for
another thread. Of course, comments on this subject are also welcome.

_the "L#" version of a verb is the long version, which takes a block and
gives a truth value.
the sorter version has, by convention,  the same name minus the "L#". The
short version is declared from de long one.
The short version only takes the arguments for subject and object (which
lets us ommit "subj" and "obj" in the sentence), and  it doesn't take a
block, where the additional thematic roles would be, so it lets us ommit the
block ending mark ("end") but this makes it less expressive than the "#L"
form. That's why we also define a "longsnt" (long sentence) function, which
takes the "kills" function and returns a function that does accept a block
for additional roles.


L#kills obj the isAnEmperor subj Brutus  a-role w-instr isAKnife end

_parsing: (L#kills [obj the isAnEmperor subj Brutus  a-role w-instr
isAknife] )


kills the isAnEmperor Brutus

_parsing: (kills (the isAnEmperor) Brutus)


longsnt kills the isAnEmperor Brutus a-role w-instr isAKnife end

_parsing: ( (longsnt kills) (the isAnEmperor) Brutus [a-role w-instr
isAKnife] )



The types let us get rid of most brackets, but we need fixed arity
functions, and we use blocks (lists, tuples,..) for things with variable
number of items. The evaluation is Polish notation, much like in REBOL.
Since we use lots of lists, we ommit the beginning of the list and only
write "end" at the end of the block. There's a "noblk" keyword that lets us
pass a value as a list instead of writing down the list. There's also a
"bgnblk" keyword to be used in combination with that. For instance:

declare exampleBlock :: b

def exampleBlock obj the emperor subj Brutus  a-role w-instr knife end

OR:

def exampleBlock noblk bgnblk obj the emperor subj Brutus  a-role w-instr
knife end

And then we can use it:

L#kills noblk exampleBlock


You see, I want to treat "emperor" and "knife" as states, which can begin
and end, and have a subject (BTW, I won't enter on whether to make the
language accusative, ergative or tripartite at this moment. I keep it
accusative in these examples, for simplicity), so much of what applies to
"kills" and "L#kills" applies to them. To avoid confusion, I'll declare the
predicates "L#isAnEmperor" and "L#isAKnife", and then their short forms.

So, we can say: "Brutus killed the then-emperor with a knife":

L#kills lam-x obj the lam-x L#isAnEmperor subj x time-1* super-x end subj
Brutus  a-role w-instr isAKnife end



lam-x means "lambda (x)". This way we avoid having to name a variable. We
win concision.
"super-x" refers the "x" in the next outer closure. That's a way to avoid
name collisions in nested lambda expressions. The "super-x" would have a
dedicated short word. Notice that the outer lam-x is of type o->v as
required.

time-1*: The "1" means that the beginning of the L#isAnEmperor event is in
the position "1" with respect to the  L#kills event, and the "*" means that
we don't care about the relative position of the ending of the L#isAnEmperor
event,that is:

"time-1* L#kills-event  L#isAnEmperor-event"

For instance, if we have two events, A and B, and the sequence is "begin-A
begin-B end-B end-A", then we say "time-15 B A". The range of 1 to 5 is due
to the fact that intervals have two points, so, begin-A could be before
begin-B (1), coinciding with begin-B (2), inside B (3), coinciding with
end-B (4) or after B (5). In the conlang implementation "time-15" would be
three short words, or maybe just one.

For this kind of situation, instead of the nested lambdas we can define a
function "the-when-role", so that in this case we would say:

L#kills the-when-role time-1* obj isAnEmperor subj Brutus  a-role w-instr
isAKnife end

We can also define an "a-when-role"

L#kills the-when-role time-1* obj isAnEmperor a-when-role time-*1 subj
isTrustedByCaesar a-role w-instr isAKnife end


----------

Now MY QUESTION is:

I need a function to take a block and return another block where the items
have been recursively wrapped in inner blocks according to their types, so
that the return block is made of blocks, and each of these inner blocks,
when applied, is of type o->v. Let's call this function "smartReduce", for
similarity with REBOL's "reduce".

For instance  (using "_#" for user imput and "_>" for the interpreter's
output):

_# smartReduce [obj the emperor subj Brutus  a-role w-instr knife]
_> [ [obj the emperor] [subj Brutus]  [a-role w-instr knife] ]

_# def exampleBlock [ obj the emperor subj Brutus  a-role w-instr knife ]
_>

_# map [tail-block-concat [e]] exampleBlock
_>[ [obj the emperor e] [subj Brutus e]  [a-role w-instr knife e] ]


You get the idea :)

Any help and/or feedback appreciated.

Regards,

        Martin O.B.