Maps abstract computational structures to real-world FriCAS code.
compCode is a package in the computation framework (the wider computation framework is discussed here) that allows FriCAS source code to be created from the abstract structures in the framework. This is done by the following functions:
writePackage
'writePackage' creates source code for a FriCAS package from a list of lambda structures over typed variables. This is reasonably easy to do since functions in a FriCAS package have a similar structure to lambda functions.
writeCategory
'writeCategory' creates source code for a FriCAS package from a list of ILogic structures. This relies on the Curry-Howard isomorphism between intuitionistic logic and types in a computation.
Example
In intuitionistic logic if we know 'a' and we know 'a->b' then we can deduce b (by modus ponens) that is:
(a /\ (a -> b) ) -> b
Curry-Howard isomorphism relates this intuitionistic logic to types in a computation so given types 'a' and 'a->b' then we can create any of these function types without using additional information (other functions or constants):
- func1:(a,a->b) -> a
- func2:(a,a->b) -> (a->b)
- func3:(a,a->b) -> b
func3 is more interesting since func1 and func2 can be created by passing on one of its parameters and throwing away the other.
So how can we implement this? From the original (a /\ (a -> b) ) we need to expand out to (a /\ (a -> b) /\ b) containing all factors.
By the Curry-Howard isomorphism we can coerce to the intuitionisticLogic from Lambda. This gives an isomorphism where theorems in intuitionistic logic correspond to type signatures in combinatory logic and programs in intuitionistic logic correspond to the proofs of those theorems in combinatory logic.
As an example of this in Haskell see "Djinn, a theorem prover in Haskell, for Haskell" here:
see also: Philip Wadler - Theorems for free!
Code Generation Package - Tutorial
First we may need to expose the reqired code such as ILOGIC and COMPCODE
(1) -> )expose COMPCODE (1) -> )expose ILOGIC |
We can generate the source code for a FriCAS package from lambda expressions. To start we will create some typed variables and lambda terms to work with:
(1) -> vx := var("x",varTyp("String"))$Typed
(1) x:String
Type: Typed
(2) -> vy := var("y",varTyp("String"))$Typed
(2) y:String
Type: Typed
(3) -> nx := lambda(vx)
(3) x:String
Type: Lambda(Typed)
(4) -> ny := lambda(vy)
(4) y:String
Type: Lambda(Typed) |
Now we create some lambda expressions to be convered to source code:
(5) -> pacEx1:Lambda Typed := lambda(nx,vx)$Lambda Typed
(5) (\x.x)
Type: Lambda(Typed)
(6) -> pacEx2:Lambda Typed := lambda(pacEx1,vy)$Lambda Typed
(6) (\y.(\x.y))
Type: Lambda(Typed)
(7) -> pacEx3:Lambda Typed := lambda(lambda(nx,ny),vy)$Lambda Typed
(7) (\y.(x:String y))
Type: Lambda(Typed) |
Now we generate the source code using the writePackage function where:
- testComp1.spad is the filename
- TESTCCP is the short name
- TestCCP is the long name
- Type is the category name
(8) -> writePackage([pacEx1,pacEx2,pacEx3],"testGeneratedCode.spad"_
,"TESTCCP","TestCCP","Type")
Type: Void |
When we look at the testComp1.spad file we can see the code that has been generated:
)abbrev package TESTCCP TestCCP TestCCP(): Exports == Implementation where Exports ==> Type with Implementation ==> add fn1(x:String):String == x fn2(y:String):String == x+->(y) fn3(y:String):String == x(y) @ |
This code may have to be tweeked by hand before it can be used.
Now we can move on to generate the source code for a FriCAS category from intuitionistic logic expressions. To start we will create some intuitionistic logic terms as examples:
(9) -> catEx1:ILogic := implies(proposition("a"),_
proposition("b"))/\proposition("a")
(9) ((a->b)/\a)
Type: ILogic
(10) -> catEx2:ILogic := proposition("a")/\proposition("b")
(10) (a/\b)
Type: ILogic |
Now we generate the source code using the writeCategory function where:
- testComp2.spad is the filename
- TESTCC is the short name
- TestCC is the long name
(11) -> writeCategory([catEx1,catEx2],"testComp2.spad","TESTCC","TestCC")
Type: Void |
When we look at the testComp2.spad file we can see the code that has been generated:
)abbrev category TESTCC TestCC TestCC() : Category == Type with fn1:(a->b,a) -> b fn2:(a,b) -> a @ |
In fn1 type 'b' was generated from 'a->b' and 'a' (by modus ponens). If two or more deductions were made then only the first would be used. In fn2 no additional deductions could be made, in this case the first parameter is used as the deduction.
Next
Modeling Computation