Can we abstract away from these specific structures to get a more general definition? A possible computational model is representation-transformation. Provided that we can transform a given representation in a sufficiently rich way (that is: Turing complete) then it can represent any computation that is possible. There are limits to what computations are possible as shown by applying Godel's incompleteness theorems to computation. This gives rise to the concept of undecidable problems.
So a 'representation' may for example be a string, but since the string may contain brackets we can represent tree structures and many other structures. Tree structues do seem to be a very good represention for modelling many computations in an efficient way.
Our 'transformation' may be a sequence of steps, or an algorithm, or a function.
We are also interested in the relationship to logic, this approach is based on the ideas of Philip Wadler [1] and others. A program that uses this approach is Djinn [2]
The arguments of these 'computation' domains are functions and combinators and the operation is usually function application, although other operations such as function composition and cartesian product may also be supported.
For combinators the number of arguments is variable and so function application is non-associative hence it is represented by binary tree structure.
For Lambda calculus function application is the opposite process to the lambda function, that is lambda creates a function with a bound variable and function application removes the bound variable. Since we have bound and unbound variables so again non-associative and represented by binary tree structure.
I am also working on a framework for function composition.
https://www.euclideanspace.com/maths/standards/program/mycode/homset/Function composition is associative and so can be represented by a list structure. It therefore has different mathematical properties to the structures studied here but they can be related to closed cartesian categories.
These domains all represent systems of logic and are constructed from tree structures and act on tree structures. These 'tree logics' seem to 'generate' other algebras, for instance, below, we see that this lambda structure:
\x.\y.y x
can be converted to this SKI structure:
S(K(SI))(S(KK)I)
This allows us to 'abstract' the definition, in that it takes a definition in terms of arbitrary variables and it converts to a definition without arbitrary variables. So these structures are equivalent and they both reverse two operands. That is they generate an $n$-ary to $n$-ary function, in this case:
(x,y) -> (y,x)
This seems to be a 'monad' and it would be interesting to see if these domains could be implemented as instances of a monad (a monad in category theory terms, not the current FriCAS monad category).
For more details see:
https://www.euclideanspace.com/maths/standards/program/mycode/computation/- Tutorial for lambda calculus:
- Tutorial for SKI calculus:
- Tutorial for Intuitionistic Logic
- Tutorial for utilities to coerce between computation domains
- Tutorial for FriCAS source code generation
To Do
There are improvements and corrections required for later versions of this software.
- Overall architecture:Investigate possibility of basing implementation on Kernel or SExpression domains. Or we could extend some non-associative or binary tree structure class?
- Possible generalisations:
- I am working on a function composition (hom-set) domain
and it would be interesting to implement these as a special (non-associative) version of that.
- It would be interesting to see if these domains could be implementedas instances of a monad.
- I would also like to extend this to investigate abstract structuressuch as 'tree automata'.
- Need to improve and correct intuitionistic logic domain.
- investigate change of meaning of '=' for intuitionistic logic torepresent equivalence rather than equality.
- implement more complete algorithm to decide if two (quantifier-free)intuitionistic formulas are equivalent.
- make sure we have all simplifications for implies,/\, \/ and ~.
Notation
It would be useful to be able to use unicode, at the moment we can't for compatibility reasons. When the restrictions on using unicode are lifted then the following would be useful:
- lambda symbol
- alpha (as in alpha-substitution)
- beta (as in beta-equivalence)
- bottom symbol for \verb'_|_'
Currently for logic symbols we use notation:
as opposed to other posibilities such as:
- \verb'true, false, and or'
- \verb'0, 1, &, |'
- \verb'join, meet, ¬'
This is because \verb'/\, \/, ~' are built-in operators in FriCAS and are already used by Logic category.
Also this emphasises the lattice-like structure of the intuitionistic logic domain. Also some systems of logic seem to treat false. The aim is to use symbols that are compatible with both logic and lattice terminology.
Implication is notated by -> to suggest its link to 'function' although perhaps this should be changed to more standard =>.
In lambda calculus the elements are functions. Function application and composition is notated by space, that is
f g represents f(g)
In lisp notation this would be (f g). Although we can use brackets they are only used to indicate precidence and not to specify a function since all variables are assumed functions.
I have used the term 'function application' for the following form: f:A->B g:A = f g:B and the term 'function composition' for the following form: f:B->C g:A->B = f g:A->C