Computation

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
tutorial on this page

A formal system for function definition and application. Untyped lambda calculus is the original inspiration for functional programming, in particular Lisp.

Ski combinators
tutorial on this page

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
tutorial on this page

The compUtil package provides utilities to convert between the computational domains: Lambda, Ski and ILogic.

Code Generation Package
tutorial on this page

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.

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:

Currently for logic symbols we use notation:

T, _|_, /\, \/, ~ \

as opposed to other posibilities such as:

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:

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:

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.

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

 


metadata block
see also:
Correspondence about this page

Book Shop - Further reading.

Where I can, I have put links to Amazon for books that are relevant to the subject, click on the appropriate country flag to get more details of the book or to buy it from them.

flag flag flag flag flag flagJ. Lambek, P. J. Scott - 1988 - Introduction to Higher-Order Categorical Logic - show that typed lambda-calculi and cartesian closed categories are essentially the same and intuitionistic logic is closely related to topos theory.

 

This site may have errors. Don't use for critical systems.

Copyright (c) 1998-2017 Martin John Baker - All rights reserved - privacy policy.