r5 - 26 Jun 2008 - 09:25:02 - Yuri KlimovYou are here: TWiki >  XSG Web > UGPSeminarSlides

Семинар в УГП 26 июня 2008г.

Слайды

Данные, функции, арность/коарность
A : 0
B : 0
C : 0
D : 0

CONS : 2
NIL  : 0

ab : , List
ab, CONS A (CONS B NIL)

t2t : 2, 3
t2t ?x ?y, x y x

Списки
abcd : , List
abcd, CONS A (CONS B (CONS C (CONS D NIL)))

head : List, Atom
head (CONS ?x ?xs), x

tail : List, List
tail (CONS ?x ?xs), xs

concat : List List, List
concat (NIL        ) ?ys, ys
       (CONS ?x ?xs) ?ys, CONS x (concat xs ys)

Списки 2
reverse : List, List
reverse (NIL        ), NIL
        (CONS ?x ?xs), concat (reverse xs)
                              (CONS x NIL)

reverse' : List, List
reverse' ?xs, reverse'' xs NIL

reverse'' : List List, List
reverse'' (NIL        ) ?ys, ys
          (CONS ?x ?xs) ?ys,
                       reverse'' xs (CONS x ys)

Равенство
concat : List List, List
concat (NIL        ) ?ys, ys
       (CONS ?x ?xs) ?ys, CONS x (concat xs ys)

concat' : List List, List
concat' ?xs ?ys, xs=(NIL        ), ys
        ?xs ?ys, xs=(CONS ?x ?xs),
                         CONS x (concat' xs ys)
{- haskell:
concat xs ys =
  case xs of
    NIL       -> ys
    CONS x xs -> CONS x (concat xs ys) -} 

Равенство 2
T : 0
F : 0

and : Bool Bool, Bool
and ?x ?y, x = T, y = T, T

hang : , Bool
hang , hang

{- Haskell:
and x y = case (x, y) of
            (True, True) -> True
            (_   , _   ) -> False -}

Равенство 3
firstButNotLast : Atom List, Bool
firstButNotLast ?x (CONS x (CONS ?y ?ys)), T

{- Haskell:
firstButNotLast :: Atom -> List -> Bool
firstButNotLast x (CONS z (CONS y ys)) | x==z
                                     = True
firstButNotLast _ _                  = False -}





Равенство*
  1. Справа и слева выражения
    exp == exp(?x, ?y)
  2. Свободные переменные могут быть как справа, так и слева
    exp(?u, ?v) == exp(?x, ?y)
  3. Выражение это не только конструкторы, но и функции!
    f (?u, ?v) == exp(?x, ?y)

split : List, List List
split ?xs, xs=(concat ?ys ?zs), ys zs

Недетерминизм
split : List, List List
split ?xs          , NIL xs
      (CONS ?x ?xs), (split xs)=(?ys ?zs),
                                 (CONS x ys) zs

split' : List, List List
split' ?xs, xs=(concat ?ys ?zs), ys zs

combs : Integer Integer, Integer_list
combs O      O     , NIL
      ?k     (I ?n), CONS A (combs k n)
      (I ?k) (I ?n), CONS B (combs k n)

Что же получилось*
  1. Удобная работа с множествами.
       intersect : 2, 1
       unify     : 2, 1
    
       intersect ?x x, x
    
       unify ?x ?y, x
             ?x ?y, y
       
  2. Средства метавычислений доступны из языка.
    Если есть функция f, множество входных данных class_in, множество результатов class_out, то легко проделываются:
    • прямая интерпретация:
      INT
      f class_in;
    • инверсное вычисление:
      URA
      f ?x, x = class_out, x;
    • табулирование всех возможных результатов f:
      TAB
      ?x (f x);
    • определение всех вариантов совпадения f и g:
      SURA
      f ?x = g ?y, x y.

Числа
O : 0
I : 1

_0 : , Int
_0 , O
_1 : , Int
_1 , I O
_2 : , Int
_2 , I I O

add : Int Int, Int
add (O   ) ?y, y
    (I ?x) ?y, I add x y

Вычитание
add : Int Int, Int
add (O   ) ?y, y
    (I ?x) ?y, I add x y

sub : Int Int, Int
sub (?x  ) (O   ), x
    (I ?x) (I ?y), sub x y

sub' : Int Int, Int
sub' ?x ?y, x=(add y ?z), z

Списки и числа
concat (NIL        ) ?ys, ys
       (CONS ?x ?xs) ?ys, CONS x (concat xs ys)

length (NIL        ), O
       (CONS ?x ?xs), I (length xs)

take : Int List, List
take (O   ) (?xs        ), NIL
     (I ?n) (CONS ?x ?xs), CONS x take n xs

take' : Int List, List
take' (length ?xs) (concat xs ?ys), xs

Списки и числа 2
concat (NIL        ) ?ys, ys
       (CONS ?x ?xs) ?ys, CONS x (concat xs ys)

length (NIL        ), O
       (CONS ?x ?xs), I (length xs)

drop : Int List, List
drop (O   ) (?xs        ), xs
     (I ?n) (CONS ?x ?xs), drop n xs

drop' : Int List, List
drop' (length !xs) (concat xs !ys), ys

Списки и числа 3
concat (NIL        ) ?ys, ys
       (CONS ?x ?xs) ?ys, CONS x (concat xs ys)

length (NIL        ), O
       (CONS ?x ?xs), I (length xs)

splitAt : Int List, List List
splitAt (O   ) (?xs        ), NIL xs
        (I ?n) (CONS ?x ?xs), CONS x
                                 (splitAt n xs)

splitAt' : Int List, List List
splitAt' (length ?xs) (concat xs ?ys), xs ys

Списки и числа 4
concat (NIL        ) ?ys, ys
       (CONS ?x ?xs) ?ys, CONS x (concat xs ys)

length (NIL        ), O
       (CONS ?x ?xs), I (length xs)

takeAt : Int List, Atom
takeAt (O   ) (CONS ?x ?xs), x
       (I ?n) (CONS ?x ?xs), takeAt n xs

takeAt' : Int List, Atom
takeAt' (length ?xs) (concat xs (CONS ?y ?ys)),
                                              y
-- Yuri Klimov - 26 Jun 2008
Edit | WYSIWYG | Attach | Printable | Raw View | Backlinks: Web, All Webs | History: r5 < r4 < r3 < r2 < r1 | More topic actions
 
Powered by TWiki

This site is powered by the TWiki collaboration platformCopyright © by the contributing authors. All material on this collaboration platform is the property of the contributing authors.
Ideas, requests, problems regarding TWiki? Send feedback