[Caml-list] Problem formalizing a representation

[Caml-list] Problem formalizing a representation

[Nicolas FRANCOIS]

Hi.

I'd like to represent logical formulas for different logics.

A logic is syntactically represented by atoms, and rules involving (at
the very least) and, or, not, and possibly implies and equivalence...

What differs between my logics is the atoms :
- for propositional logic LP, atoms are just variables, and
  interpretations assign true or false to those variables ;
- the there is a logic LQ, where atoms are of the form
  "variable=r"
  r being a rational number (there may later be atoms of the form
  "variable >= r", and so on).

Then, with those logics, I can define new logics, for example, with LP,
I can define atoms of the form a^+, meaning a was false and becomes
true, or a^.1, meaning a was anything, but becomes true...

So what I would like to do is create some parametrized types (or
modules), taking atoms types as parameter, the methods for manipulating
logics (for example, computing a normal form) being defined in those
types (via modules, maybe ?), independently of the atoms types, and the
code for manipulating atoms being inside each atom type.

last but not least, certain methods would have to take two formulas
from a logic, and build with them a formula of a new type.

I don't know if I'm perfectly clear (as a matter of fact, I'm quite
sure I'm not :-(, but maybe I gave you a sufficiently clear image of
what I want to do for you to give me some tips...

The problem is I've never used parametrized modules or objects, so I
don't know how to start. If you could give me the initial thrust, maybe
I could fly :-)

Thank you for any tip, and sorry for my poor english.

\bye

-- 

Nicolas FRANCOIS                      |  /\ 
http://nicolas.francois.free.fr       | |__|
				      X--/\\
We are the Micro$oft.		        _\_V
Resistance is futile.		    
You will be assimilated.         darthvader penguin

Re: [Caml-list] Problem formalizing a representation

[Oleg]

> I'd like to represent logical formulas for different logics.
>
> A logic is syntactically represented by atoms, and rules involving (at
> the very least) and, or, not, and possibly implies and equivalence...
>
> What differs between my logics is the atoms :
> - for propositional logic LP, atoms are just variables, and
>   interpretations assign true or false to those variables ;

You have probably received lots of help already. Just in case, let me
mention that back in 2019 I gave a short course at a Dagstuhl summer
school on meta-programming on a similar topic. It was
formulated a bit differently: wires (instead of atoms) and logical
gates (as connectives).

        http://okmij.org/ftp/tagless-final/course2/index.html

Starting from zero, the course dealt with various transformations
(NAND conversion), constant propagation (or unit propagation, as
sometimes called) and finally the CNF conversion
(normalization). Actually the course finished with circuits (gate
assemblies with several inputs and outputs), full adder and applying
unit propagation/CNF to all these things, but you probably don't need
that. There was an exercise to make wires more interesting, like
32-bit busses.

As you can see from the course materials, I talked a lot about
parameterization.