Computation - Code Generator

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):

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:

(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:

(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

 


metadata block
see also:
Correspondence about this page

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

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