Higher-order operators should not require absolute definitions, but rather it should be encouraged that they are defined in terms of already defined operators for several reasons. Firstly, most operators in mathematics are already defined this way. Secondly, it allows for existing proof algorithms to be applied on these operators to determine their higher-order properties. For example, the commutative property could be proven on binary AND based on the explicitly defined properties of NAND and a definition of AND constructed from NAND.
Derivations should form a DAG (directed acyclic graph), meaning many of the same algorithms used in Pluto's WYSIWYR can be reused here as well.
Higher-order operators should not require absolute definitions, but rather it should be encouraged that they are defined in terms of already defined operators for several reasons. Firstly, most operators in mathematics are already defined this way. Secondly, it allows for existing proof algorithms to be applied on these operators to determine their higher-order properties. For example, the commutative property could be proven on binary AND based on the explicitly defined properties of NAND and a definition of AND constructed from NAND.
Derivations should form a DAG (directed acyclic graph), meaning many of the same algorithms used in Pluto's WYSIWYR can be reused here as well.