search

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

Explain what has the expression of combinators be interpretation-preserving #70

Open orcmid opened 1 year ago

orcmid commented 1 year ago

That the combinators leave scripts intact and they are only applied as-is if applied at all. I what allows the emergence of simple types.

This needs to be explained in combinators.txt and it also leads to the interesting case of when scripts are acted on as data rather than used in their interpretation-preserving nature as applicative operations on obs and representations of other structures in Ob.

Transformation of scripts in other ways is a different matter and we need to bring that under scrutiny without breaking our heads on it.

orcmid commented 1 year ago

It is somewhat the case that this applies to the Combinator Arithmetic structure, ‹ca›, except that extensional equality is challenging.

It is clearly the case that the oMiser scripts in the computational interpretation do preserve intended representations of types insofar as the application of ^cK, ^cI, and ^cS, etc., simply preserve obs supplied as operands and themselves do not manipulate their operands.