On these pages are Axiom/FriCAS implementations of various mathematical structures related to computation and type theory.
The aim here is to model and study abstract models of computing such as λ-calculus, combinators and intuitionistic logic. These abstract mathematical structures, which were discovered before modern computers, are worthy of study in their own right.
We a less interested in using these domains to do actual computing than to study the structures and their relationships to each other. If we only wanted to evaluate a λ function then there are many other programs that could you that. So, in these domains such as lambda, we do not attempt to reduce as soon as it is constructed (although redux can be called if explicitly required). Instead we leave it as a structure to be combined, transformed, compared and studied.
We are also interested in the reationship to logic, this approach is based on the ideas of Philip Wadler and others. A program that uses this approach is Djinn.
The arguments of these 'computation' domains are functions and combinators and the operation is function composition. For combinators the number of arguments is variable and so function composition is non-associative hence it is represented by binary tree structure. For Lambda calculus 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. Conventional 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 there appears to be links between these various types of function composition which I would like to investigate.
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, on this page, we see that this λ 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).
I would also like to extend this to investigate abstract structures such as 'tree automata'.
λ-calculus |
A formal system for function definition and application. Untyped lambda calculus is the original inspiration for functional programming, in particular Lisp. |
Ski combinators |
Were introduced by Moses Schönfinkel and Haskell Curry with the aim of eliminating the need for variables in mathematical logic. It is equivalent to λ-calculus but it can be used for doing, without variables, anything that would require variables in other systems. The structure is a self-modifing binary tree. |
Intuitionistic Logic tutorial on this page |
The intuitionisticLogic domain implements a Heyting algebra implied by intuitionistic logic similar to boolean algebra. Intuitionistic or constructive logic is similar to classical logic but where the law of excluded middle is not used. |
Logic Utility Package |
The compUtil package provides utilities to convert between the computational domains: Lambda, Ski and ILogic. |
Code Generation Package |
compCode is a package in the computation framework allows FriCAS source code to be created from the abstract structures in the framework |
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 implemented as instances of a monad.
- I would also like to extend this to investigate abstract structures such as 'tree automata'.
- Need to improve and correct intuitionistic logic domain.
- investigate change of meaning of '=' for intuitionistic logic to represent 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 _|_
Currently for logic symbols we use notation:
T, _|_, /\, \/, ~ \
as opposed to other posibilities such as:
- true, false, and or
- 0, 1, &, |
- join, meet, ¬
This is because /\, \/, ~ 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 _|_ as a logical contradiction rather than 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 =>.
Related Structures
If we want to cover the full range of mathematical structures related to computing then we should really include Finite State Machines and Automata. These are coalgebra-like structures which are related to the algebra structures already included.
I was thinking about how to convert a finite state machine into a instance of Lambda, then I realised this is just about implementing stateful code in a pure functional language and Haskell has already solved that problem - use monads (from my limited knowledge of Haskell I get the impression, whatever the problem, the answer is to use monads).
Perhaps FriCAS should have a lattice structure which could then be extended into intuitionistic logic domain. I don't think partially ordered set (setorder.spad.pamphlet) would be in the right form to extend logic domains.
Also graph structures, for instance:
- A deductive system is a graph where the nodes are formulas and the arrows are deductions or proofs.
- The category of small graphs is a concrete category.
Many of the domains in this document are also tree structures.
Category Theory
Lambek and Scott 1988 show that typed lambda-calculi and cartesian closed categories are essentially the same and intuitionistic logic is closely related to topos theory.
Also the discussion of monads above tends to indicate that they need to be used here.
Also the common use of function composition.
All of this suggests to me that all the code in this document would benifit from being put into a wider framework based on category theory.
Variables and Types
The various domains above use variables so before we get on to the main domains we have some code to represent variables in Lambda and Ski domains. Since we are working in terms of functions then a variable will be a function (possibly a constant function).
There is a category 'VarCat' to represent these function variables and there are two implementations of this category so far:
- Untyped - Untyped represents an untyped variable in Lambda and Ski domains, a variable has a name represented by a String.
- Typed - Typed represents an typed variable in Lambda and Ski domains, a variable has a name represented by a String and a type represented by a tree of strings.
There may be possibly be other implementations in the future. For instance we could introduce a typed variable which could have FriCAS types instead of abstract types represented by strings. This might allow more interaction with other domains, although as already stated, the main aim is to implement these as abstract structures like any other mathematical structure.
- How do we handle (and should we handle) subtypes and the various flavors of polymorphism? I was thinking of an additional type domain within this category whose representation is a list of sub-types, which in turn may have sub-sub-types. In other words a tree structure. Most of the structures in this computation framework are already tree structures so this fits the pattern.
- How do we handle (and should we handle) compounded types such as 'List over String'?
- It would be interesting to have a type domain in this category where the types were FriCAS types. This would be an exception, usualy I would prefer an abstract type model, but it may be possible to do interesing things by mapping FriCAS to an abstract type model.
- Could these type models be used outside of the computation framework? For instance a set whose elements may be assigned different types.
I am trying to develop an abstract model of general mathematical structures here, not a sub-language within FriCAS, so I don't want to over specify this. However I think it would be good to specify a model which is as general as possible and can be expanded to model these things.
Variables Tutorial
The two implementations: Untyped and Typed which can be constructed as follows:
(1) -> )library VTYP
VarTyp is now explicitly exposed in frame frame1
VarTyp will be automatically loaded when needed from
/home/martin/VTYP.NRLIB/VTYP
(1) -> )library VARCAT
VarCat is now explicitly exposed in frame frame1
VarCat will be automatically loaded when needed from
/home/martin/VARCAT.NRLIB/VARCAT
(1) -> )library UNTYPED
Untyped is now explicitly exposed in frame frame1
Untyped will be automatically loaded when needed from
/home/martin/UNTYPED.NRLIB/UNTYPED
(1) -> )library TYPED
Typed is now explicitly exposed in frame frame1
Typed will be automatically loaded when needed from
/home/martin/TYPED.NRLIB/TYPED
(1) -> var("x")$Untyped
(1) x
Type: Untyped
(2) -> var("x",varTyp("a"))$Typed
(2) x:a
Type: Typed
(3) -> parseVar("x:(a->b)")$Typed
(3) x:(a->b)
Type: Typed
(4) -> parseVar("x:(a/\b)")$Typed
(4) x:(a/\b)
Type: Typed
(5) -> parseVar("x:(a\/b)")$Typed
(5) x:(a\/b)
Type: Typed |
In (3) we are entering a variable with a more complicated type (in this case 'a->b') so it is easier to use parseVar to construct from a string although this could have been built from raw types.
parseVar also requires '1' which means: start parsing at position 1 in the string. It returns x:a->b which means variable 'x' from type 'a' to type 'b' and 7 which is the position of the pointer after this term has been parsed.
Variables are not usually constructed directly by the user but instead are used by lambda and ski domains.
Future Enhancements
Interaction with SPAD types
These mathematical structures are implemented in the same way as any other algebras implemented in SPAD and they are intended to interact with the other SPAD algebras in the usual way. That is, there is nothing special about them because they are related to computing, after all these structures were discovered and used before electronic computers.
So, for instance, when developing typed versions of these algebras we can define a type system which is separate from, and independent of, the SPAD type system.
Since these structures concern functions it would be nice, as an additional bonus, if they could be applied to existing SPAD functions. For instance, in the existing String type:
concat("ab","cd") = "abcd"
but on the Ski combinator tutorial we saw that S(K(SI))K reverses the order of the operands so it would be good if we could apply it to an existing function likes this:
S(K(SI))K concat("ab","cd") = "cdab"
This is just an idea, it is not possible at the moment, it would be a bonus if it were possible but it is not the main intention.
Lifting
It would be good to replace definations of algebas in terms of arbitary elements of the algebra:
∀x,y. x*y = y*x
with an external definition using no elements of the algebra:
S(K(SI))K * = *
and also work purely in terms of combinators (cancel out the vaiables that they are being applied to) such as:
SKK=I
Next
Modeling Computation
