orcmid / miser

The Miser Project is practical demonstration of computation-theoretical aspects of software
https://orcmid.github.io/miser/
Apache License 2.0
3 stars 1 forks source link

Need intensional printing #32

Closed orcmid closed 3 years ago

orcmid commented 4 years ago

One of the limitations of oFrugal is that the canonical form ob-exp is not as useful for representing anything else, in contrast with the way LISP S-Expressions are usable for practical disguises.

Until there is some rational handling of types and symbolic expression of type forms, and also printable strings for them, there are limited disguise forms.

Part of oMiser and oFrugal being the way they are is because I did not favor the disguising that is so common with LISP, especially when it comes to messing with the REPL reader. So oMiser is closer to the M-expression of LISP semantics and I am happy about that. The goal is to expose oMiser as realization of the ‹ob› model of computation in this consistent manner.

It is also desirable to express representations in a manner that manifests the entity being interpreted in ‹ob›. There are ways to accomplish that early, with a little help from oFrugal.

Default Bare Output

In the oFrugal REPL, the standard output for a bare ob-exp is a pretty-printed canonical form. The pretty printing uses the occurrence of obap primitives as clues to off-side layout that aligns certain operators and their operands. For example,

 .C :: `.C
    :: .C :: (.E :: .C :: (.E :: .ARG)
                       :: `.ARG)
          :: `(.C :: (.E :: .ARG)
                  :: `.ARG),

the value of ^cS, a representation of combinator S established in combinators.txt.

The use of indentation white-space in this manner is irrelevant to the semantics. The key provision is that if the output expression were submitted back to the oFrugal REPL, the output would be an expression for the same ob. That is, canonical forms expressed in ob-exp have that ob expressed by canonical form in the output once again. It is an elaborate expression for a constant ob.

Intensional Formatting

The bare oFrugal output does reflect some intensional presumptions based on appearance of primitives in the structure of an ob. Occurrence of primitives is taken as signalling likely intended use as a script. The pretty-printed forms set off indented parts such that the expression of operands for primitive-associated operations are easily identified.

What is also sought here is a kind of decompiling (or disassembly) into an ob-exp that gives rise to the same ob via applicative expression.

There is a simple case involving lindies. The evaluation of script A :: B :: C is the same as that of ob-exp A B C. And of [A, B, C:] for that matter. All three of these forms of ob-exp lead to result A :: B :: C, and one could choose to prefer the applicative or list expression based on knowledge of the intended situation.

For oMiser, it falls to oFrugal for satisfyiing such expectations. This would apply to the complete result of an ob-exp in the simplest case. More complex situations require extensions beyone oMiser.

Lindy Disguises

The rules for Lindies provide a means for expression of representations. An oFrugal command can be used to render a pure-lindy trace such as (x ;; z) :: y :: z in the form such as (x z) y z that has the same ob-exp semantics.

In this case, oFrugal commands

!apexp (x :: y) :: y :: z;
!apexp (x y) y z;;

are proposed to both produce output text (x y) y z.

This allows certain kinds of canonical forms to be more-readable disguises for a representation.

The idea is to present a stream-lined ob-exp the eval of which would yield the same canonical form ob given as the operand of the command. Essentially, x :: y is replaced by some form of .C (x, y) with some crafty in-lining depending on the nature of the operands.

Unfortunately, !apexp defined on every ob, is not so helpful. For example,

!apexp  .C :: `.C
           :: .C :: (.E :: .C :: (.E :: .ARG)
                              :: `.ARG)
                 :: `(.C :: (.E :: .ARG)
                         :: `.ARG);

is difficult to consider if the goal is an applicative expression with eval result being the same ob as that provided as the operand. Inference of a list form is helpful but not so useful.

[  .C, '.C, .C,  .E :: C :: (.E :: ARG) :: ` .ARG, ' [.C,  .E :: .ARG, ' .ARG :] :]

and then, being obsessive about it,

[  .C, '.C, .C, [ .E, .C, .E :: ARG , ` .ARG:], ' [.C,  .E :: .ARG, ' .ARG :] :]

Re-Abstraction

It would be even more useful to be able to re-abstract (what would be a better term?) an ob. It is possible to make functions that expose the applicative structure better. A sort of re-lambda procedure, such that

!def ob ^dcS =^dλ.z ^dλ.y ^dλ.x  ^cS;

(reading dλ as de-lambda) would result in

^dcS =( x :: z) :: y :: z

with

!apexp ^dcS;

yielding (x z) y z.

Note the reversal with respect to ^λ.x ^λ.y ^λ.z (x z) y z.

This case features two problems. First, choosing names (here represented by lindies) for the "bound" variables in the re-abstraction. oMiser has nothing comparable to a source-code that is retained somehow by the ^λ (and ^ρ) procedures. Secondly, binding names are ephemeral and the bindings are mutable. There are no reserved binding names and there is no means for naming obs that can be used for persistent collections (libriaries) of them (issue #31).

Without higher-level machinery and treatment of shared definitions, precise re-abstraction is unobtainable.

orcmid commented 4 years ago

I don't know that !aexp is worth it, although i tis an interesting exercise. The Lindy disguise situation is not unlike the S-expression disguising business.. It makes the treatment of lindies in the ‹ob› model of computation rather fortuitous.

It is very clear that without reconciliation of bindings and libraries with regard to extensional equality, if maintained, use of oFrugal is very ungainly..

I also think that reconciliation with stateful arrangenents, including assignment operations, is the hold-up. Until that is accomplished in a tractable manner, I must withhold thoughts about bridging higher with oMiser, perhaps requiring a change of level first.

orcmid commented 4 years ago

I had a brain-fart with regard to !apexp producing list-style ob-exps. In demonstration of Turing machines,

Basically, tapes are represented by a tape pair, back :: aheadwith ahead a list of forward tape entries and back a list of backwards tape entries, nearest first. The next position read will be .a ahead. There is also a state that goes with that configuration and we could save all that as state :: tape. The elements are all lindies.

In this case, that structure is indistinguishable from a list, [state, back, ahead:] except ahead would be expanded. For an initial start, back could just be .NIL. The expansion of back is rather problematic if lengthy.

Of course, to specify the particular TM as well as the configuration we are back to the issue #31 problem of having persistent namings that can be relied upon or some compromise accommodation.